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.

Exercises
Implement get and put. One case for get is get (Passage x _) = x. To get a concrete example, write down the labyrinth shown in the picture as a value of type Node (Int,Int). The extra parameter (Int,Int) holds the cartesian coordinates of a node.

"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

Exercises
Write a function update that applies a function of type a -> a to the extra data at the player's position.

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.
"Ariadne Consulting. What can I do for you?"
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, "Mr. Theseus, the times of darling are long over. What do you want?"
"Well, I uhm ... I need some help with a programming problem. I'm programming a new Theseus & the Minotaur™ computer game."
She jeered, "Yet another artifact to glorify your 'heroic being'? And you want me of all people to help you?"
"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.
"Fine, I will help you. But only if you transfer a substantial part of Ancient Geeks Inc. to me. Let's say thirty percent."
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,
"You need a zipper."
"Huh? What does the problem have to do with my fly?"
"Nothing, it's a data structure first published by Gérard Huet."
"Ah."
"More precisely, it's a purely functional way to augment tree-like data structures like lists or binary trees with a single focus or finger that points to a subtree inside the data structure and allows constant time updates and lookups at the spot it points to. In our case, we want a focus on the player's position."
"I know for myself that I want fast updates, but how do I code it?"
"Don't get impatient, you cannot solve problems by coding, you can only solve them by thinking. The only place where we can get constant time updates in a purely functional data structure is the topmost node. So, the focus necessarily has to be at the top. Currently, the topmost node in your labyrinth is always the entrance, but your previous idea of replacing the labyrinth by one of its sub-labyrinths ensures that the player's position is at the topmost node."
"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."
"Well, you can use my thread in order not to lose the sub-labyrinths."
Ariadne savored Theseus' puzzlement but quickly continued before he could complain that he already used Ariadne's thread,
"The key is to glue the lost sub-labyrinths to the thread so that they actually don't get lost at all. The intention is that the thread and the current sub-labyrinth complement one another to the whole labyrinth. With 'current' sub-labyrinth, I mean the one that the player stands on top of. The zipper simply consists of the thread and the current sub-labyrinth."

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.
"You can also view the thread as a context in which the current sub-labyrinth resides. Now, let's find out how to define Thread a. By the way, Thread has to take the extra parameter a because it now stores sub-labyrinths. The thread is still a simple list of branches, but the branches are different from before."

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

"Most importantly, TurnLeft and TurnRight have a sub-labyrinth glued to them. When the player chooses say to turn right, we extend the thread with a TurnRight and now attach the untaken left branch to it, so that it doesn't get lost."
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."
"Indeed. The second point about the thread is that it is stored backwards. To extend it, you put a new branch in front of the list. To go back, you delete the topmost element."
"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.

Exercises
Write the function turnLeft.

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, "Note that a partial test for correctness is to check that each bound variable like x, l and r on the left hand side appears exactly once at the right hands side as well. So, when walking up and down a zipper, we only redistribute data between the thread and the current sub-labyrinth."

Exercises

Now that we can navigate the zipper, code the functions get, put and update that operate on the extra data at the player's position. Zippers are by no means limited to the concrete example Node a, they can be constructed for all tree-like data types. Go on and construct a zipper for binary trees data Tree a = Leaf a | Bin (Tree a) (Tree a) Start by thinking about the possible branches Branch a that a thread can take. What do you have to glue to the thread when exploring the tree? Simple lists have a zipper as well. data List a = Empty | Cons a (List a) What does it look like? Write a complete game based on Theseus' labyrinth.

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?"
"Well, I would have called it 'Ariadne's pearl necklace'. But most likely, it's called zipper because the thread is in analogy to the open part and the sub-labyrinth is like the closed part of a zipper. Moving around in the data structure is analogous to zipping or unzipping the zipper."
"'Ariadne's pearl necklace'," he articulated disdainfully. "As if your thread was any help back then on Crete."
"As if the idea with the thread were yours," 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, "Well, indeed you don't need a thread. Another view is to literally grab the tree at the focus with your finger and lift it up in the air. The focus will be at the top and all other branches of the tree hang down. You only have to assign the resulting tree a suitable algebraic data type, most likely that of the zipper."

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.

Exercises
Take a list, fix one element in the middle with your finger and lift the list into the air. What type can you give to the resulting tree?

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.

Exercises
Start with a ternary tree data Tree a = Leaf a | Node (Tree a) (Tree a) (Tree a) and derive the corresponding Thread a and Zipper a.

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

${\mathit {Tree2}}=1+{\mathit {Tree2}}\times {\mathit {Tree2}}$.

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

${\mathit {Branch2}}={\mathit {Tree2}}+{\mathit {Tree2}}\cong 2\times {\mathit {Tree2}}$.

Similarly, the thread for a ternary tree

${\mathit {Tree3}}=1+{\mathit {Tree3}}\times {\mathit {Tree3}}\times {\mathit {Tree3}}$

has branches of type

${\mathit {Branch3}}=3\times {\mathit {Tree3}}\times {\mathit {Tree3}}$

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 ${\mathit {Tree}}\,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 ${\mathit {Tree}}\,X$. The hole acts as a distinguished position, a focus. The figures illustrate this.

Removing a value of type $X$ from a ${\mathit {Tree}}\,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 $F\,X$ with a functor $F$ and an argument type $X$, we want to calculate the type $\partial F\,X$ 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 {\mathit {Const_{A}}})\,X$	$=\,0$	There is no $X$ in $A={\mathit {Const_{A}}}\,X$, so the type of its one-hole contexts must be empty.
$(\partial {\mathit {Id}})\,X$	$=\,1$	There is only one position for items $X$ in $X={\mathit {Id}}\,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 ${\mathit {Id}}\,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 F\,X)\times X\to F\,X$.

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}(F\,X)$

An example is

$\partial ({\mathit {Id}}\times {\mathit {Id}})\,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.

Exercises

Rewrite some rules in point-wise style. For example, the left hand side of the product rule becomes $\partial _{X}(F\,X\times G\,X)=\dots$. To get familiar with one-hole contexts, differentiate the product $X^{n}:=X\times X\times \dots \times X$ of exactly $n$ factors formally and convince yourself that the result is indeed the corresponding one-hole context. Of course, one-hole contexts are useless if we cannot plug values of type $X$ back into them. Write the plug functions corresponding to the five rules. Formulate the chain rule for two variables and prove that it yields one-hole contexts. You can do this by viewing a bifunctor $F\,X\,Y$ as an normal functor in the pair $(X,Y)$. Of course, you may need a handy notation for partial derivatives of bifunctors in point-free style.

Zippers via Differentiation

The above rules enable us to construct zippers for recursive data types $\mu F:=\mu X.\,F\,X$ 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

${\mathit {Zipper}}_{F}=\mu F\times {\mathit {Context}}_{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

${\mathit {Context}}_{F}={\mathit {List}}\,(\partial F\,(\mu F))$.

or equivalently

${\mathit {Context}}_{F}=1+\partial F\,(\mu F)\times {\mathit {Context}}_{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

${\mathit {Node}}\,A=\mu X.\,{\mathit {NodeF}}_{A}\,X$

of the functor

${\mathit {NodeF}}_{A}\,X=A+A\times X+A\times X\times X$.

In other words, we have

${\mathit {Node}}\,A\cong {\mathit {NodeF}}_{A}\,({\mathit {Node}}\,A)\cong A+A\times {\mathit {Node}}\,A+A\times {\mathit {Node}}\,A\times {\mathit {Node}}\,A$.

The derivative reads

$\partial _{X}({\mathit {NodeF}}_{A}\,X)\cong A+2\times A\times X$

and we get

$\partial {\mathit {NodeF}}_{A}\,({\mathit {Node}}\,A)\cong A+2\times A\times {\mathit {Node}}\,A$.

Thus, the context reads

${\mathit {Context}}_{\mathit {NodeF}}\cong {\mathit {List}}\,(\partial {\mathit {NodeF}}_{A}\,({\mathit {Node}}\,A))\cong {\mathit {List}}\,(A+2\times A\times ({\mathit {Node}}\,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!

Exercises
Redo the zipper for a ternary tree, but with differentiation this time. Construct the zipper for a list. Rhetorical question concerning the previous exercise: what's the difference between a list and a stack?

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 F\,X=\mu Y.\,F\,X\,Y$:

$\partial _{X}(\mu F\,X)={?}$.

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 ${\mathit {Node}}\,A$:

${\begin{matrix}\partial _{A}({\mathit {Node}}\,A)&=&\partial _{A}(A+A\times {\mathit {Node}}\,A+A\times {\mathit {Node}}\,A\times {\mathit {Node}}\,A)\\&\cong &1+{\mathit {Node}}\,A+{\mathit {Node}}\,A\times {\mathit {Node}}\,A\\&&+\partial _{A}({\mathit {Node}}\,A)\times (A+2\times A\times {\mathit {Node}}\,A).\end{matrix}}$

Of course, expanding $\partial _{A}({\mathit {Node}}\,A)$ further is of no use, but we can see this as a fixed point equation and arrive at

$\partial _{A}({\mathit {Node}}\,A)=\mu X.\,T\,A+S\,A\times X$

with the abbreviations

$T\,A=1+{\mathit {Node}}\,A+{\mathit {Node}}\,A\times {\mathit {Node}}\,A$

and

$S\,A=A+2\times A\times {\mathit {Node}}\,A$.

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

$\partial _{A}({\mathit {Node}}\,A)\cong T\,A\times (\mu X.\,1+S\,A\times X)=T\,A\times {\mathit {List}}\,(S\,A)$.

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

${\mathit {List}}\,(S\,A)\cong {\mathit {Context}}_{\mathit {NodeF}}$

and that

$A\times T\,A\cong {\mathit {Node}}\,A$.

In the end, we have

${\mathit {Zipper}}_{\mathit {NodeF}}\cong \partial _{A}({\mathit {Node}}\,A)\times A$.

Thus, differentiating our concrete example ${\mathit {Node}}\,A$ with respect to $A$ yields the zipper up to an $A$!

Exercises
Use the chain rule in two variables to formulate a rule for the differentiation of a fixed point. Maybe you know that there are inductive ($\mu$) and coinductive fixed points ($\nu$). What's the rule for coinductive fixed points?

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

${\mathit {Tree}}\,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 ${\mathit {Tree}}\,A$ may only focus a Leafs because this is where the items of type $A$ reside. The derivative of ${\mathit {Node}}\,A$ only turned out to be the zipper because every top of a subtree is always decorated with an $A$.

Exercises

Surprisingly, $\partial _{A}({\mathit {Tree}}\,A)\times A$ and the zipper for ${\mathit {Tree}}\,A$ again turn out to be the same type. Doing the calculation is not difficult but can you give a reason why this has to be the case? Prove that the zipper construction for $\mu F$ can be obtained by introducing an auxiliary variable $Y$, differentiating $\mu X.\,Y\times F\,X$ with respect to it and re-substituting $Y=1$. Why does this work? Find a type $G\,A$ whose zipper is different from the one-hole context.

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}F\,X\to (X\multimap F\,X)$

where $A\multimap 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\multimap F\,X$, which can be thought of being a linear approximation to $X\to F\,X$.

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