Stream: new members
ohhaimark (Oct 17 2019 at 13:49):
Has anyone had implemented lenses in lean? Would it be helpful in mathlib, or useful to formalize here?
Johan Commelin (Oct 17 2019 at 13:57):
What is a lens?
ohhaimark (Oct 17 2019 at 13:58):
Edward Ayers (Oct 17 2019 at 14:02):
I remember chatting about this at Lean Together 2019
Edward Ayers (Oct 17 2019 at 14:03):
I had a go at implementing them but I didn't finish.
Edward Ayers (Oct 17 2019 at 14:12):
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 (Oct 17 2019 at 14:16):
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 (Oct 17 2019 at 14:17):
Yeah sorry. I'm looking for another source.
Edward Ayers (Oct 17 2019 at 14:19):
Johan Commelin (Oct 17 2019 at 14:21):
ohhaimark (Oct 17 2019 at 14:21):
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 (Oct 17 2019 at 14:21):
If you like pictures: http://adit.io/posts/2013-07-22-lenses-in-pictures.html
Johan Commelin (Oct 17 2019 at 14:22):
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 (Oct 17 2019 at 14:22):
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 (Oct 17 2019 at 14:43):
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
Last updated: May 15 2021 at 23:13 UTC