Zipper

A data structure with a focus: the subterm at the focus, plus the path back to the root together with everything not on it. Moving the focus and editing at it take constant time, and the type of contexts is the derivative of the structure's type.

A list zipper and a binary tree zipper.

(* List zipper: the elements before the focus (nearest first), and after. *)
type 'a lzip = { before : 'a list; focus : 'a; after : 'a list }
 
let left z = match z.before with x :: b -> { before = b; focus = x; after = z.focus :: z.after } | [] -> z
let right z = match z.after with x :: a -> { before = z.focus :: z.before; focus = x; after = a } | [] -> z
 
(* Binary tree zipper: the path back to the root records, at each step,
   which way we went and the sibling we did not take. *)
type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree
type 'a step = WentLeft of 'a * 'a tree | WentRight of 'a tree * 'a
type 'a tzip = { path : 'a step list; here : 'a tree }
 
let down_left z = match z.here with
  | Node (l, v, r) -> { path = WentLeft (v, r) :: z.path; here = l } | Leaf -> z
let down_right z = match z.here with
  | Node (l, v, r) -> { path = WentRight (l, v) :: z.path; here = r } | Leaf -> z
let up z = match z.path with
  | WentLeft (v, r) :: p -> { path = p; here = Node (z.here, v, r) }
  | WentRight (l, v) :: p -> { path = p; here = Node (l, v, z.here) }
  | [] -> z
let rec root z = if z.path = [] then z.here else root (up z)
let modify f z = match z.here with Node (l, v, r) -> { z with here = Node (l, f v, r) } | Leaf -> z
 
let rec show = function
  | Leaf -> "."
  | Node (l, v, r) -> "(" ^ show l ^ " " ^ string_of_int v ^ " " ^ show r ^ ")"

Editing the node 3 in place, and moving along a list.

before  ((. 1 .) 2 ((. 3 .) 4 .))
after   ((. 1 .) 2 ((. 300 .) 4 .))
list zipper after two rights: before [2; 1], focus 3, after [4]

Read a type as a polynomial in its element type $x$ . Lists satisfy $L = 1 + xL$ , so $L = 1/ (1 - x)$ . A one-hole context is the structure with one $x$ taken out, and taking one $x$ out of a product follows the product rule:

\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

\frac{\partial L}{\partial x} = \frac{1}{( 1 - x ) ^{2}} = L \times L

A one-hole context of a list is two lists, the elements before the hole and after it, which is the list zipper above. For binary trees with values at the nodes, $T = 1 + x T^{2}$ :

\partial T = T^{2} + 2 x T \partial T ⟹ \partial T = \frac{T ^{2}}{1 - 2 x T} = T^{2} \times L (2 x T)

The hole is at some node's value, whose two subtrees give the $T^{2}$ , and above it is a list of steps, each recording a direction (the 2), the value $x$ at that node and the sibling subtree $T$ . The tree zipper above focuses a whole subtree rather than a value, so its context is the path alone, $L (2 x T)$ , with the steps as WentLeft and WentRight.