Haskell/Zippers

Theseus and the Zipper

The Labyrinth

"Theseus, we have to do something" said Homer, chief marketing officer of Ancient Geeks Inc.. Theseus put the Minotaur action figure™ back onto the shelf and nodded. "Today's children are no longer interested in the ancient myths, they prefer modern heroes like Spiderman or Sponge Bob." Heroes. Theseus knew well how much he had been a hero in the labyrinth back then on Crete. But those "modern heroes" did not even try to appear realistic. What made them so successful? Anyway, if the pending sales problems could not be resolved, the shareholders would certainly arrange a passage over the Styx for Ancient Geeks Inc.

"Heureka! Theseus, I have an idea: we implement your story with the Minotaur as a computer game! What do you say?" Homer was right. There had been several books, epic (and chart breaking) songs, a mandatory movie trilogy and uncountable Theseus & the Minotaur™ gimmicks, but a computer game was missing. "Perfect, then. Now, Theseus, your task is to implement the game".

A true hero, Theseus chose Haskell as the language to implement the company's redeeming product in. Of course, exploring the labyrinth of the Minotaur was to become one of the game's highlights. He pondered: "We have a two-dimensional labyrinth whose corridors can point in many directions. Of course, we can abstract from the detailed lengths and angles: for the purpose of finding the way out, we only need to know how the path forks. To keep things easy, we model the labyrinth as a tree. This way, the two branches of a fork cannot join again when walking deeper and the player cannot go round in circles. But I think there is enough opportunity to get lost; and this way, if the player is patient enough, they can explore the entire labyrinth with the left-hand rule."

data Node a = DeadEnd a
            | Passage a (Node a)
            | Fork    a (Node a) (Node a)

An example labyrinth and its representation as tree.

Theseus made the nodes of the labyrinth carry an extra parameter of type a. Later on, it may hold game relevant information like the coordinates of the spot a node designates, the ambience around it, a list of game items that lie on the floor, or a list of monsters wandering in that section of the labyrinth. We assume that two helper functions

get :: Node a -> a
put :: a -> Node a -> Node a

retrieve and change the value of type a stored in the first argument of every constructor of Node a. Template:Exercises

"Mh, how to represent the player's current position in the labyrinth? The player can explore deeper by choosing left or right branches, like in"

 turnRight :: Node a -> Maybe (Node a)
 turnRight (Fork _ l r) = Just r
 turnRight _            = Nothing

"But replacing the current top of the labyrinth with the corresponding sub-labyrinth this way is not an option, because the player cannot go back then." He pondered. "Ah, we can apply Ariadne's trick with the thread for going back. We simply represent the player's position by the list of branches their thread takes, the labyrinth always remains the same."

data Branch = KeepStraightOn
            | TurnLeft
            | TurnRight
type Thread = [Branch]

Representation of the player's position by Ariadne's thread.

"For example, a thread [TurnRight,KeepStraightOn] means that the player took the right branch at the entrance and then went straight down a Passage to reach its current position. With the thread, the player can now explore the labyrinth by extending or shortening it. For instance, the function turnRight extends the thread by appending the TurnRight to it."

turnRight :: Thread -> Thread
turnRight t = t ++ [TurnRight]

"To access the extra data, i.e. the game relevant items and such, we simply follow the thread into the labyrinth."

retrieve :: Thread -> Node a -> a
retrieve []                  n             = get n
retrieve (KeepStraightOn:bs) (Passage _ n) = retrieve bs n
retrieve (TurnLeft      :bs) (Fork _ l r)  = retrieve bs l
retrieve (TurnRight     :bs) (Fork _ l r)  = retrieve bs r

Theseus' satisfaction over this solution did not last long. "Unfortunately, if we want to extend the path or go back a step, we have to change the last element of the list. We could store the list in reverse, but even then, we have to follow the thread again and again to access the data in the labyrinth at the player's position. Both actions take time proportional to the length of the thread and for large labyrinths, this will be too long. Isn't there another way?"

Ariadne's Zipper

While Theseus was a skillful warrior, he did not train much in the art of programming and could not find a satisfying solution. After intense but fruitless cogitation, he decided to call his former love Ariadne to ask her for advice. After all, it was she who had the idea with the thread.
Template:Haskell speaker 2
Our hero immediately recognized the voice.
"Hello Ariadne, it's Theseus."
An uneasy silence paused the conversation. Theseus remembered well that he had abandoned her on the island of Naxos and knew that she would not appreciate his call. But Ancient Geeks Inc. was on the road to Hades and he had no choice.
"Uhm, darling, ... how are you?"
Ariadne retorted an icy response, Template:Haskell speaker 2
"Well, I uhm ... I need some help with a programming problem. I'm programming a new Theseus & the Minotaur™ computer game."
She jeered, Template:Haskell speaker 2
"Ariadne, please, I beg of you, Ancient Geeks Inc. is on the brink of insolvency. The game is our last hope!"
After a pause, she came to a decision.
Template:Haskell speaker 2
Theseus turned pale. But what could he do? The situation was desperate enough, so he agreed but only after negotiating Ariadne's share to a tenth.

After Theseus told Ariadne of the labyrinth representation he had in mind, she could immediately give advice,
Template:Haskell speaker 2
"Huh? What does the problem have to do with my fly?"
Template:Haskell speaker 2
"Ah."
Template:Haskell speaker 2
"I know for myself that I want fast updates, but how do I code it?"
Template:Haskell speaker 2
"But then, the problem is how to go back, because all those sub-labyrinths get lost that the player did not choose to branch into."
Template:Haskell speaker 2
Ariadne savored Theseus' puzzlement but quickly continued before he could complain that he already used Ariadne's thread,
Template:Haskell speaker 2

type Zipper a = (Thread a, Node a)

The zipper is a pair of Ariadne's thread and the current sub-labyrinth that the player stands on top. The main thread is colored red and has sub-labyrinths attached to it, such that the whole labyrinth can be reconstructed from the pair.

Theseus didn't say anything.
Template:Haskell speaker 2

data Branch a  = KeepStraightOn a
               | TurnLeft  a (Node a)
               | TurnRight a (Node a)
type Thread a  = [Branch a]

Template:Haskell speaker 2
Theseus interrupts, "Wait, how would I implement this behavior as a function turnRight? And what about the first argument of type a for TurnRight? Ah, I see. We not only need to glue the branch that would get lost, but also the extra data of the Fork because it would otherwise get lost as well. So, we can generate a new branch by a preliminary"

branchRight (Fork x l r) = TurnRight x l

"Now, we have to somehow extend the existing thread with it."
Template:Haskell speaker 2
"Aha, this makes extending and going back take only constant time, not time proportional to the length as in my previous version. So the final version of turnRight is"

turnRight :: Zipper a -> Maybe (Zipper a)
turnRight (t, Fork x l r) = Just (TurnRight x l : t, r)
turnRight _               = Nothing

Taking the right subtree from the entrance. Of course, the thread is initially empty. Note that the thread runs backwards, i.e. the topmost segment is the most recent.

"That was not too difficult. So let's continue with keepStraightOn for going down a passage. This is even easier than choosing a branch as we only need to keep the extra data:"

keepStraightOn :: Zipper a -> Maybe (Zipper a)
keepStraightOn (t, Passage x n) = Just (KeepStraightOn x : t, n)
keepStraightOn _                = Nothing

Now going down a passage.

Pleased, he continued, "But the interesting part is to go back, of course. Let's see..."

back :: Zipper a -> Maybe (Zipper a)
back ([]                   , _) = Nothing
back (KeepStraightOn x : t , n) = Just (t, Passage x n)
back (TurnLeft  x r    : t , l) = Just (t, Fork x l r)
back (TurnRight x l    : t , r) = Just (t, Fork x l r)

"If the thread is empty, we're already at the entrance of the labyrinth and cannot go back. In all other cases, we have to wind up the thread. And thanks to the attachments to the thread, we can actually reconstruct the sub-labyrinth we came from."
Ariadne remarked, Template:Haskell speaker 2

Heureka! That was the solution Theseus sought and Ancient Geeks Inc. should prevail, even if partially sold to Ariadne Consulting. But one question remained:
"Why is it called zipper?"
Template:Haskell speaker 2
"'Ariadne's pearl necklace'," he articulated disdainfully. "As if your thread was any help back then on Crete."
Template:Haskell speaker 2 she replied.
"Bah, I need no thread," he defied the fact that he actually did need the thread to program the game.
Much to his surprise, she agreed, Template:Haskell speaker 2

Grab the focus with your finger, lift it in the air and the hanging branches will form new tree with your finger at the top, ready to be structured by an algebraic data type.

"Ah." He didn't need Ariadne's thread but he needed Ariadne to tell him? That was too much.
"Thank you, Ariadne, good bye."
She did not hide her smirk as he could not see it anyway through the phone.

Half a year later, Theseus stopped in front of a shop window, defying the cold rain that tried to creep under his buttoned up anorak. Blinking letters announced

"Spider-Man: lost in the Web"

- find your way through the labyrinth of threads -
the great computer game by Ancient Geeks Inc.

He cursed the day when he called Ariadne and sold her a part of the company. Was it she who contrived the unfriendly takeover by WineOS Corp., led by Ariadne's husband Dionysus? Theseus watched the raindrops finding their way down the glass window. After the production line was changed, nobody would produce Theseus and the Minotaur™ merchandise anymore. He sighed. His time, the time of heroes, was over. Now came the super-heroes.

Differentiation of data types

The previous section has presented the zipper, a way to augment a tree-like data structure Node a with a finger that can focus on the different subtrees. While we constructed a zipper for a particular data structure Node a, the construction can be easily adapted to different tree data structures by hand. Template:Exercises

Mechanical Differentiation

But there is also an entirely mechanical way to derive the zipper of any (suitably regular) data type. Surprisingly, 'derive' is to be taken literally, for the zipper can be obtained by the derivative of the data type, a discovery first described by Conor McBride. The subsequent section is going to explicate this truly wonderful mathematical gem.

For a systematic construction, we need to calculate with types. The basics of structural calculations with types are outlined in a separate chapter [[../Generic Programming/]] and we will heavily rely on this material.

Let's look at some examples to see what their zippers have in common and how they hint differentiation. The type of binary tree is the fixed point of the recursive equation

$𝑇𝑟𝑒𝑒2=1+𝑇𝑟𝑒𝑒2\times 𝑇𝑟𝑒𝑒2$.

When walking down the tree, we iteratively choose to enter the left or the right subtree and then glue the not-entered subtree to Ariadne's thread. Thus, the branches of our thread have the type

$𝐵𝑟𝑎𝑛𝑐ℎ2=𝑇𝑟𝑒𝑒2+𝑇𝑟𝑒𝑒2\cong 2\times 𝑇𝑟𝑒𝑒2$.

Similarly, the thread for a ternary tree

$𝑇𝑟𝑒𝑒3=1+𝑇𝑟𝑒𝑒3\times 𝑇𝑟𝑒𝑒3\times 𝑇𝑟𝑒𝑒3$

has branches of type

$𝐵𝑟𝑎𝑛𝑐ℎ3=3\times 𝑇𝑟𝑒𝑒3\times 𝑇𝑟𝑒𝑒3$

because at every step, we can choose between three subtrees and have to store the two subtrees we don't enter. Isn't this strikingly similar to the derivatives $\frac{d}{dx}{x}^2=2\times x$ and $\frac{d}{dx}{x}^3=3\times x^2$?

The key to the mystery is the notion of the one-hole context of a data structure. Imagine a data structure parameterised over a type $X$, like the type of trees $𝑇𝑟𝑒𝑒X$. If we were to remove one of the items of this type $X$ from the structure and somehow mark the now empty position, we obtain a structure with a marked hole. The result is called "one-hole context" and inserting an item of type $X$ into the hole gives back a completely filled $𝑇𝑟𝑒𝑒X$. The hole acts as a distinguished position, a focus. The figures illustrate this.

Removing a value of type $X$ from a $𝑇𝑟𝑒𝑒X$ leaves a hole at that position.

A more abstract illustration of plugging $X$ into a one-hole context.

Of course, we are interested in the type to give to a one-hole context, i.e. how to represent it in Haskell. The problem is how to efficiently mark the focus. But as we will see, finding a representation for one-hole contexts by induction on the structure of the type we want to take the one-hole context of automatically leads to an efficient data type. So, given a data structure $FX$ with a functor $F$ and an argument type $X$, we want to calculate the type $\partial FX$ of one-hole contexts from the structure of $F$. As our choice of notation $\partial F$ already reveals, the rules for constructing one-hole contexts of sums, products and compositions are exactly Leibniz' rules for differentiation.

One-hole context		Illustration
$(\partial 𝐶𝑜𝑛𝑠{𝑡}_{𝐴})X$	$=0$	There is no $X$ in $A=𝐶𝑜𝑛𝑠{𝑡}_{𝐴}X$, so the type of its one-hole contexts must be empty.
$(\partial 𝐼𝑑)X$	$=1$	There is only one position for items $X$ in $X=𝐼𝑑X$. Removing one $X$ leaves no $X$ in the result. And as there is only one position we can remove it from, there is exactly one one-hole context for $𝐼𝑑X$. Thus, the type of one-hole contexts is the singleton type.
$\partial (F+G)$	$=\partial F+\partial G$	As an element of type $F+G$ is either of type $F$ or of type $G$, a one-hole context is also either $\partial F$ or $\partial G$.
$\partial (F\times G)$	$=F\times \partial G+\partial F\times G$	The hole in a one-hole context of a pair is either in the first or in the second component.
$\partial (F\circ G)$	$=(\partial F\circ G)\times \partial G$	Chain rule. The hole in a composition arises by making a hole in the enclosing structure and fitting the enclosed structure in.

Of course, the function plug that fills a hole has the type $(\partial FX)\times X\to FX$.

So far, the syntax $\partial$ denotes the differentiation of functors, i.e. of a kind of type functions with one argument. But there is also a handy expression oriented notation ${\partial }_X$ slightly more suitable for calculation. The subscript indicates the variable with respect to which we want to differentiate. In general, we have

$(\partial F)X={\partial }_X(FX)$

An example is

$\partial (𝐼𝑑\times 𝐼𝑑)X={\partial }_X(X\times X)=1\times X+X\times 1\cong 2\times X$

Of course, ${\partial }_X$ is just point-wise whereas $\partial$ is point-free style. Template:Exercises

Zippers via Differentiation

The above rules enable us to construct zippers for recursive data types $\mu F:=\mu X.FX$ where $F$ is a polynomial functor. A zipper is a focus on a particular subtree, i.e. substructure of type $\mu F$ inside a large tree of the same type. As in the previous chapter, it can be represented by the subtree we want to focus at and the thread, that is the context in which the subtree resides

${𝑍𝑖𝑝𝑝𝑒𝑟}_F=\mu F\times {𝐶𝑜𝑛𝑡𝑒𝑥𝑡}_F$.

Now, the context is a series of steps each of which chooses a particular subtree $\mu F$ among those in $F\mu F$. Thus, the unchosen subtrees are collected together by the one-hole context $\partial F(\mu F)$. The hole of this context comes from removing the subtree we've chosen to enter. Putting things together, we have

${𝐶𝑜𝑛𝑡𝑒𝑥𝑡}_F=𝐿𝑖𝑠𝑡(\partial F(\mu F))$.

or equivalently

${𝐶𝑜𝑛𝑡𝑒𝑥𝑡}_F=1+\partial F(\mu F)\times {𝐶𝑜𝑛𝑡𝑒𝑥𝑡}_F$.

To illustrate how a concrete calculation proceeds, let's systematically construct the zipper for our labyrinth data type

data Node a = DeadEnd a
            | Passage a (Node a)
            | Fork a (Node a) (Node a)

This recursive type is the fixed point

$𝑁𝑜𝑑𝑒A=\mu X.{𝑁𝑜𝑑𝑒𝐹}_{A}X$

of the functor

${𝑁𝑜𝑑𝑒𝐹}_{A}X=A+A\times X+A\times X\times X$.

In other words, we have

$𝑁𝑜𝑑𝑒A\cong {𝑁𝑜𝑑𝑒𝐹}_A(𝑁𝑜𝑑𝑒A)\cong A+A\times 𝑁𝑜𝑑𝑒A+A\times 𝑁𝑜𝑑𝑒A\times 𝑁𝑜𝑑𝑒A$.

The derivative reads

${\partial }_X({𝑁𝑜𝑑𝑒𝐹}_{A}X)\cong A+2\times A\times X$

and we get

$\partial {𝑁𝑜𝑑𝑒𝐹}_A(𝑁𝑜𝑑𝑒A)\cong A+2\times A\times 𝑁𝑜𝑑𝑒A$.

Thus, the context reads

${𝐶𝑜𝑛𝑡𝑒𝑥𝑡}_{𝑁𝑜𝑑𝑒𝐹}\cong 𝐿𝑖𝑠𝑡(\partial {𝑁𝑜𝑑𝑒𝐹}_A(𝑁𝑜𝑑𝑒A))\cong 𝐿𝑖𝑠𝑡(A+2\times A\times (𝑁𝑜𝑑𝑒A))$.

Comparing with

data Branch a  = KeepStraightOn a
               | TurnLeft  a (Node a)
               | TurnRight a (Node a)
type Thread a  = [Branch a]

we see that both are exactly the same as expected! Template:Exercises

Differentiation of Fixed Point

There is more to data types than sums and products, we also have a fixed point operator with no direct correspondence in calculus. Consequently, the table is missing a rule of differentiation, namely how to differentiate fixed points $\mu FX=\mu Y.FXY$:

${\partial }_X(\mu FX)=?$.

As its formulation involves the chain rule in two variables, we delegate it to the exercises. Instead, we will calculate it for our concrete example type $𝑁𝑜𝑑𝑒A$:

$\begin{array}{ccc}{\partial }_A(𝑁𝑜𝑑𝑒A)& =& {\partial }_A(A+A\times 𝑁𝑜𝑑𝑒A+A\times 𝑁𝑜𝑑𝑒A\times 𝑁𝑜𝑑𝑒A)\\ & \cong & 1+𝑁𝑜𝑑𝑒A+𝑁𝑜𝑑𝑒A\times 𝑁𝑜𝑑𝑒A\\ & & +{\partial }_A(𝑁𝑜𝑑𝑒A)\times (A+2\times A\times 𝑁𝑜𝑑𝑒A).\end{array}$

Of course, expanding ${\partial }_A(𝑁𝑜𝑑𝑒A)$ further is of no use, but we can see this as a fixed point equation and arrive at

${\partial }_A(𝑁𝑜𝑑𝑒A)=\mu X.TA+SA\times X$

with the abbreviations

$TA=1+𝑁𝑜𝑑𝑒A+𝑁𝑜𝑑𝑒A\times 𝑁𝑜𝑑𝑒A$

and

$SA=A+2\times A\times 𝑁𝑜𝑑𝑒A$.

The recursive type is like a list with element types $SA$, only that the empty list is replaced by a base case of type $TA$. But given that the list is finite, we can replace the base case with $1$ and pull $TA$ out of the list:

${\partial }_A(𝑁𝑜𝑑𝑒A)\cong TA\times (\mu X.1+SA\times X)=TA\times 𝐿𝑖𝑠𝑡(SA)$.

Comparing with the zipper we derived in the last paragraph, we see that the list type is our context

$𝐿𝑖𝑠𝑡(SA)\cong {𝐶𝑜𝑛𝑡𝑒𝑥𝑡}_{𝑁𝑜𝑑𝑒𝐹}$

and that

$A\times TA\cong 𝑁𝑜𝑑𝑒A$.

In the end, we have

${𝑍𝑖𝑝𝑝𝑒𝑟}_{𝑁𝑜𝑑𝑒𝐹}\cong {\partial }_A(𝑁𝑜𝑑𝑒A)\times A$.

Thus, differentiating our concrete example $𝑁𝑜𝑑𝑒A$ with respect to $A$ yields the zipper up to an $A$! Template:Exercises

Differentation with respect to functions of the argument

When finding the type of a one-hole context one does d f(x)/d x. It is entirely possible to solve expressions like d f(x)/d g(x). For example, solving d x^4 / d x^2 gives 2x^2 , a two-hole context of a 4-tuple. The derivation is as follows let u=x^2 d x^4 / d x^2 = d u^2 /d u = 2u = 2 x^2 .

Zippers vs Contexts

In general however, zippers and one-hole contexts denote different things. The zipper is a focus on arbitrary subtrees whereas a one-hole context can only focus on the argument of a type constructor. Take for example the data type

 data Tree a = Leaf a | Bin (Tree a) (Tree a)

which is the fixed point

$𝑇𝑟𝑒𝑒A=\mu X.A+X\times X$.

The zipper can focus on subtrees whose top is Bin or Leaf but the hole of one-hole context of $𝑇𝑟𝑒𝑒A$ may only focus a Leafs because this is where the items of type $A$ reside. The derivative of $𝑁𝑜𝑑𝑒A$ only turned out to be the zipper because every top of a subtree is always decorated with an $A$. Template:Exercises

Conclusion

We close this section by asking how it may happen that rules from calculus appear in a discrete setting. Currently, nobody knows. But at least, there is a discrete notion of linear, namely in the sense of "exactly once". The key feature of the function that plugs an item of type $X$ into the hole of a one-hole context is the fact that the item is used exactly once, i.e. linearly. We may think of the plugging map as having type

${\partial }_{X}FX\to (X⊸FX)$

where $A⊸B$ denotes a linear function, one that does not duplicate or ignore its argument, as in linear logic. In a sense, the one-hole context is a representation of the function space $X⊸FX$, which can be thought of being a linear approximation to $X\to FX$.

See also

• Zipper on the haskell.org wiki
• Generic Zipper and its applications
• Zipper-based file server/OS
• Scrap Your Zippers: A Generic Zipper for Heterogeneous Types