Types and Power Series

In this post I'm going to try and introduce the two major components of Algebraic Data Types (ADT's), what connection they have with algebra, and some cool algebraic magic we can do on ADT's by representing them as a power series.

Choice as a Sum

Say we want to represent a number as being either an integer, or a floating point number. We might declare the type as Num = Choice Int Float or Num = Int or Float, or perhaps as Num = Int | Float, as a shorthand.

However we want to write it, the meaning of it doesn't change: we're choosing between two types. The Syntax is flexible but the Semantics is set in stone.

Now, this new 'Choice' operator we've created has a couple of interesting properties.

• It is commutative: choosing between A and B should be the same as choosing between B and A.
• It is associative: choosing first between A and B, and then between C should be the same as choosing between B and C and then A. Essentially, it doesn't matter in what order we make our choices, we're still choosing between three things and end up only with one of them.

So we can write Num = Int | Float or Num = Float | Int, since it is commutative.
We can also write Num = (Int | Float) | Double as Num = Int | (Float | Double) or even without any ambiguity Num = Int | Float | Double, since the Choice is associative.

Alright, we can choose between things in any order. Anything else we can find out about Choice?

Well, we can try and figure out how many elements/values our new type we created with Choice has.

Let's take the type BoolOrByte = Bool | Byte. So, we have a type Bool, which can be True or False, and we have a type Byte that has $2^8 = 256$ possible values. Then BoolOrByte is either one of 2 Bool values or one of the 256 Byte values, and so BoolOrByte can have $2 + 256 = 258$ values.

In general, the number of values a Choice type can have is the sum of the number of values of the choosable types, which we can write as #AorB = #(A | B) = #A + #B

Empty/Zero Type

There's a pretty weird type that I want you to consider right now. There are a lot of types: Int, Bool, String, each with a varying number of elements of that type. If Int is a 64-bit integer there are 2⁶⁴ elements, Bool has 2 elements and String has an infinite amount of elements!

But what about a type that has no elements, no possible values? That type is usually referred to as the Empty Type or Zero Type.

You can't do much with the Zero Type, but that's kind of the point. It's whole purpose is to represent something that can't be built. It's not very useful, I'll say that much, but it does have it's niche use cases, such as representing a non terminating function by giving it a type Int -> Empty. More advanced type systems can use it to represent the falsity of a proposition, but that's way beyond the scope of this little post.

What I'm interested in right now is how we can use it with Choice. If we have a type IntOrEmpty = Int | Empty what elements can that type have? It either has an element of Int , or an element of Empty. But since Empty has no elements, it can only have an element of Int! So IntOrEmpty = Int | Empty = Int! (It's also comforting to note that #IntOrEmpty = #Int + #Empty = #Int + 0 = #Int)

Since applying Choice to Empty pretty much does nothing, we say that Empty is the identity of the Choice operator, kind of like how $0$ is the identity of addition.

Pairing as a Product

Alright, being able to choose between two things is pretty neat, and it comes up often enough in programming to be relevant. But being able to have two things at once? Now that's something that is absolutely essential, so let's take the time to take a look at how might implement a 'Pair' operator.

Say we want to store a record of someone's name and age. We could state the record's type as a simple Record = Pair String Int or Record = (String, Int). Like before, the way we write it doesn't really matter, what matters is what we can do with it.

We know that Choice is associative and commutative, so let's try to show that Pair is as well. Having Record = (String, Int) or Record = (Int, String) is somewhat irrelevant, we can always swap between the two representations. The record still holds the same information, just in a different layout, so we can say that they are pretty much the same type (isomorphic would be the technical term). So, Pair is commutative, huzzah! Now, is it associative?

Let's see, if I also wanted to store the date of birth in the record I could extend the type to DatedRecord = ((String, Int), Date), where we now have a pair inside a pair. Anyone who has dabbled in a bit of Lisp or more functional languages will recognize that this is essentially a list, but kind of backwards.

The way it is usually presented is as DatedRecord = (String, (Int, Date)), with the pairs accumulating to the back of the type. But the information is exactly the same as before, we've just shuffled around pair boundaries, so we can say that the two representations are pretty much the same type.

So? This means that Pair is associative as well, and we can write DatedRecord as DatedRecord = (String, Int, Date), because the order in which we pair doesn't really matter!

Like we did for Choice, how many different values of BoolAndByte = (Bool, Byte) are there? Well, the first element can be either True or False, and the second element can be one of $2^8 = 256$ values, from $0$ to $255$, just like before. But this time we're not taking one or the other. We're taking both at the same time. So we can pair True with $256$ values, and we can pair False with $256$ values, totaling $2×256$ values we can have in our pair. In general, the number of values in a pair is the product of the number of values in each element type, and we can write that as before as #AandB = #(A, B) = #A × #B

Unit/One Type

Let's consider another pretty weird type, the type with just one element: Unit. The one element in Unit is usually represented as () or *.

If we Pair some type with Unit, like IntAndUnit = (Int, Unit), then since Unit only has one element, we're not really adding any additional in the pair. Any element of IntAndUnit is some integer and *, the unit element. In fact, if we consider how many elements IntAndUnit has we'll see that #IntAndUnit = #(Int, Unit) = #Int × #Unit = #Int × 1 = #Int.

Since putting Unit in a pair doesn't really do anything, we say that Unit is the identity of Pair, and we can write that (A, Unit) = A for any type A.

Whoops, there goes my Type

If you think that smashing together Unit in a pair with some other type was weird, wait until you do it with Empty.

How are you even supposed to build a pair of something with Empty, like IntAndEmpty = (Int, Empty), when Empty doesn't have any elements? That's the neat thing, you can't.

Just taking a look at the size of a type for pairs, #IntAndEmpty = #Int × #Empty = #Int × 0 = 0. So IntAndEmpty is empty, which means that IntAndEmpty is Empty.

This works for any type, and so, for any type A, (A, Empty) = Empty. We can call Empty the annihilator for Pair or the absorbing type.

"This is all fine and dandy", you might be saying to yourself, "but why are we even doing this?" Ah, fine question, completely unbiased mental representation of the reader. The beauty of all of this comes together when we put both Pair and Choice together.

Putting the two together

Time to dip some chocolate in peanut butter. What happens when we have a Choice inside of a Pair? Something like (Date, String | Int). This type represents storing a pair of a Date and either a String or an Int. So we can store either a String or an Int on the second element of the pair. But, hang on a minute, isn't that pretty much the same as having either a (Date, String) or a (Date, Int)? Yeah, pretty much.

So, we can say that (Date, String | Int) = (Date, String) | (Date, Int). In fact, since Pair is commutative like we showed before, we can even say that (String | Int, Date) = (String, Date) | (Int, Date).

This property has a really fancy name: distributivity. More concretely, we say that Pair distributes over Choice.

All these nice properties of these two types/operators culminate into one very neat structure: a rig.

The One Rig to Type them all

A rig (also known as a semiring), in the high marble palace of Abstract Algebra, is a special type of structure that has a few very specific properties. It consists of two operations, labeled $+$ (addition) and $×$ (multiplication), that act on some objects and satisfy the following properties:

Addition

• Associativity: $(a + b) + c = a + (b + c)$
• Commutativity: $a + b = b + a$
• Identity: $0 + a = a + 0$

Multiplication

• Associativity: $(a × b) × c = a × (b × c)$
• Identity: $1 × a = a × 1 = a$
• Annihilation: $0 × a = a × 0 = 0$

Peanut Butter and Chocolate

• Multiplication distributes over addition:
  • $a × (b + c) = (a × b) + (a + c)$
  • $(a + b) × c = (a × c) + (b + c)$

Now, if you've been paying close attention, you'll see that our Choice and Pair type operators do satisfy these properties. Namely, Choice takes the place of $+$, Pair of $×$, Unit of $1$, and Empty of $0$.

This is useful, because mathematicians and other smart people have studied rig's for some time now, and have proven some very convenient, and some outright cool properties.¹

To exemplify, let's write some equations.

Type equations

Let's look at the type List. As the name suggest, it represents all lists of some type. For example, List Int would be the type of all lists of integers.

The usual definition of List is the following:

• There is the empty list: []
• And there is a pair of an item and a list, that represents placing the item at the start of the list: cons

So we can write List as List A = Unit | (A, List A), where A is just some type, Unit stands in for the empty list (since there is only one), and (A, List A) for cons.

I'm going to be a little sneaky and replace all occurrences of Unit, Pair and Choice with the rig counterparts. That would make the type equation:

$$ \begin{align*} \text{List A} &= 1 + A\times\text{List A} \newline \end{align*} $$

Now, remember what I said about mathematicians and other smart people having already played around with rigs and found out a lot of nice properties? Well, one of the nice things we can do is "divide" as we wish, and as long as we get rid of the "divisions", in the end our equation will still be valid.

So let's do some shenanigans,

$$ \begin{align*} \text{List A} &= 1 + A\times\text{List A} \newline \text{List A} - A\times\text{List A} &= 1 \newline \text{List A}(1 - A) &= 1 \newline \text{List A} &= \frac{1}{1 - A} \newline \end{align*} $$

Now, this doesn't make much sense, but that's because we haven't cleaned up the division. To do that, we're going to expand it into a power series. If you're unfamiliar with power series, well, take a look, they're pretty cool, but for now, all you need to know is that we can expand this very particular form of division like so:

$$ \begin{align*} \text{List A} &= \frac{1}{1 - A} \newline \text{List A} &= \sum_{n = 0}^{\infty}A^n \end{align*} $$

Looks pretty weird, and complicated, so let's expand a couple of the terms

$$ \text{List A} = 1 + A + A^2 + A^3 + A^4 + ... $$

Now, let's think back on our type operators, Pair and Choice. What this equation is telling us is that a List A is either $1$, that is, the empty list [], or it's an element of A, or it's two elements of A, or it's three elements of A, or it's four elements of A, etc.

What this equation is doing, is enumerating all the possible lists of a given length.

• There is 1 list of length 0.
• There are #A lists of length 1.
• There are #A² lists of length 2.
• There are #A³ lists of length 3.
• There are #A⁴ lists of length 4.
• etc.

It's pretty cool that we were able to do this, even though the example is kind of trivial.

So let's tackle something more interesting than lists: Binary Trees

Binary Trees

This is the type usually used to represent binary trees: BinTree A = Unit | (A (BinTree A) (BinTree A)), where Unit stands for the empty tree, and (A (BinTree A) (BinTree A)) stands for a node with a type A and two, possibly empty, sub-trees.

When written in rig form:

$$ \begin{align*} \text{BinTree} \ A &= 1 + A \times \text{BinTree} \ A \times \text{BinTree} \ A \newline \text{BinTree} \ A &= 1 + A \times (\text{BinTree} \ A)^2 \newline \end{align*} $$

Alright, so let's rewrite this as a power series, by first trying to solve for BinTree A:

$$ \begin{align*} \text{BinTree} \ A &= 1 + A \times (\text{BinTree} \ A)^2 \newline A \times (\text{BinTree} \ A)^2 - \text{BinTree} \ A + 1 &= 0 \newline \text{BinTree} \ A &= \frac{1 \pm \sqrt{1 - 4A}}{2A}, \text{using the quadratic formula} \newline \end{align*} $$

Alright, this is pretty weird. But hey, we've solved for the type, we just need to find a way to expand this as a power series. Which is, well, hard.

First of all, the solution with the plus sign can't work, because when we take the limit as $A \rightarrow 0$ of the right hand side, that is, $ \frac{1 + \sqrt{1 - 4A}}{2A}$, we get $-1$, and we don't have $-1$ possible empty trees: we have $1$.

So, we need that the limit as $A \rightarrow 0$ of $\frac{1 + \sqrt{1 - 4A}}{2A}$ be $1$. Which... it is! Huzzah! (Feel free to work it out yourself)

Alright, so how do we expand $\frac{1 + \sqrt{1 - 4A}}{2A}$ as a power series? Well, it's pretty hard, and cumbersome, at least, so we outsource the heavy lifting to WolframAlpha.

If you do, you'll find that it expands to $1 + A + 2A^2 + 5A^3 + 14A^4 + ...$, instead of giving a general formula. So yeah, it must be pretty hard.

So... next step, to the OEIS! The OEIS (On-line Encyclopedia of Integer Sequences) is an absolute marvel of collaborative work that catalogs a whole bunch of integer sequences. You can give it some starting integers and it will try to find existing integer sequences from the few items you provided.

Slapping in the sequence $1$, $1$, $2$, $5$, $14$, (the coefficients on the power series expansion we found from WolframAlpha), we find the Catalan numbers! How exciting! Wait, what are they? (Opens up Wikipedia)

Ah, yes, it's a sequence of numbers associated with many (and I mean many) counting problems and recursive structures. The general term is $$ \begin{equation*} {\displaystyle C_{n}={\frac {1}{n+1}}{2n \choose n}={\frac {(2n)!}{(n+1)!n!}}=\prod \limits _{k=2}^{n}{\frac {n+k}{k}}\qquad {\text{for }}n\geq 0.} \end{equation*} $$

So yeah, pretty hard. Reading further into the Wikipedia page you'll see that the Catalan number's generating function solves the type equation we had previously written, so we can rest assured that the Catalan numbers are indeed the way to count binary trees.

From this we can conclude that there is one empty tree (seems about right), one tree with just one node (looking good so far), two trees with just two nodes (one left and one right, alright), then there are five trees with just three nodes (you can write them all out if you want), etc.

Wrapping Up

The Algebraic Data Types that you can create with Choice and Pair are plenty, even though I've only shown lists and binary trees, especially when you combine them with recursive type definitions, such as a list being either empty or a pair of an item and another list.

Along with their expressiveness, ADT's also have very nice algebraic properties as we've seen, such as being able to derive a method of counting the number of possible values of a certain "size" that a type can hold, such as lists of length ten, or binary trees with four nodes.