This existential encoding kind of reminds me of a Zipper. You basically split a piece of data into a “context” and a “focus”, and then reassemble it (unzip and zip?). A lens focusing on a particular element of a list might have a c ~ ([a], [a]), for “elements before and after”.
Yeah there is a strong connection between optics and zippers - you can nearly think of them as essentially the same thing.
I think the Store encoding of lenses makes that clearer. The post misses one useful intermediate step between the getter/setter and van Laarhoven encoding - if you apply some DRY to
data Lens s a = Lens (s -> a) (s -> a -> s)
we can factor out the s -> to get
data Lens s a = Lens (s -> (a, a -> s))
or, a lens is a function which given an s, can give you an a, and a way to re-fill the hole made by removing that a from the s
This isn’t that different to what a zipper is - it’s the combination of some focused part of some structure, and the rest of the structure, whatever that rest is is what makes sense for that structure.
This existential encoding kind of reminds me of a Zipper. You basically split a piece of data into a “context” and a “focus”, and then reassemble it (unzip and zip?). A lens focusing on a particular element of a list might have a
c ~ ([a], [a]), for “elements before and after”.Yeah there is a strong connection between optics and zippers - you can nearly think of them as essentially the same thing.
I think the Store encoding of lenses makes that clearer. The post misses one useful intermediate step between the getter/setter and van Laarhoven encoding - if you apply some DRY to
we can factor out the
s ->to getor, a lens is a function which given an
s, can give you ana, and a way to re-fill the hole made by removing thatafrom thesThis isn’t that different to what a zipper is - it’s the combination of some focused part of some structure, and the rest of the structure, whatever that rest is is what makes sense for that structure.
Because there is this strong link, the Haskell lens package used to include Data.Lens.Zipper (now moved into its own package https://hackage.haskell.org/package/zippers-0.3.2/docs/Control-Zipper.html). What this gives you is the ability to use lenses to make zippers into any structure, with arbitrary movement around.