I gave a talk on this subject at London Haskell in November 2012. A video of the talk is on YouTube and slides are on GitHub. This is Part 3 in a series; you can also read Part 1 and Part 2.
Last time I described recursive types, showed how they can be written as algebraic equations, and you you can solve the equations to deduce interesting facts about types. In this post I’ll explain what it means to do calculus with types.
Zippers
The regular Haskell list is a linked list. While they are simple to define and convenient to work with, they have disadvantages. If you want to append an element to the list of length n, it takes O(n) time. Accessing or modifying elements partway through the list is also slow. Linked lists don’t support efficient random access.
You could solve this with an array, but immutable arrays have their own problems. Data sharing is harder, for example, if you want the elements of the array to be contiguous in memory.
Fortunately, not all applications require random access. Sometimes you just want to keep track of your location within a list, with the ability to move around in the list, possibly modifying elements as you go.
This is exactly the functionality offered by a zipper, which is a data structure with a pointer to a distinguished location, called the focus.
List Zippers
You can write a zipper for any data structure, but I’ll focus on lists.
To store the pointer we could wrap the list up with an Int
that stores the location currently in focus. That’s fraught with all kind of difficulties, though – and it doesn’t meet our requirements for efficient access to the element in focus.
Instead, we define a new type composed of the element in focus, coupled with a pair of lists - one of which contains the elements before the focus, and the other the elements after the focus. Schematically it looks like this:
The element in focus is in the center, and the two lists on either side. In Haskell we would write:
data Zipper a = Z [a] a [a]
For a zipper to be useful we need to define functions that move the focus left and right. For efficiency reasons we store the first list in reverse order – we need to efficiently add and remove elements from the end of the list, rather than the head:
left (Z (l:ls) c rs) = Z ls l (c:rs)
right (Z ls c (r:rs)) = Z (c:ls) r rs
If you want to read more about zippers, the final chapter of Learn You a Haskell has a great introduction.
One-Hole Contexts
The zipper is a product type – it’s the product of two lists of as and a single a. Remembering that lists are L(a) = 1 / (1 - a), the list zipper LZ(a) is written as
$$ \begin{align}
L\!Z(a) & = a \cdot L(a) \cdot L(a) \\
& = \frac{a}{(1-a) ^ 2}
\end{align}
$$
Because a zipper is a product type, it’s possible to tease it apart, decomposing it into a single piece of data of paired with two lists. The two lists tell us where the focus is, and we complete the zipper by filling in the piece of data that’s in focus. Algebraically we have
$$ Z(a) = a \cdot L(a) ^ 2 $$
which is clearly equivalent to the previous expression. The first part of the product is just a piece of data, and we can think of the second as a data structure with a hole. When we ‘fill in’ the hole by pairing it with some data, we get a zipper. This ‘data structure with a hole’ goes by the name of a one-hole context. For the list zipper, this looks like:
The empty circle is a hole, representing ‘no data’ – it’s a placeholder for data. The type that contains no data is the unit type ()
, so we can say that the type of a hole is ()
.
There’s nothing special about list zippers – any zipper can be decomposed into a one-hole context, and a piece of data that fills the hole.
One-Hole Contexts for Tuples
I said that you can write a zipper for any data type, so let’s write some zippers for tuples – that is, types of the form \( a ^ n \) for some whole number n.
One-Tuples
The simplest case is a one-tuple, which is just a single piece of data. A zipper for a one-tuple is trivial - there’s only one location for data, so there’s only one focus – the zipper for a one-tuple a is just a.
But remember that a zipper is a piece of data paired with a one-hole context, so what is the one-hole context? There’s only one place to put the hole, and once we’ve put a hole in a single piece of data, we’re just left with the hole! Schematically, the pairing of the data with the one-hole context looks like this:
$$ ( a, \circ )$$
The type of the one-hole context has to be ()
, or 1, so that when we paired it with the data a, we get a back again.
Two-Tuples
In a two-tuple there are two possible locations for the hole. Remembering that a sum represents a choice, either the left constructor or the right constructor, the pairing of data and one-hole context looks like:
$$ \Big( a , \; (\circ, a) + (a,\circ) \Big)$$
Remembering that the type of the hole is 1, the type of the one-hole context is a + a, or 2a.
Three-Tuples
In a three-tuple there are three possible locations for the hole. The pairing of data and one-hole context looks like
$$ \Big( a, \;(\circ,a,a) + (a,\circ,a) + (a,a,\circ) \Big) $$
The type of the one-hole context is a² + a² + a², or 3a².
Finding the pattern
Perhaps you’ve already seen the pattern. In the left column are the types of n-tuples for n = 1, 2, 3 and in the right column are their corresponding zippers:
$$
\begin{align}
a^{\phantom{2}} &&& 1 \\
a^2 &&& 2a \\
a^3 &&& 3a^2
\end{align}
$$
If you’ve studied any calculus, you will immediately spot the pattern – for an n-tuple of type \( a ^ n \), the type of the zipper is \( n a ^ {n-1} \), which is exactly the derivative of \( a ^ n \).
In fact, this pattern always applies! This was noted by Conor McBride in a paper, whose title gives the key insight:
“The Derivative of a Regular Type is its Type of One-Hole Contexts”
If you take a type expression and differentiate it, the result is the type of one-hole contexts for that type. This makes it easy to figure out how to write zippers for arbitrary data types.
Calculus of Types
I’ll use the notation \( \partial_a \) to mean ‘take the derivative with respect to a’. You may already be familiar with the notation \( d / da\) for differentiation – this is no different, but it has the advantage that it can be typeset on one line!
How far can we push the analogy between taking the derivative of a type and finding its type of one-hole contexts? Is it valid to differentiate a type in all contexts, or do we have to be careful? We should certainly check that the operation of differentiation makes sense when applied to the types we already know about, for example.
Constants
Here’s a simple rule from calculus – the derivative of any constant is zero:
$$ \partial_a({\rm const}) = 0 $$
To interpret this for types, remember that the derivative operator d/da makes holes in a data structure that contains data of type a. This equation is saying that if a type doesn’t have any data of type a, then its one-hole context is Void
, i.e. you can’t create any instances of it.
Sums
The sum rule for derivatives is that for any f(a) and g(a), differentiating the sum is the same as differentiating individually and then summing:
$$ \partial_a (f(a) + g(a)) = \partial_a f(a) + \partial_a g(a) $$
This tells us that making a hole in the sum type is equivalent to making a hole in each of the summands, and taking their sum. In more explicit language, if F a
and G a
are types with one-hole contexts DF a
and DG a
, then the one-hole context of
type Sum a = Add (F a) (G a)
is
type DSum a = Add (DF a) (DG a)
Products
In calculus, the derivative of a product is given by Leibniz’s product rule:
$$ \partial_a ( f(a) \cdot g(a) ) = \partial_a f(a)\cdot g(a) + f(a) \cdot \partial_a g(a) $$
Interpreted as a statement about types, this tells us that making a hole in the product of two types is equivalent to either making a hole in the first type (and leaving the second one as it is) or making a hole in the second type (and leaving the first one as it is). That is, the one-hole context of
type Prod a = (F a, G a)
is
type DProd a = Add (DF a, G a) (F a, DG a)
Composition
We haven’t yet met composition. This occurs when you have a data structure F
that holds elements of type G a
. In Haskell, we could write this as
data Compose f g a = Compose (f (g a))
where f
and g
have kind * -> *
and a
has kind *
, although its simpler to keep the syntax light and just write f (g a)
.
In calculus the chain rule tells us how to differentiate compositions:
$$ \partial_a f (g (a)) = \partial_a g(a) \cdot \partial_g f (g(a)) $$
As a type equation, this says that to make a hole in a layered data structure, we need a product – one half of the product tells us where the hole is in the outer structure, and the other half keeps track of the hole in the inner structure. That is, the one-hole context of
type Comp a = F (G a)
is
type DComp a = (DG a, DF (G a))
Deriving Zippers
I said that knowing that the derivative of an ADT corresponds to its type of one-hole contexts makes it easy to derive zippers for arbitrary data types. Now I’ll justify that assertion.
List Zippers
The type of lists is
$$ L(a) = \frac{1}{1-a} $$
We can differentiate this using the quotient rule and the chain rule, finding
$$ \partial_a L(a) = \frac{1}{(1-a) ^ 2} = L(a) ^ 2 $$
which says that the one-hole context of a list is a pair of lists, exactly as we saw earlier. To get the list zipper we take the product of an a with a pair of lists L(*a).
Tree Zippers
Remember that the type of binary trees T(a) is defined by the recursive equation
$$ T(a) = 1 + a \cdot T(a) ^ 2 $$
We could solve for T(a) as we did in the previous post, and differentiate the result. However, it’s much easier to use implicit differentiation to differentiate the above expression, to get
$$ \partial T(a) = T(a) ^ 2 + 2 \cdot a \cdot T(a) \cdot \partial T(a) $$
We can then solve this for dT/da, finding
$$ \partial T (a) = \frac{T(a) ^ 2}{1 - 2 \cdot a\cdot T(a)} $$
To make sense of this, remember that the type 1 / (1 - x) is synonymous with the type L(x), of lists of x. So the tree zipper is
$$ \partial T (a) = T(a) ^ 2 \cdot L\big(2 \cdot a \cdot T(a)\big) $$
That is, the one-hole context of a tree is a product of two trees, and a list holding elements of type (Bool, a, Tree a)
. It looks like this:
The hole is our current location, the focus. Beneath the hole are two trees, which hold the part of the tree that we haven’t yet traversed. In this picture they are both single-element trees.
The sequence of red nodes leading back to the top of the tree is the past - the elements of the tree that we traversed to end up at the hole. Each node is associated with a Bool
, which tells us whether we took the left or the right branch after passing through that node, and a Tree a
which contains all the elements that we missed by not going down the other path.
Exercise: Code up the zipper for binary trees, remembering that a zipper is a one-hole context paired with data. You’ll need to write functions left
and right
to take the left or right path at a particular node, and up
to go back up the tree.
Exercise: Rose trees are trees with arbitrarily many branches from each node. In Haskell you would define them by
data Rose a = Rose a [Rose a]
What does a rose tree zipper look like?
Next Time
In this post we learned what it means to take the derivative of an ADT, and how to manipulate the type algebra to automatically derive zippers for arbitrary data types.
Next time I’ll talk about assigning a meaning to subtraction and division of types – and I might get on to mentioning combinatorial species.