# 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⁸ = 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⁸ = 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.