I’ve been meaning to look into lenses for quite some time. They seem to be useful when working with Redux. But when looking into how to implement them there are a lot of varieties of lenses. Do you know any good explanation of the theory bebind lenses?
There are a few theories, the nicest one is as follows: a value of type Lens s a is a demonstration that values of type s can be split into (x, a) for some unknown type a. If we talk about Iso a b which says that a and b are the same type then Lens s a = exists x. Iso s (x, a).
Another way to look at it is that a lens pairs a getter and a setter, so we can say Lens s a is the same as { get :: s -> a, set :: a -> s -> s }.
All of these constructions have to follow some rules (the intuitive ones) like “if you set and then get you’ll get what you just set” also “if you set and then set it’s the same as just setting that second time” and also “if you set what you just got it’s the same as doing nothing at all”.
If you consider the construction a | b to mean “a or b, and I know which one” so that Int | Int is distinct from Int then we can consider a thing called a Prism s a which, parallel to above, can be considered the same as Prism s a = exists x . Iso s (x | a). In other words, when you’ve got a Prism s a you’ve got evidence for how to see s as either an a or something else.
Prisms aren’t really getter-setter pairs, but they’re something close. You need to be able to always convert an a directly into an s, but also maybe pull an a out (unless it’s the other thing). So, we say Prism s a is the same as { retract :: a -> s, extract :: s -> Maybe a } where Maybe means you might fail to produce that a sometimes.
This one is really a foreign concept. Here’s an example: there’s a Prism String Int which is a printer/parser pair for integers. In other words, we consider String to be equivalent to x | Int where x stands in for “all of the strings which fail to parse as an int”. So retract just prints an Int out and extract is our (potentially failing) parser. Prisms are printer/parser pairs.
All of these things can combine with one another. There are interesting theories around “Profunctor and/or Functor transformations” which make all of the compositions fall out as natural consequences. It’s good for implementers but only so useful for just understanding the thing.
There are also “type changing” lenses/prisms which let you handle generic/templated types well and more exotic “optics” like traversals and folds. All of these things continue to compose with one another nicely and fit into the same universe of ideas. It’s really quite rich!
Lenses are great fun, glad to see they’re making their way to more communities :)
I’ve been meaning to look into lenses for quite some time. They seem to be useful when working with Redux. But when looking into how to implement them there are a lot of varieties of lenses. Do you know any good explanation of the theory bebind lenses?
There are a few theories, the nicest one is as follows: a value of type
Lens s ais a demonstration that values of typescan be split into(x, a)for some unknown typea. If we talk aboutIso a bwhich says thataandbare the same type thenLens s a = exists x. Iso s (x, a).Another way to look at it is that a lens pairs a getter and a setter, so we can say
Lens s ais the same as{ get :: s -> a, set :: a -> s -> s }.All of these constructions have to follow some rules (the intuitive ones) like “if you set and then get you’ll get what you just set” also “if you set and then set it’s the same as just setting that second time” and also “if you set what you just got it’s the same as doing nothing at all”.
If you consider the construction
a | bto mean “aorb, and I know which one” so thatInt | Intis distinct fromIntthen we can consider a thing called aPrism s awhich, parallel to above, can be considered the same asPrism s a = exists x . Iso s (x | a). In other words, when you’ve got aPrism s ayou’ve got evidence for how to seesas either anaor something else.Prisms aren’t really getter-setter pairs, but they’re something close. You need to be able to always convert an
adirectly into ans, but also maybe pull anaout (unless it’s the other thing). So, we sayPrism s ais the same as{ retract :: a -> s, extract :: s -> Maybe a }whereMaybemeans you might fail to produce thatasometimes.This one is really a foreign concept. Here’s an example: there’s a
Prism String Intwhich is a printer/parser pair for integers. In other words, we considerStringto be equivalent tox | Intwherexstands in for “all of the strings which fail to parse as an int”. Soretractjust prints anIntout andextractis our (potentially failing) parser. Prisms are printer/parser pairs.All of these things can combine with one another. There are interesting theories around “Profunctor and/or Functor transformations” which make all of the compositions fall out as natural consequences. It’s good for implementers but only so useful for just understanding the thing.
There are also “type changing” lenses/prisms which let you handle generic/templated types well and more exotic “optics” like traversals and folds. All of these things continue to compose with one another nicely and fit into the same universe of ideas. It’s really quite rich!
This is the best, most intuitive description of lenses I’ve ever seen. Thank you!
I’m glad!
In the first sentence: “… some unknown type
x” not “a”. Whoops!