Do lenses fit anywhere in mathlib?

Stream: new members

[ohhaimark]

Has anyone had implemented lenses in lean? Would it be helpful in mathlib, or useful to formalize here?

[Johan Commelin]

What is a lens?

[ohhaimark]

http://hackage.haskell.org/package/lens

[Edward Ayers]

I remember chatting about this at Lean Together 2019

[Edward Ayers]

I had a go at implementing them but I didn't finish.

[Edward Ayers]

If I remember, I basically got it working but I had many issues with getting coercions between the different classes (prism, optic, iso etc) to be painless. I'll dig it up and link to it.

[Johan Commelin]

That package is really bad at telling me what a lens is. Do I need to read the code to figure it out? They only tell me how to use it. Not what it is.

[ohhaimark]

Yeah sorry. I'm looking for another source.

[Edward Ayers]

https://github.com/EdAyers/edlib/blob/master/lens.lean

[Johan Commelin]

https://en.wikibooks.org/wiki/Haskell/Lenses_and_functional_references helps

[ohhaimark]

In short, lenses are a way to update part of a whole and are composable. For example if you have nested records, then you can have a lens for accessing each field. In c terms, it's like a functional lvalue.

[Kevin Kappelmann]

If you like pictures: http://adit.io/posts/2013-07-22-lenses-in-pictures.html

[Johan Commelin]

So, as a mathematician I'm supposed to find them not interesting at all. Except that they might be really handy as implementation toolkit for complex mathematical objects, and so it's good if I know what they are.

[Edward Ayers]

I implemented like the minimum amount so that I could understand what lenses are and then I gave up, so don't expect too much!

[Simon Hudon]

I've been playing with the idea of having lenses in Lean for a while. There's no approach I have found that reproduces the flexibility of the Haskell lenses. The question becomes: where is the sweet spot. I'm not sure