Zulip Chat Archive

Stream: new members

Topic: Do lenses fit anywhere in mathlib?


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Oct 17 2019 at 13:57):

What is a lens?

view this post on Zulip ohhaimark (Oct 17 2019 at 13:58):

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

view this post on Zulip Edward Ayers (Oct 17 2019 at 14:02):

I remember chatting about this at Lean Together 2019

view this post on Zulip Edward Ayers (Oct 17 2019 at 14:03):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip ohhaimark (Oct 17 2019 at 14:17):

Yeah sorry. I'm looking for another source.

view this post on Zulip Edward Ayers (Oct 17 2019 at 14:19):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 14:21):

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

view this post on Zulip 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.

view this post on Zulip Kevin Kappelmann (Oct 17 2019 at 14:21):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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