Type Derivatives & Zippers

Taking the derivative of a type gives you "the type of one hole contexts" of your original type.

What it gives you is a generic way to traverse your data type from the perspective of a 'hole' (akin to pointers).

ex) If I had a tree data type, I would get a way to write primative combinators
'left', 'right', 'up', 'down', etc.

-- binary tree with no data
data Tree = Leaf | Node Tree Tree

this is equivalently expressed as a polynomial

Tree(X)= 1 + ( X * X )

where 1 ≅ Leaf
(X * X) ≅ Node Tree Tree

or

Tree(X) = 1 + X²

We know how to take the derivative of polynomials

Derivative(Tree) = 0 + (1 * X + X * 1) ≅ 2X

This is isomorphic to type

type Tree' X = (Unit :*: X) :+: (X :*: Unit)

This Tree' type represents the idea of
  Either
    the hole(Unit) is pointing to the left subtree (and we record what the right subtree is)
  or
    the hole(Unit) is pointing to the right subtree (and we record what the left subtree is)

If you have a List of Tree' elements, this represents a traced path from the root node to the hole

And if you have a trace from the root node to the hold AND a subtree to fill the hole, THEN you can reconstruct the whole tree.