Zipper - Derived from Type

    Zipper is a data type representation method that allows you to walk through the structure and change individual elements, despite the functional purity. For example, if we can only go forward through the list, doing something with the elements, then with the zipper we can “stay” in a certain element, move forward and backward and change the current element.
    Interestingly, a zipper for a certain type can be obtained by literally taking its derivative.

    First, let's try to come up with a zipper for a list without math.
    We need the ability to go forward and backward through the list, as well as have a separate current value 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 the 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 “tear off” this 4 from the list of subsequent ones, and vice versa to go to element 2. Since adding and cutting off the list is easier from the head, it is more convenient to expand the list of previous elements (so in this case the 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 the zipper for the list, you can take its head as the initial element, and the tail as the next elements. Well, in order to get the appropriate list for the zipper, the list of previous elements (without forgetting to expand it back, of course) must be connected to the current element and the list of subsequent ones.

    To take a derivative, first you need to somehow imagine the type in a form suitable for its taking.
    Let type 0 be a type without any value, 1 be a type with exactly one value, etc.
    Type A + B can be represented either by a value of type A, or by 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 a b.
    Type A × B is represented by values ​​of both types at the same time, i.e. this is a tuple.

    The list can be either 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 front and the list behind:
    ZipperList A = A × (List A) × (List A)
    We rewrite the list type in the form of a regular function, so that it is more familiar to take the derivative:
    f(x) = 1 + x*f(x)
    zipper = x*f'(x) -- x - текущий элемент
    Only in this case, x is not a number, but the type of [list items], but this does not affect further transformations.
    The following is a mechanical capture 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) a couple of times on the right side
    g(x) = f(x) + x*f(x) + x*x*f(x) + x*x*x*g(x)
    then we can see that f (x) can be put out of brackets
    g(x) = f(x) * (1 + x*g(x))
    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)
    Thus, finally zipper has the form
    zipper = x*f'(x) = x*f(x)*h(x)
    Zipper = A × (List A) × (List A)
    Those. exactly what we had!

    To make sure, try to find a zipper for the tree and figure out what happens. The tree can be either empty or have the 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, we can take out T and finally 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 be understood what this all means.
    The first A is obviously the value at the current node. The next two (Tree A) - left and right subtrees relative to this node. Knowing them, we can move down the tree - to the 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 to the list. But besides this, it is also necessary to indicate in the list which path we have chosen (to the right or to the left), therefore there is a sum of identical tuples. If the value of the left term is there, then we have moved to the left, if the right is to the right. Thus, all the 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 (one we already have - our current position is the known subtree of the node above). There can be many steps up, so you need to keep the entire list.
    If the value of Left is in the head of the list (5 × rtree), then we got to the current node by stepping to the left from a node with a value of 5, whose right subtree has rtree; and if Right (7 × ltree) is in the list, then we stepped right from the node with the left rtree subtree.

    Perhaps the code will be easier to understand, I will bring 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 Derivative of a Regular Type is its Type of One-Hole Contexts

    Also popular now: