Lenses and zippers are not mutually exclusive ways of looking at the world. You can build a "movable focus" datatype on top of lenses, by reifying a chain of lenses as a type-aligned stack. Keeping track of the types you visited on your way down a structure means you know what types you'll be looking at when you go back up.
The API of this "movable focus" looks roughly like this:
empty :: Path (E :> a)
up :: Path (as :> a :> b) -> Path (as :> a)
down :: Path (as :> a) -> Traversal' a b -> Path (as :> a :> b)
left :: Path (as :> a :> b) -> Path (as :> a :> b)
right :: Path (as :> a :> b) -> Path (as :> a :> b)
flatten :: Path as -> Traversal' (Top as) (Bottom as)
Path
is parameterised by a snoc-list of types. The type of the "current focus" of the Path
is the rightmost element of the list.
Given a Path
which focuses on an a
in some structure, you can use down
to append a Traversal' a b
, to get back a Path
which focuses on a b
(namely, the first result of the Traversal
). You can then go back up
, which pops the most recently-appended Traversal
to give you back a Path
which focuses on an a
again. left
and right
move the focus around inside the topmost Traversal
.
You also need a way to turn a Path
back into an actual Traversal
, in order to access the actual value that your Path
zooms in on. The flatten
combinator does this. Top
and Bottom
are a pair of type families which find the leftmost and rightmost elements of a snoc-list, respectively.
So how's it implemented?
infixl 5 :>
data Snoc a = E | Snoc a :> a
type family Top as where
Top (E :> a) = a
Top (as :> _) = Top as
type family Bottom as where
Bottom (_ :> a) = a
data Path as where
Top :: Path (E :> a)
Child :: Path (as :> a) -> Traversal' a b -> Int -> Path (as :> a :> b)
Path
is a stack-shaped GADT. The Top
constructor creates an empty Path
- a path from any value to itself. The Child
constructor focuses on a particular element of a Traversal
- it contains the parent Path
which focuses on an a
, a Traversal
from a
to b
, and an Int
representing the particular element of the Traversal
which the Path
focuses on.
empty
creates an empty path.
empty :: Path (E :> a)
empty = Top
up
takes a non-empty path (guaranteed by the type) and pops the topmost Traversal
from it.
up :: Path (as :> a :> b) -> Path (as :> a)
up (Child p _ _) = p
down
takes a Traversal
and appends it to a Path
, focusing on the leftmost result of the Traversal
.
down :: Path (as :> a) -> Traversal' a b -> Path (as :> a :> b)
down p t = Child p t 0
left
and right
don't change the level of the structure that you're focusing on - no adding or removing traversals from the stack - they just change which element of the topmost traversal the path points to.
left :: Path (as :> a :> b) -> Path (as :> a :> b)
left (Child p t n) = Child p t (n - 1)
right :: Path (as :> a :> b) -> Path (as :> a :> b)
right (Child p t n) = Child p t (n + 1)
flatten
looks at each traversal in turn and uses elementOf
to focus on a particular element of the traversal. It composes them all together using .
.
flatten :: Path as -> Traversal' (Top as) (Bottom as)
flatten Top = id
flatten (Child p t n) = flatten p . elementOf t n
Path
isn't a zipper, exactly. An important part of what makes a zipper a zipper is that you can efficiently view or edit the focus and its neighbours without traversing or rebuilding the whole thing. Path
merely composes traversals without reference to a particular structure, so it's just as inefficient as working with whole traversals.
However, it's not a big leap from Path
to a true zipper. The zippers
package provides true zippers - cursors with efficient access to a focused part of an actual structure - generically, based on this idea of a type-aligned sequence of lenses. As you descend through a structure, the Zipper
unpacks each traversal into a data structure rather like your Loc
. Then when you go back upward
it writes the new values back into the structure using the Traversal
.