The Essence of a Zipper

The essence of a zipper is a “one-hole context” – the context of a value in some structure, together with that value – and a means of moving from one one-hole context to another. What do we mean by a one-hole context? That structure you obtain by pulling out a single element in a structure, and replacing it with a “hole”, a placeholder. A variable, if you like. For example, in the algebraic expression ax² + bx + c the one-hole context of c is ax² + bx + _. A zipper thus represents a focus on some part of a data structure.

Implementing Huet’s zipper means that we construct:

1. the set of possible one-hole context types ^[1],
2. define traversals through the structure,
3. and record the series of actions we took to arrive at this particular element in the structure.

We can easily store the how-we-got-here state by having the contexts be a recursive type: each context stores a reference to the previous context of the zipper (and we can mark the first context with some marker type).

Oleg Kiselyov and Chung-Chieh Shan show another way of deriving a zipper. Instead of type differentiating the structure,

1. define a traversal function on the structure,
2. define a map on that traversal,
3. “derive” the traversal through the use of partial continuations.

In particular, we see that Huet’s zipper is essentially a per-type manual reification of the Kiselyov-Shan zipper: instead of keeping the how-did-we-get-here information in the recursive context type, we can keep that information on the stack, in the form of partial continuations. Each continuation forms a one-hole context into which we can plug a value. The act of plugging in a value returns us a new (one-hole context, current value) pair, into which we can plug our next value.

The really nice thing about the Kiselyov-Shan zipper is that the zipper and traversal have no knowledge about the other, allowing each to vary independently.

I found it much harder to implement the Kiselyov-Shan zipper for a few reasons. I had to write my own control operator, and partial continuations are tricky to get right: I had to remember when debugging not only where I was but how I got there in any piece of code. My debugging ability was greatly reduced by the fact that I was manipulating the stack directly and thus couldn’t rely on the stack to remind me how I ended up at a particular piece of code. Bad Things can happen. I often had to force-kill my image because I’d made the wrong move in my self-brain surgery: an over-eager capture of a continuation can cause serious disruption.

Implementing a Huet-style zipper, in contrast, was a lot more manual labour, but the process felt almost automatic. Which is a hint: I could probably automate or generate a large part of implementing the zipper.

[1] See Conor McBride’s “The Derivative of a Type is the Type of its One Hole Context“.