*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.

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 *a*s is either empty, denoted `[]`

, or it is a cons of a single *a* onto another list of *a*s, 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 *a*s.

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 `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

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?

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:

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

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 `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

for some polynomial *p*, and deduce

where *q*1 and *q*2 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.