Data Structure Differentiation, Intuition Building

Question

According to this paper differentiation works on data structures.

According to this answer:

Differentiation, the derivative of a data type D (given as D') is the type of D-structures with a single “hole”, that is, a distinguished location not containing any data. That amazingly satisfy the same rules as for differentiation in calculus.

The rules are:

 1 = 0
 X′ = 1
 (F + G)′ = F' + G′
 (F • G)′ = F • G′ + F′ • G
 (F ◦ G)′ = (F′ ◦ G) • G′

The referenced paper is a bit too complex for me to get an intuition. What does this this mean in practice? A concrete example would be fantastic.

Answer 1

What's a one hole context for an X in an X? There's no choice: it's (-), representable by the unit type.

What's a one hole context for an X in an X*X? It's something like (-,x2) or (x1,-), so it's representable by X+X (or 2*X, if you like).

What's a one hole context for an X in an X*X*X? It's something like (-,x2,x3) or (x1,-,x3) or (x1,x2,-), representable by X*X + X*X + X*X, or (3*X^2, if you like).

More generally, an F*G with a hole is either an F with a hole and a G intact, or an F intact and a G with a hole.

Recursive datatypes are often defined as fixpoints of polynomials.

data Tree = Leaf | Node Tree Tree

is really saying Tree = 1 + Tree*Tree. Differentiating the polynomial tells you the contexts for immediate subtrees: no subtrees in a Leaf; in a Node, it's either hole on the left, tree on the right, or tree on the left, hole on the right.

data Tree' = NodeLeft () Tree | NodeRight Tree ()

That's the polynomial differentiated and rendered as a type. A context for a subtree in a tree is thus a list of those Tree' steps.

type TreeCtxt = [Tree']
type TreeZipper = (Tree, TreeCtxt)

Here, for example, is a function (untried code) which searches a tree for subtrees passing a given test subtree.

search :: (Tree -> Bool) -> Tree -> [TreeZipper]
search p t = go (t, []) where
  go :: TreeZipper -> [TreeZipper]
  go z = here z ++ below z
  here :: TreeZipper -> [TreeZipper]
  here z@(t, _) | p t       = [z]
                | otherwise = []
  below (Leaf,     _)  = []
  below (Node l r, cs) = go (l, NodeLeft () r : cs) ++ go (r, NodeRight l () : cs)

The role of "below" is to generate the inhabitants of Tree' relevant to the given Tree.

Differentiation of datatypes is a good way make programs like "search" generic.