Last time I introduced the unit type
() and the zero type
Void. I also introduced the type operators
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.
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.
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
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
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.
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
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
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
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
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.
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:
Now factor out the L(a) on the left-hand side:
And finally, divide both sides by 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?
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.
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
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:
We can now recognize this as a quadratic equation for T(a), which we can solve using the quadratic formula, to get
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
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
By playing with the algebra, and repeatedly using the fact that \( T ^ 2 = T - 1 \), we can deduce that
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
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
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.
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
for some polynomial p, and deduce
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.