Draft: optics and implications

This is something that had been nagging me for a while. I've been wanting to add a modicum of optics in GHC. I think this has a potential of helping a lot.

This (draft) MR demonstrate a few ways in which it can be used:

• subterm traversals (à la Scrap your Boilerplate) for binding trees
• avoid duplicate logic about finding elements of a certain type in syntax trees (zonking and substituting, in this draft, both look for types to substitute)

A few design notes:

• The optics library is designed to be tiny to avoid any extra dependency in the bootstrap cycle.
  • This is why I chose to focus on optics that can be expressed in a -> f b form (in particular: no profunctor (in particular: no prism)). Just lenses and traversals seem to suffice for now.
• These optics are modified to understand the concept of binding. Designing this part took me most of my time, but I'm pretty happy with the status. This translates as one extra argument to optics. When irrelevant, it could be hidden by builder functions.
• As proud as I am of my clever trick with data kinds and type families, I'm thinking it should probably be scraped in favour of two type argument per position (Optic var var' s t a b instead of Optic var s a)
  • This trick can be used to handle homogeneous optics and heterogeneous optics with a single type or to define a category theory instance, but not both (you can define a category instance either way, but it won't be able to compose a homogeneous optics and a heterogeneous optic, so it's rather worthless).
  • The category instance (which was my original motivation for using pairs of types instead of multiple arguments) requires me to invert the order of the arguments compared to the lens library, and I'm not sure the extra surprise is worth it.
    • This would force us to come up with a name for the optics composition operator. Naming is hard, avoiding naming was my reason for wanting a category instance in the first place.
  • Type families have a tendency to create ambiguous variable type errors. Which are harder to debug than unification type errors. It hasn't been a big issue, honestly. But type errors inside GHC can be puzzling enough as they are, so maybe something more straightforward is better.
• There are a bunch of environment-passing variant of optics combinators (overenv, etc…) which I haven't found an opportunity to use yet. I've put them in because such combinators are used a lot in the Coq proof assistant's source, so I expected to need them. I'd still leave them around because I feel that their existence will make some idioms easier in the future (maybe there are already opportunities. Substitution could be phrased in that way for instance).
• To fully take advantage of subterms traversal, we would need to take into account that coercions and types are mutually recursive, and make traversals that traverse both types. I don't know how to do that without either adding an extra box (worrying for performance-critical code) or making Type and Coercion part of the same GADTs (not reasonable). So there's a discussion to be had about how to best handle this situation.
  • In fact, it's not only subterms traversal: we also want to traverse CoreExpr and such and reach both the Coercion and Type locations (for substitution, zonking, in particular).

---

My goal with this draft is to gauge interest. Is it something that we want to do? maybe only part of this? Interestingly, in terms of lines of code, the MR doesn't pay for itself at all, the gains in files are about compensated by extra lines of code, and the optics library itself is on top of all this more-or-less-equal refactor. For the record: I very much want this. I feel that the code thus obtained is much more orthogonal. I've been motivated by my patches on linear types, and how much they tend to interact. And I believe that with this approach we can help make conflicts less frequents.

I think this may be of interest to @phadej and @hsyl20 . Let me also tag @simonpj and @rae : feel free to turn notification off if you want to bail out of this conversation if you don't care, but I consider you owners of this part of the code that I'm proposing to refactor, so I don't want to do this without your knowing.