Zipper (data structure)

Many common data structures in computer science can be expressed as the structure generated by a few primitive constructor operations or observer operations. These include the structure of finite lists, which can be generated by two operations:

• Empty constructs an empty list,
• Cons(x, L) constructs a list by prepending or concatenating value x in front of list L.

A list such as [1, 2, 3] is therefore the declaration Cons(1, Cons(2, Cons(3, Empty))). It is possible to describe the location in such a list as the number of steps from the front of the list to the target location. More formally, a location in the list is the number of Cons operations required to reconstruct the whole list from that particular location. For example, in Cons(1, Cons(2, Cons( X, Cons(4, Empty)))) a Cons(2, L) and a Cons(1, L) operation would be required to reconstruct the list relative to position X otherwise known as Cons( X, Cons(4, Empty)). This recording together with the location is called a zipped representation of the list or a list-zipper.

To be clear, a location in the list is not just the number of Cons operations, but also all of the other information about those Cons; in this case, the values that must be reconnected. Here, these values may be conveniently represented in a separate list in the order of application from the target location. Specifically, from the context of "3" in the list [1, 2, 3, 4], a recording (commonly referred to as a 'path') could be represented as [2, 1] where Cons(2, L) is applied followed by (Cons 1, L) to reconstitute the original list starting from [X, 4].

A list-zipper always represents the entire data structure. However, this information is from the perspective of a specific location within that data structure. Consequently, a list-zipper is a pair consisting of both the location as a context or starting point, and a recording or path that permits reconstruction from that starting location. In particular, the list-zipper of [1, 2, 3, 4] at the location of "3" may be represented as ([2, 1], [3, 4]). Now, if "3" is changed to "10", then the list-zipper becomes ([2, 1], [10, 4]). The list may then be efficiently reconstructed: [1, 2, 10, 4] or other locations traversed to.

With the list represented this way, it is easy to define relatively efficient operations on immutable data structures such as Lists and Trees at arbitrary locations. In particular, applying the zipper transform to a tree makes it is easy to insert or remove values at any particular location in the tree.

The type of a zipper's contexts can be constructed via a transformation of the original type that is closely related to the derivative of calculus through decategorification. The recursive types that zippers are formed from can be viewed as the least fixed point of a unary type constructor of kind ${\displaystyle *\rightarrow *}$. For example, with a higher-order type constructor ${\displaystyle lfp:(*\rightarrow *)\rightarrow *}$ that constructs the least fixed point of its argument, an unlabeled binary tree can be represented as ${\displaystyle lfp(T\mapsto T^{2}+1)}$ and an unlabeled list may take the form ${\displaystyle lfp(T\mapsto T+1)}$. Here, the notation of exponentiation, multiplication, and addition correspond to function types, product types, and sum types respectively, whilst the natural numbers label the finite types; in this way, the type constructors resemble polynomial functions in ${\displaystyle \mathbb {N} \rightarrow \mathbb {N} }$.[2]

The derivative of a type constructor can therefore be formed through this syntactic analogy: for the example of an unlabeled ternary tree, the derivative of its type constructor ${\displaystyle (T\mapsto T^{3}+1)'}$ would be equivalent to ${\displaystyle T\mapsto 3\times T^{2}}$, analogously to the use of the sum and power rules in differential calculus. The type of the contexts of a zipper over an original type ${\displaystyle lfp(f)}$ is equivalent to the derivative of the type constructor applied to the original type, ${\displaystyle f'(lfp(f))}$.[3]

For illustration, consider the recursive data structure of a binary tree with nodes that are either sentinel nodes of type ${\displaystyle 1}$ or contain a value of type ${\displaystyle A}$:

${\displaystyle BTree:=lfp(T\mapsto A\times T^{2}+1)}$

The derivative of the type constructor can be computed to be

${\displaystyle (T\mapsto A\times T^{2}+1)'=T\mapsto 2\times A\times T}$

Thus, the type of the zipper's contexts is

${\displaystyle (T\mapsto 2\times A\times T)(BTree)=2\times A\times BTree}$

As such, we find that the context of each non-sentinel child node in the labelled binary tree is a triple consisting of

• a boolean value of type ${\displaystyle 2}$, expressing whether the current node is the left or right child of its parent node;
• a value of type ${\displaystyle A}$, the label of the current node's parent; and
• the node's sibling of type ${\displaystyle BTree}$, the subtree contained by the other branch of the current node's parent.

In general, a zipper for a tree of type ${\displaystyle lfp(f)}$ consists of two parts: a list of contexts of type ${\displaystyle f'(lfp(f))}$ of the current node and each of its ancestors up until the root node, and the subtree of type ${\displaystyle lfp(f)}$ that the current node contains.

The zipper is often used where there is some concept of focus or of moving around in some set of data, since its semantics reflect that of moving around but in a functional non-destructive manner.

The zipper has been used in

• Xmonad, to manage focus and placement of windows
• Huet's papers cover a structural editor[4] based on zippers and a theorem prover
• A filesystem (ZipperFS) written in Haskell offering "...transactional semantics; undo of any file and directory operation; snapshots; statically guaranteed the strongest, repeatable read, isolation mode for clients; pervasive copy-on-write for files and directories; built-in traversal facility; and just the right behavior for cyclic directory references."[5]
• Clojure has extensive support for zippers.[6]

• Huet, Gerard (September 1997). "Functional Pearl: The Zipper" (PDF). Journal of Functional Programming. 7 (5): 549–554. doi:10.1017/s0956796897002864.
• Hinze, Ralf, et al. "Type-indexed data types". 23 July 2003

The Wikibook Haskell has a page on the topic of: Zippers

• Zipper
• Theseus and the Zipper
• "Roll Your Own Window Manager: Tracking Focus with a Zipper"
• Definition
• "An Applicative Control-Flow Graph Based on Huet's Zipper"
• Infinitesimal Types