Chris Taylor

Mainly math and haskell

The Algebra of Algebraic Data Types, Part 2

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 2 in a series; you can read Part 1 here.

Last time I introduced the unit type Unit or () and the zero type Void. I also introduced the type operators Add and Mul, and the function type a -> b.

In this post I’ll be using both Haskell notation and mathematical notation. The table below will help you convert back and forth between the two.

$$ \begin{align} {\rm Void} && \leftrightarrow && 0 \\ () \,,\; {\rm Unit} && \leftrightarrow && 1 \\ {\rm Add} \; a \; b && \leftrightarrow && a + b \\ (a,b) \,,\; {\rm Mul} \; a \; b && \leftrightarrow && a \cdot b \\ a \rightarrow b && \leftrightarrow && b ^ a \end{align} $$

In this post I’ll talk about recursive types, and show how you can abuse the algebra of types to deduce interesting things about them.

Maybe

Let’s ease ourselves in by exploring Maybe a. This is the type that indicates that it might contain a value of type a, but it also might be empty. It’s defined like this

data Maybe a = Nothing | Just a

The vertical bar indicates that this is a sum type, so we could write it using the type Add that we defined last time, if we first defined the types Nothing and Just a. It would look like this:

data Nothing = Nothing
data Just a  = Just a

type Maybe a = Add Nothing (Just a)

See how we’ve replace the data declaration with a type declaration? That means that Maybe a is no longer a new type – it’s just a synonym for a type we already knew about.

But we can take it further. Notice that Nothing only has one value, so it’s equivalent to (). Similarly, Just is a container with a single value of type a, so it’s equivalent to a. We therefore have

type Maybe a = Add () a

But that’s the same as saying that Maybe a is the same as 1 + a. All that Maybe does is add one more possible value to a type.

Recursive Types

Lists

The basic list in Haskell is a linked list. A list of as is either empty, denoted [], or it is a cons of a single a onto another list of as, denoted a : as. If we wanted to define lists ourself, we could write something like

data List a = Nil | Cons a (List a)

Let’s take a second to look at the structure of this declaration. Just like Maybe, the List type is the sum of two simpler types.

The first summand is Nil, a nullary constructor which is equivalent to ().

The second summand is Cons a (List a), which is a product consisting of an a and a list of as.

The algebraic form, if we write lists as L(a), is

$$ L(a) = 1 + a \cdot L(a) $$

It seems as though we should be able to write the list type in Haskell as

type List a = Add () (a, (List a))

but in fact that won’t compile. The reason is that type synonyms are expanded out at compile time, after type checking, but before compilation. This definition would never finish expanding – it would just keep growing as

Add () (a, Add () (a, Add () (a, ...)))

and so on. The reason that this doesn’t work is to do with the way that Haskell handles recursive type definitions (like most languages with sophisticated type systems, it uses isorecursive rather than equirecursive types).

The way around it is to use a newtype declaration instead of a type declaration, and wrap the type inside a new constructor L:

newtype List a = L (Add () (a, List a))

This is just to satisfy the type checker – when the code is compiled the additional constructor will be optimized away, and what we’re left with will be identical to the type declaration above.

If I write the type List a as L(a) then this declaration for lists says that

$$ L(a) = 1 + a \cdot L(a) $$

To see what lists really are, we can start expanding the definition by repeated substitution. In the expansion, whenever I see a type of the form a · a, I’ll replace it with a² to save space.

Exercise: the expression a² can denote a pair (a, a) or a function 2 → a. Show these are the same.

$$ \begin{align} L(a) & = 1 + a \cdot L(a) \\ & = 1 + a \cdot (1 + a \cdot L(a)) \\ & = 1 + a + a ^ 2 \cdot (1 + a \cdot L(a)) \\ & = 1 + a + a ^ 2 + a ^ 3 \cdot (1 + a \cdot L(a)) \\ & = \ldots \\ & = 1 + a + a ^ 2 + a ^ 3 + a ^ 4 + a ^ 5 + \cdots \end{align} $$

This is telling us that a list of a is either the empty list, or it’s a list containing a single a, or a list of two a, or three a, etc. Maybe you already knew that - but it’s neat that the algebra is telling us!

But now, here is something really cool. Let’s start with our equation for lists, and instead of repeatedly substituting, we’ll forget for a moment that the objects are types and pretend that they’re arbitrary mathematical expressions. That means we’re justified in using whatever techniques we like to “solve for L(a)”.

First subtract a · L(a) from both sides:

$$ L(a) - a \cdot L(a) = 1 $$

Now factor out the L(a) on the left-hand side:

$$ (1 - a) \cdot L(a) = 1 $$

And finally, divide both sides by 1 - a:

$$ L(a) = \frac{1}{1-a} $$

This looks nonsensical, because we don’t know what it means to subtract one type from another, and we certainly don’t know what it means to divide one type by another. But is it telling us something interesting anyway?

If you studied calculus, you may remember that many functions have an expansion as a Taylor Series. We can ask Wolfram Alpha what the Taylor series of 1 / (1 - a) is, and it tells us:

$$ L(a) = 1 + a + a ^ 2 + a ^ 3 + a ^ 4 + \cdots $$

That is, the series expansion of L(a) is exactly what we deduced from our repeated substitutions. Although we abused the algebra horribly, by performing operations that are completely unjustified on types, we still ended up with a sensible answer.

Trees

Consider the type of binary trees with values at the nodes. In Haskell you can write this as

data Tree a = Empty | Node a (Tree a) (Tree a)

In a way that is probably becoming familiar, we can look at this as a sum of two types - a nullary type equivalent to (), and a product type. This time it is a product of three terms, but that’s not a problem - we just use a nested product, of the form (a, (b, c)).

The definition in terms of operators that we already know about (again, using a newtype to allow us to have a recursive definition) is

newtype Tree a = T (Add () (a, (Tree a, Tree a)))

In algebraic language, with T(a) for the type of trees, we would write

$$ T(a) = 1 + a\cdot T(a)^2 $$

To get a better handle on what trees are, we could apply repeated substitution in the same way we did for lists, but it would be much messier. Instead, can we apply the trick of rearranging the equation to solve for T(a)?

First, rearrange to get everything on one side of the equation:

$$ a \cdot T(a)^2 - T(a) + 1 = 0 $$

We can now recognize this as a quadratic equation for T(a), which we can solve using the quadratic formula, to get

$$ T(a) = \frac{1 - \sqrt{1 - 4 a}}{2a} $$

This makes even less sense than the equation for lists. What on earth does it mean to take the square root of a type? But, keeping calm, we again ask Wolfram Alpha for the series expansion, and it tells us

$$ T(a) = 1 + a + 2a ^ 2 + 5a ^ 3 + 14a ^ 4 + \cdots $$

How do we make sense of this? The first two terms tell us that a tree can either be empty (if it is Empty) or it can have one value of type a (if it is Node a Empty Empty).

Then the next term tells us that a tree can contain two values of type a, in two different ways, while the next term tells us that there can be three values of type a in five different ways.

But that’s exactly what we notice if we enumerate all of the binary trees, grouping them by the number of values they contain. There is one tree with no values and one tree with one value. Then there are two trees with two values and five trees with three values – as in this picture (borrowed from the excellent book Analytic Combinatorics by Flajolet and Sedgewick).

The equation counts the number of different binary trees that can exist! This counting property is related to the simple value-counting examples we saw in the first post, and also related to combinatorial species, as written about extensively by Brent Yorgey. Species and types have a lot in common, although they are not the same thing.

Seven Trees In One

If we restrict to trees that contain only the unit type, i.e. Tree (), then the a appearing in T(a) is equal to 1, and we can write the defining equation of trees as

$$ T = 1 + T^2 $$

By playing with the algebra, and repeatedly using the fact that \( T ^ 2 = T - 1 \), we can deduce that

$$ \begin{align} T^6 & = (T-1) ^ 3 \\ & = T ^ 3 - 3T ^ 2 + 3T - 1 \\ & = T (T - 1) - 3T ^ 2 + 3T - 1 \\ & = - 2T ^ 2 + 2T - 1 \\ & = -2(T-1) + 2T - 1 \\ & = 1 \end{align} $$

which, when interpreted in the language of types, says that a six-tuple of trees is equivalent to the unit type. In other words, there is only one six-tuple of trees.

This is clearly nonsense, so what’s gone wrong? Even more mysterious is that if we just multiply both sides of the equation by T, we get

$$ T ^ 7 = T $$

which isn’t nonsense - it says that a seven-tuple of trees is equivalent to a single tree.

At first glance this isn’t a profound result. Any two types that have a countably infinite number of possible values are equivalent - that’s what being countable means.

However, it’s more subtle than this. In the paper Seven Trees In One, Andreas Blass not only shows how to find an explicit map from seven trees to one and back again (essentially he tells you how to write the from and to functions from the previous post), but he shows that the functions never have to look more than four levels deep into any of the trees.

Finally, he explains why deducing that \( T ^ 7 = T \) is valid, but \( T ^ 6 = 1 \) is not. It turns out that you can turn a derivation like the one I gave above, which uses subtraction, into an ‘honest’ proof that doesn’t use subtraction, and hence is valid for types – but only when the power of T that you start with is one more than a multiple of 6. Hence you can reduce \( T ^ 7 \) to \( T \) (because 7 = 6 + 1) but you can’t reduce \(T ^ 6\) to 1.

An Explanation?

It would be fair if you come away thinking that this post has raised more questions than it has supplied answers. For example,

  • What does it mean to subtract, divide or take square roots of types?
  • What else you can do to a type equation that still has a meaningful computational interpretation?
  • Why do unjustified manipulations of type equations produce sensible answers anyway?

As a teaser for the last question, a mathematical structure that models types is the semiring. That’s just a way of saying that you can add and multiply objects, and you have objects corresponding to 0 and 1. There is a paper by Marcelo Fiore and Tom Leinster that shows that if you can start with a complex number t defined by the equation

$$ t = p(t) $$

for some polynomial p, and deduce

$$ q_1(t) = q_2(t) $$

where q1 and q2 aren’t constant (they can’t just be 1) then the same result is true for semirings. In particular, it is true for types, and you can find a proof that doesn’t use subtraction, or any other operators that are illegal for types.

Next time, I’ll explain what zippers are, and describe how to do calculus with types.