Relationship to Lenses?

[gmalecha]

This is nice. I'm wondering if you've thought about the connection to lenses. I cooked up a (very simple) library for lenses (https://github.com/gmalecha/coq-lens) that has been fairly convenient in my work and overlaps quite a bit with what you're doing here. I'm wondering if there is some possibility to unify these efforts.

[tchajed]

Yeah, lenses make a lot of sense in conjunction with this library. It shouldn't be hard to define and implement lenses on top of the Setter typeclass, and then let record-update generate those instances with Ltac (which is a bit hacky but I try hard to avoid depending on plugins in my work).

If you want to implement that here then that would definitely be welcome! I haven't personally run into complicated in enough structs to require nested updates, and where it has come up I just nested calls to set.

[tchajed]

I implemented something in ca0fe8ef47fd95c99ab3241abf0e4f61ad6dd357 - it's really just your definitions of lenses and lens composition, with a way to definition that turns a projection function into a lens using this library. Is there something else you think we can do, without a plugin?

[gmalecha]

I guess the delta between what you have and lenses is just the packaging. Lenses bundle together getters and setters and you address them through two type classes. The standard lens also supports polymorphic update which is useful, but unfortunately greatly complicates the laws.

I could imagine that the plugin-using code be pulled off to a separate repository if that seems like a problem.

I'd be interested in better understanding the pros and cons of the two and generally building up this infrastructure to be more comprehensive. A unified interface around this could be very valuable to the Coq ecosystem, it is certainly very valuable in Haskell, though there are questions (to me at least) of whether Coq can handle what Haskell can do.