Zipper - derived from type

Zipper is a way to represent the data type, allowing you to go through the structure and change individual elements, despite the functional purity. For example, if according to the list we can only run forward, doing something with elements, then with a zipper we can “be” in a certain element, move back and forth and change the current element.
Interestingly, a zipper for some type can be obtained literally by taking its derivative.

Let's try to come up with a zipper first for a list without mathematics.
We need the ability to go through the list forward and back, as well as to have a separately taken current value in order to change it.

[0,1,2,3,4,5,6,7,8,9]
|
[0,1,2]3[4,5,6,7,8,9]


This shows that the zipper can be represented as a current element, a list of subsequent values ​​and a list of previous ones. Then, to go to element 4, we simply add 3 to the list of previous ones, and in the list of subsequent ones we will “tear off” this 4, and to go to element 2, the opposite is true. Since it is easier to add and cut off a list from the head, it is more convenient to expand the list of previous elements (so in this case, 2 will be in front of the list). Replacing the current item is trivial.

[1,2]3[4,5,6,7,8,9]
|->
[1,2,3]4[5,6,7,8,9]
|
[1,2,3]7[5,6,7,8,9]


To get a zipper for the list, you can take its head as the initial element, and the tail as the subsequent elements. Well, to get the corresponding list for the zipper, the list of previous elements (without forgetting to turn it back, of course) must be connected with the current element and the list of the subsequent ones.

To take a derivative, first you need to somehow present the type in a form suitable for its taking.
Let type 0 be a type that has no value, 1 be a type with exactly one value, and so on.
Type A + B can be represented by either a value of type A or a value of type B. the number of all possible values ​​of type A + B will be the sum of all possible values ​​of A and B. In Haskell, this corresponds to the type Either ab .
Type A × B is represented by both types simultaneously. this is a tuple.

A list can either be empty (a simple value corresponds to 1), or it contains a head (an element of the corresponding type) and a tail (the rest of the list). We write this using the above notation:

List A = 1 + A × (List A)


The zipper for the list contains the current item, the list in the front and the list behind:

ZipperList A = A × (List A) × (List A)


Rewrite the type of the list as a normal function, so that it is more familiar to take a derivative:

f(x) = 1 + x*f(x)
zipper = x*f'(x) -- x -


Only in this case, x is not a number, but a type of [list elements], but this does not affect further conversions.
This is followed by the mechanical taking of the derivative, known to everyone since school:

f'(x) = 0 + 1*f(x) + x*f'(x)
f'(x) = f(x) + x*f'(x)


rename f 'to g

g(x) = f(x) + x*g(x)


if you open g (x) on the right side a couple of times

g(x) = f(x) + x*f(x) + x*x*f(x) + x*x*x*g(x)


then you can see that f (x) can be braced out

g(x) = f(x) * (1 + x*g(x))


we introduce an additional function h (x)

h(x) = 1 + x*h(x)


note that h (x) * f (x) = g (x)

h(x)*f(x) = f(x) + x*f(x)*h(x) = f(x) + x*f(x) + x*x*f(x)*h(x) = g(x)
g(x) = f(x)*h(x)


Now look at f (x);)

f(x) = 1 + x*f(x)
h(x) = 1 + x*h(x)


So finally, zipper looks like

zipper = x*f'(x) = x*f(x)*h(x)
Zipper = A × (List A) × (List A)


Those. exactly what we had!
')
To make sure, we will try to find a zipper for a tree and see what happens. The tree can either be empty or have a current element and left / right branches:

Tree A = 1 + A × (Tree A) × (Tree A)
f(x) = 1 + x*f(x)^2
f'(x) = 0 + 1*f(x)^2 + x*2*f(x)*f'(x)
f'(x) = f(x)^2 + f'(x)*(2*x*f(x))
-- f' -> g, f(x)^2 -> T, 2*x*f(x) -> S
g(x) = T + S*g(x) = T + S*T + S*S*g(x) = T + S*T + S*S*T + ... = T * (1 + S*g(x))


History repeats itself, only expressions become more complicated. Similarly, you can make T and eventually we get:

h(x) = 1 + S*h(x) = List S(x)
g(x) = T(x) * (List S(x))

Zipper = A × (Tree A) × (Tree A) × [A × (Tree A) + A × (Tree A)]


It remains to figure out what it all means.
The first A is obviously the value in the current node. The next two (Tree A) are left and right subtrees relative to this node. Knowing them, we can move down the tree - right or left.
If we go to the right, then we take the current values ​​of the subtrees from the right subtree, and in order not to lose the left one, we will write it in the list. But besides this, we must also indicate in the list exactly which path we have chosen (right or left), so there is a sum of identical tuples. If there is the value of the left term, then we have moved to the left, if the right, then to the right. Thus, all information for moving is available.
How do we get back up? To take one step up, you need to know the element in that node and know the missing subtree (we already have one — our current position is the known subtree of the node above). Steps up can be many, so you need to keep the entire list.
If the list contains the Left value (5 × rtree), then we hit the current node by stepping left from the node with value 5, which has a right subtree of rtree; and if the list is Right (7 × ltree), then we have stepped to the right from the node with the left subtree rtree.

Perhaps the code will be easier to understand, I will give it “as is”, you can check it in the interpreter.

data Tree a = Empty | Node a ( Tree a ) ( Tree a ) deriving ( Read , Show )

data TreeZipper a = TreeZipper a ( Tree a ) ( Tree a ) [ Either ( a , Tree a ) ( a , Tree a ) ] deriving ( Read , Show )

zipperFromTree Empty = error "Zipper can't point empty trees"
zipperFromTree ( Node val left right ) = TreeZipper val left right []

zipperToTree ( TreeZipper val left right [] ) = Node val left right
zipperToTree zipper = zipperToTree $ moveBack zipper

moveRight ( TreeZipper _ _ Empty _ ) = error "No way!"
moveRight ( TreeZipper val left ( Node nval nleft nright ) trace ) =
TreeZipper nval nleft nright ( ( Right ( val , left ) ) : trace )

moveLeft ( TreeZipper _ Empty _ _ ) = error "No way!"
moveLeft ( TreeZipper val ( Node nval nleft nright ) right trace ) =
TreeZipper nval nleft nright ( ( Left ( val , right ) ) : trace )

moveBack ( TreeZipper val left right [] ) = error "No way!"
moveBack ( TreeZipper val left right ( ( Right ( rval , rleft ) ) : trace ) ) =
TreeZipper rval rleft ( Node val left right ) trace
moveBack ( TreeZipper val left right ( ( Left ( lval , lright ) ) : trace ) ) =
TreeZipper lval ( Node val left right ) lright trace

getNodeValue ( TreeZipper val _ _ _ ) = val
setNodeValue ( TreeZipper _ left right trace ) = TreeZipper val left right trace

-- , , , 10
ghci > zipperFromTree tree
TreeZipper 1 ( Node 2 Empty Empty ) ( Node 3 ( Node 4 Empty Empty ) Empty ) []
ghci > moveRight it
TreeZipper 3 ( Node 4 Empty Empty ) Empty [ Right ( 1 , Node 2 Empty Empty ) ]
ghci > moveLeft it
TreeZipper 4 Empty Empty [ Left ( 3 , Empty ) , Right ( 1 , Node 2 Empty Empty ) ]
ghci > setNodeValue 10 it
TreeZipper 10 Empty Empty [ Left ( 3 , Empty ) , Right ( 1 , Node 2 Empty Empty ) ]
ghci > zipperToTree it
Node 1 ( Node 2 Empty Empty ) ( Node 3 ( Node 10 Empty Empty ) Empty )

Based on the Regular Type The One-Hole Contexts