Zipper

A zipper represents an immutable data structure together with a focus, a position inside it. It stores the substructure at the focus, and the path from the focus back to the root, together with everything to either side of that path. Moving the focus one step and editing at the focus take constant time, and the old version remains valid, sharing everything off the path with the new one. Huet introduced the zipper in 1997 for editing trees^[1]. The type of a zipper's contexts is the derivative of the structure's type, in the sense of calculus^[2].

§ 01

Overview

An editor for immutable trees has a problem that a mutable one does not: changing a node deep inside means rebuilding every node on the path from it to the root, and finding that node again for the next edit means walking down from the root again. The zipper keeps the path. Walking down from the root, it records at each step which child it took and the parts of the node it did not enter; these records are the context. The focused subtree together with its context is equivalent to the whole tree, and the tree can be rebuilt from them by walking back up.

A binary tree, and the same tree as a zipper focused on 5. The edges on the path from the root to the focus are reversed, so the focus is reached first and the root last; the rest of the tree is unchanged.

Seen this way, a zipper is the tree with the pointers on the path to the focus reversed. The Schorr–Waite graph-marking algorithm walks a structure with the same pointer reversal, performed in place^[6]; the zipper does it persistently, by allocating new path records instead of overwriting pointers.

§ 02

Lists

The simplest zipper is for lists. A position between two elements of a list is determined by the elements before it and the elements after it. Storing the elements before it in reverse, nearest first, makes every operation at the position constant-time:

zipper (A) = list (A) \times list (A) [a_{1}, \dots, a_{i} ∣ a_{i + 1}, \dots, a_{n}] \mapsto ([a_{i}, \dots, a_{1}], [a_{i + 1}, \dots, a_{n}])

A list zipper used as a text buffer with a cursor.

(* A list zipper: the elements before the focus, nearest first, and the
   elements from the focus on. Used here as a text buffer with a cursor. *)
type 'a zipper = { before : 'a list; after : 'a list }
 
let of_list xs = { before = []; after = xs }
let to_list z = List.rev_append z.before z.after
 
let left z = match z.before with x :: b -> { before = b; after = x :: z.after } | [] -> z
let right z = match z.after with x :: a -> { before = x :: z.before; after = a } | [] -> z
let insert x z = { z with before = x :: z.before }
let backspace z = match z.before with _ :: b -> { z with before = b } | [] -> z
let delete z = match z.after with _ :: a -> { z with after = a } | [] -> z
 
let rec repeat n f z = if n = 0 then z else repeat (n - 1) f (f z)
 
let show z =
  let s l = String.of_seq (List.to_seq l) in
  s (List.rev z.before) ^ "|" ^ s z.after

Running it; | is the cursor.

start            |the zipper
right x4         the |zipper
delete x6        the |
insert "fast "   the fast |
left x2          the fas|t 
backspace        the fa|t

Moving the cursor moves one element from one list to the other, and inserting or deleting at the cursor conses onto or removes from the head of one of them. This is the functional counterpart of a gap buffer, the array with a gap at the cursor used by text editors such as Emacs.

§ 03

Trees

For binary trees, a step of the path records whether the step went left or right, the value at the node it passed through, and the subtree it did not enter. A zipper is the focused subtree and the list of steps from the focus back to the root:

step (A) = A \times tree (A) + tree (A) \times A zipper (A) = tree (A) \times list (step (A))

A binary-tree zipper: moving down, rebuilding on the way up, and editing.

type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree
 
(* One step of the path back to the root: which way we went, and what we
   passed by, the parent's value and the other subtree. *)
type 'a step = WentLeft of 'a * 'a tree | WentRight of 'a tree * 'a
type 'a zipper = { focus : 'a tree; path : 'a step list }
 
let of_tree t = { focus = t; path = [] }
 
let down_left z =
  match z.focus with Node (l, v, r) -> Some { focus = l; path = WentLeft (v, r) :: z.path } | Leaf -> None
 
let down_right z =
  match z.focus with Node (l, v, r) -> Some { focus = r; path = WentRight (l, v) :: z.path } | Leaf -> None
 
let up z =
  match z.path with
  | WentLeft (v, r) :: p -> Some { focus = Node (z.focus, v, r); path = p }
  | WentRight (l, v) :: p -> Some { focus = Node (l, v, z.focus); path = p }
  | [] -> None
 
let rec to_tree z = match up z with Some z' -> to_tree z' | None -> z.focus
let modify f z = match z.focus with Node (l, v, r) -> { z with focus = Node (l, f v, r) } | Leaf -> z
 
let rec show = function
  | Leaf -> "."
  | Node (Leaf, v, Leaf) -> string_of_int v
  | Node (l, v, r) -> "(" ^ show l ^ " " ^ string_of_int v ^ " " ^ show r ^ ")"
 
let ( >>= ) = Option.bind

Running it.

tree           ((1 2 3) 4 (5 6 7))
focus          5
path length    2
after edit     ((1 2 3) 4 (500 6 7))
left subtree shared:   true
right subtree shared:  false
original unchanged     ((1 2 3) 4 (5 6 7))

Going down pushes a step; going up pops one and rebuilds a single node. An edit at depth $d$ followed by returning to the root allocates $d + 1$ nodes, those on the path. The rest of the tree is shared between the old version and the new one: the physical equality test shows that the untouched left subtree is the same object in both, which is what makes the structure persistent^[7]. An editor can keep the previous versions for undo at a cost proportional to the edited paths.

Huet's zipper

Huet's paper treats trees whose nodes have any number of children. A step of the path records the siblings to the left of the focus, nearest first, the path above, and the siblings to the right, so the focus can also move sideways in constant time^[1]:

Huet's zipper, with his example of the tree for a * b + c * d.

(* Huet's zipper for trees with any number of children, following his
   1997 paper. A path records the siblings to the left (nearest first),
   the path above, and the siblings to the right. *)
type tree = Item of string | Section of tree list
type path = Top | Node of tree list * path * tree list
type location = Loc of tree * path
 
let go_left (Loc (t, p)) =
  match p with
  | Node (l :: left, up, right) -> Loc (l, Node (left, up, t :: right))
  | _ -> failwith "left of first"
 
let go_right (Loc (t, p)) =
  match p with
  | Node (left, up, r :: right) -> Loc (r, Node (t :: left, up, right))
  | _ -> failwith "right of last"
 
let go_up (Loc (t, p)) =
  match p with
  | Node (left, up, right) -> Loc (Section (List.rev_append left (t :: right)), up)
  | Top -> failwith "up of top"
 
let go_down (Loc (t, p)) =
  match t with
  | Section (t1 :: trees) -> Loc (t1, Node ([], p, trees))
  | _ -> failwith "down of item or empty"
 
let change (Loc (_, p)) t = Loc (t, p)
let insert_right (Loc (t, p)) r =
  match p with Node (left, up, right) -> Loc (t, Node (left, up, r :: right)) | Top -> failwith "insert of top"
 
let rec root (Loc (t, p) as l) = match p with Top -> t | _ -> root (go_up l)
 
let rec show = function
  | Item s -> s
  | Section ts -> "[" ^ String.concat " " (List.map show ts) ^ "]"

Running it.

tree      [[a * b] + [c * d]]
focus     d
edited    [[a * b] + [c * e f]]

The navigation functions are partial: at the top there is no parent, and at the last child nothing to the right. Huet's paper uses them to build a structure editor and discusses scars, a variant that remembers which child was last visited so that going up and down again returns to it^[1].

§ 04

Derivatives

McBride observed that the context type of a zipper can be computed from the structure's type by differentiating it^[2]. Read a type as an expression in the element type $x$ , with $+$ for sum types, $\times$ for product types, $1$ for the unit type and $0$ for the empty type. A one-hole context is a value of the type with one occurrence of $x$ removed, and removing an $x$ follows the rules of differentiation:

\partial x = 1 \partial c = 0 \partial (A + B) = \partial A + \partial B \partial (A \times B) = \partial A \times B + A \times \partial B

The product rule says that the hole in a pair is either in the first component, with the second intact, or in the second, with the first intact. For a triple $x^{3}$ the derivative is $3 x^{2}$ : the hole is in one of three positions, and the other two elements remain. The number of pairs of a value and one of its positions, counted over all values with elements from an $n$ -element set, is $n$ times the number of contexts, since a pair is a context with an element in the hole:

Symbolic derivatives of polynomial types, with the contexts counted.

(* Polynomial types in one variable x, their derivatives, and a check that
   the derivative counts one-hole contexts. *)
type ty = Zero | One | X | Plus of ty * ty | Times of ty * ty
 
let rec d = function
  | Zero | One -> Zero
  | X -> One
  | Plus (a, b) -> Plus (d a, d b)
  | Times (a, b) -> Plus (Times (d a, b), Times (a, d b))
 
(* The values of a type when x has n elements: E i is an element. *)
type v = U | E of int | L of v | R of v | P of v * v
 
let rec values n = function
  | Zero -> []
  | One -> [ U ]
  | X -> List.init n (fun i -> E i)
  | Plus (a, b) -> List.map (fun v -> L v) (values n a) @ List.map (fun v -> R v) (values n b)
  | Times (a, b) -> List.concat_map (fun u -> List.map (fun w -> P (u, w)) (values n b)) (values n a)
 
let rec holes = function U -> 0 | E _ -> 1 | L v | R v -> holes v | P (a, b) -> holes a + holes b
 
let size n t = List.length (values n t)
 
(* The number of values as a polynomial in the size of x: coefficients,
   constant term first. *)
let rec add a b = match (a, b) with [], c | c, [] -> c | x :: a, y :: b -> (x + y) :: add a b
let rec mul a b = match a with [] -> [] | x :: a -> add (List.map (( * ) x) b) (0 :: mul a b)
 
let rec poly = function
  | Zero -> [] | One -> [ 1 ] | X -> [ 0; 1 ]
  | Plus (a, b) -> add (poly a) (poly b)
  | Times (a, b) -> mul (poly a) (poly b)
 
let show p =
  let term i c = match (i, c) with 0, c -> string_of_int c | 1, 1 -> "x" | 1, c -> Printf.sprintf "%dx" c
    | i, 1 -> Printf.sprintf "x^%d" i | i, c -> Printf.sprintf "%dx^%d" c i in
  match List.filteri (fun _ (_, c) -> c <> 0) (List.mapi (fun i c -> (i, c)) p) with
  | [] -> "0"
  | ts -> String.concat " + " (List.map (fun (i, c) -> term i c) ts)

Running it.

triples
  F  = x^3
  dF = 3x^2
  n = 3:  holes in all values = 81,  n * |dF| = 81
lists of length at most 3
  F  = 1 + x + x^2 + x^3
  dF = 1 + 2x + 3x^2
  n = 3:  holes in all values = 102,  n * |dF| = 102
binary trees of depth at most 2
  F  = 1 + x + 2x^2 + x^3
  dF = 1 + 4x + 3x^2
  n = 3:  holes in all values = 120,  n * |dF| = 120

Recursive types

Lists satisfy $L = 1 + x \times L$ . Differentiating both sides and solving for $\partial L$ :

\partial L = L + x \cdot \partial L ⟹ \partial L = \frac{L}{1 - x} = L \times L

using $1/ (1 - x) = L$ . A list with a hole is a pair of lists, the elements before the hole and the elements after it: the list zipper. For a recursive type $T = F (x, T)$ the general rule is a chain rule^[3]:

\partial T = list (\partial_{T} F (x, T)) \times \partial_{x} F (x, T)

The list is the path of steps down to the node that contains the hole, each step a context for one recursive position, and the last factor is the context of the element within that node. Binary trees have $F (x, T) = 1 + x \times T^{2}$ , so $\partial_{T} F = 2 x T$ and $\partial_{x} F = T^{2}$ :

\partial T = list (2 x T) \times T^{2}

A step is one of two alternatives, each with the parent's value and the other subtree, which is the step type above, and the hole sits in a node whose two subtrees are the $T^{2}$ . A zipper focused on a whole subtree, as in the code, uses the path alone: $T \times list (2 x T)$ .

Combinatorial species

The same derivative appears in Joyal's theory of combinatorial species, which treats classes of labelled structures as formal power series^[4]. The derivative of a species is the species of structures with one extra point, unlabelled, and the operations of calculus on generating functions correspond to operations on structures^[5]. McBride's observation and its generalization to containers by Abbott, Altenkirch, Ghani and McBride carry this over to data types^[3]. A related operation, dissection, splits a structure into a part already processed and a part still to be processed, like the two sides of a zipper with different element types, and can be used to derive tail-recursive traversals^[11].

§ 05

Applications

Structure editors were the original application: the focus is the cursor, and every editing command is a local operation at it^[1]. The xmonad window manager keeps each workspace's windows in a list zipper, with the focused window at the focus, so that moving focus and swapping windows are local^[10]. Zippers are used for navigating file systems and XML documents, for tracking the position in a traversal so that it can be suspended and resumed, and in theorem provers to represent a proof state with a focused goal. Finger trees apply a related idea to sequences, keeping both ends of a balanced tree within constant distance of the root.

Writing a zipper by hand for every data type is repetitive. Generic programming libraries derive them automatically: Hinze and Jeuring gave a generic construction^[8], and Adams's "Scrap your zippers" works over any type with a generic traversal^[9].

§ 06

History

Huet published the zipper as a functional pearl in 1997, presenting it as an idea that had been used and rediscovered informally without being published^[1]. McBride's note connecting it to differentiation circulated in 2001^[2], and Abbott, Altenkirch, Ghani and McBride gave the theory for containers in 2003, published in 2005^[3].