RFC: Make telescope constructors & functions use binding operators

[andrevidela]

Description

Asking for opinions here. I've been using telescopes with binding operators and it's been quite helpful. So my questions are:

• Should this go in or not?
• Should we move all the telescopes outside of contrib and into a library or into base? If so which one?

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md (and potentially also
  CONTRIBUTORS.md).

[buzden]

Asking for opinions here

• Should we move all the telescopes outside of contrib and into a library or into base? If so which one?

My opinion is that it should be moved outside contrib because shrinking the library with no single idea is a good thing. I think it should go to a separate library rather than to base, because I don't feel this thing needs to be in base. Maybe I feel so because I haven't used this module ever.

[gallais]

Should we move all the telescopes outside of contrib and into a library or into base?

I don't think we should: right telescopes indexed by a fixed size are a strict subset of right telescopes. So the library is not as general as could be.

[andrevidela]

I just realised it's not clear to me what's the objection:

• to move it outside contrib? (And therefore it should stay in contrib)
• to move it outside contrib and into its own library? (And therefore it should be moved into base)
• to move it outside contrib and into base? (And therefore it should be moved somewhere else)

[gallais]

I'm against making it part of base because it's a corner case of a more general theory.