… As taught by someone whose experience with type algebra consists of “figuring it out” and “being drip-fed things by Alwinfy.” This is going to be fast and loose.

Anyways. Type algebra is doing math on types. The core idea, I suppose, is that a type can be represented as an integer that is the number of possible values for the type.

That’s a weird idea, but let’s just try playing with it on some simple types. What about `bool`? There are two values, `true` and `false`, so `bool = 2`. We could imagine some kind of type with three states, which mathematicians call `Z3` (“Z sub 3”), and that would equal `3`, of course. `u8`, an unsigned 8-bit integer, would equal `2^8 = 256`.

Also, note that `i8`, a signed 8-bit integer, also equals `256`. Only the number of values matters in type algebra, not whatever the values might actually be. Because you can losslessly convert from `i8` to `u8` and back, in type algebra they’re considered the same.1

## Composing Types#

Now, of course in computer science we can combine types into other types. For example, we can do this:

``````struct MyType {
foo: bool,
bar: Z3,
}
``````

(I’m writing that in Rust, but the language doesn’t really matter.)

Now, let’s think about what integer is equivalent to `MyType`. We can enumerate the options pretty easily:

1. `{ foo: false, bar: 0 }`
2. `{ foo: false, bar: 1 }`
3. `{ foo: false, bar: 2 }`
4. `{ foo: true, bar: 0 }`
5. `{ foo: true, bar: 1 }`
6. `{ foo: true, bar: 2 }`

Alright, so `MyType = 6`.

What about a pair of `(bool, u8)`? Well, we have 256 options for the `u8`, and for each of them we can pick `true` or `false` for the `bool`. So it looks like `(bool, u8) = 2 * 256 = 512`.

Hang on a moment. We know that `bool = 2` and `u8 = 256`… and the size of `(bool, u8)`, 512, was the result of multiplying them together. Similarly, `MyType` equaled `6 = bool * Z3 = 2 * 3`.

So, in type algebra, making a struct is multiplication.

We can test this idea with some property-based tests. What do we know about multiplication? Casting back to grade school,

• Commutative property: `x*y = y*x`
• Associative property: `x*(y*z) = (x*y)*z`
• Distributive property: `x*(y+z) = x*y + x*z`
• Identity property: `x * 1 = x`
• Zero property: `x * 0 = 0`

We can’t test the last three properties because we don’t have an analogue for addition or the numbers 0 or 1 (yet). But let’s try out the other two:

• `MyType` would have 6 possible values no matter if it was defined with `foo` before `bar` or `bar` before `foo`.
• Let’s examine `(bool, (Z3, Z4))`. We know `(Z3, Z4)` has `12 = 3*4` possibilities (we could enumerate them if we want), and so `(bool, (Z3, Z4))` has `24 = 2*12`. And if we change that to `((bool, Z3), Z4)`, we already wrote all 6 possibilities for `(bool, Z3) = 6`. And that all multiplies together to `24 = 6*4`.

Alright! Now, if we could only find a nice analogue for addition.

## A Nice Analogue for Addition#

Well, let’s start by exploring around. We know, say, `2 + 3 = 5` in normal-math-land. So we need to do something to `bool` and `Z3` and end up with five possibilities.

We can go back to listing the possibilities outright, like we did way back at the beginning of the article.

• `bool`:
• `true`
• `false`
• `Z3`:
• `0`
• `1`
• `2`

… and hey wait a second. Let’s remove the type headers:

• `true`
• `false`
• `0`
• `1`
• `2`

And lookie here, we end up with five possibilities! It looks like the analogue of addition is picking one type or the other. So, `bool | Z3 = 2 + 3 = 5`.2

What about `Z3 | Z4`? That looks like it should just be 7, but if we write them out:

• `0`
• `1`
• `2`
• `0`
• `1`
• `2`
• `3`

… we have repeats. It looks like we need to consider numbers of different types to be completely different. Some languages (like Rust) do this; most (like C and Java) will automatically convert between numerical types sometimes. But in type algebra, the `0` from `Z3` and `0` from `Z4` have to be completely different.

As an argument for that, imagine that we did fold these things together. So, `Z2 | Z3` would have the values `0, 1, 2`, and would equal `3`. And `bool | Z3` would have the values `true, false, 0, 1, 2`, and would equal 5. But we know that `bool = Z2`, so we would have `3 = 5` … so we can’t have that. To avoid ambiguity, if it would be ambiguous I’ll mark them as `Z3(0)` and `Z4(0)` or whatever.

Anyone who’s coded in Rust (🚀🚀🚀) might recognize this addition operator as its enum construct. TypeScript coders might recognize it as its union types.3 And programmers of Haskell or OCaml might recognize it as an algebraic data type. Hey, it’s the same algebra as in type algebra!

Again, let’s try picking at some property based tests. Addition has the following properties:

• Commutative property: `x+y = y+x`
• Associative property: `x+(y+z) = (x+y)+z`
• Identity property: `x + 0 = x`
• (And the distributive property which we covered above)

We also don’t know a type for the number `0`, but let’s try out the other two:

• `bool | Z3 = Z3 | bool = 5`; it doesn’t matter which order we write the types in (`true, false, 0, 1, 2` vs `0, 1, 2, true, false`)
• `bool | (Z3 | Z4) = 2 + (3 + 4) = 7`; `(bool | Z3) | Z4 = (2 + 3) + 4 = 7`

Hey, that all seems to check out. Now, let’s tackle the distributive property. In other words, `(bool, (Z3 | Z4))` should equal `(bool, Z3) | (bool, Z4)`. Well, these types are all small enough that we can just enumerate them.

• `(bool, (Z3 | Z4))` has 14 possibilities:
• `true, Z3(0)`
• `true, Z3(1)`
• `true, Z3(2)`
• `true, Z4(0)`
• `true, Z4(1)`
• `true, Z4(2)`
• `true, Z4(3)`
• `false, Z3(0)`
• `false, Z3(1)`
• `false, Z3(2)`
• `false, Z4(0)`
• `false, Z4(1)`
• `false, Z4(2)`
• `false, Z4(3)`
• `(bool, Z3) | (bool, Z4)` also has 14 possibilities. I’ll label the options `L` and `R` for `L`eft and `R`right:
• `L(true, 0)`
• `L(true, 1)`
• `L(true, 2)`
• `L(false, 0)`
• `L(false, 1)`
• `L(false, 2)`
• `R(true, 0)`
• `R(true, 1)`
• `R(true, 2)`
• `R(true, 3)`
• `R(false, 0)`
• `R(false, 1)`
• `R(false, 2)`
• `R(false, 3)`

Nice! Now if only we had types for 0 and 1.

## Types for 0 and 1#

A type for `1` would have exactly one value. Not a lot of languages have this, but some do:

• Rust has the `()` type, pronounced “unit.”
• Java has the `Void` type, which can only ever be `null`.
• TypeScript lets you define “string types,” where the only valid value of that type is that particular string. Note that under type algebra all these string types are considered the same.

For this article I’ll call this `unit`. And we can play around with it: a struct `(T, ())` adds no more information to `T` that wasn’t already there. Hey look `x * 1 = 1`!

What about `0`? A type that has no values? What would you ever want that for?

Actually, it’s quite handy. Both Rust and TypeScript have this and call it `never`.4 It’s the type of things like exiting the program or throwing an exception. The secret sauce here is that both languages implicitly cast that type to anything else, which is OK because you can never have a value of that type. This lets you write type-checking code like:

``````const myNum: number = x !== 0
? x / 5                // type of this branch is number
: throw DivideByZero() // type of this branch is never, which we can pretend is a number because
// we'll never get to do anything with `myNum`
``````

But that’s the realm of actual computer science; we’re doing type algebra here. And we can test the additive identity with our new `never` type. What happens if we go `x + 0`? We get something like `T | never`. And look at that! We can’t actually have a `never`. so `T | never = T`.

We can also test the multiplicative zero property: what happens if we have a type `(T, never)`? Well, we can’t actually construct an instance of that type, because we would need to get a `never` somehow and we can’t. So, `(T, never)` has 0 values … and hey look, `x * 0 = 0`.

Let’s look at this type here.

``````enum MyEnum<T> {
TheType(T),
Boolean(bool),
}
``````

(If you don’t know rust, that’s how you would write the equivalent of `T | bool`. The `<T>` is a generic parameter, meaning you can put any type you like in there).

You know the drill, start plugging things into it:

• `MyEnum<Z3> = Z3 | bool = 3 + 2 = 5 `
• `MyEnum<bool> = bool | bool = 2 + 2 = 4`
• `MyEnum<u8> = u8 | bool | 256 + 2 = 258`

… hey, that looks an awful lot like the function `f(x) = x + 2`.

In type algebra, types with generics are functions.

## Exponentiation#

Now let’s get onto the thing I actually promised in the title of the article. What on earth could exponentiation represent?

Like we learned above, we’re going to want some generic type over two types, `T` and `U`, that somehow ends up exponentiating them.

Let’s look at a simple arithmetic example again, let’s say `3^2`. From grade school we know exponentiation is repeated multiplication, so this equals `3 * 3`. So we’re looking for something that will repeat `Z3` twice, like a struct that automatically has two fields.

Or how about `5^3`? That’s `5*5*5`, so we want something that has three fields of `Z5`. In fact, any `T^U` can be read as “something with the number `U` fields of type `T`”.

So we have every value in `U`, and a `T` associated with each one. What does that sound like? Well,

… it’s a `HashMap<U, T>`!

Well, almost. Most languages don’t require every `U` key to have an associated `T` value. So I’ll call the exponentiation function an `OmniMap`.

Let’s enumerate one of these `OmniMap`s to make sure we’re not completely barking up the wrong tree. What about checking `3^2`? That would be `OmniMap<bool, Z3>`.

• `{true => 0, false => 0}`
• `{true => 0, false => 1}`
• `{true => 0, false => 2}`
• `{true => 1, false => 0}`
• `{true => 1, false => 1}`
• `{true => 1, false => 2}`
• `{true => 2, false => 0}`
• `{true => 2, false => 1}`
• `{true => 2, false => 2}`

… and lo and behold there are 9 values!

We’re at the home stretch here! Let’s look at powers of 0. `0^3`, say, would be `OmniMap<Z3, never>`. Let’s go and construct that:

• `{0 => ... wait a minute }`

We can’t actually construct any values of `OmniMap<Z3, never>`, because in order to do so, we would need a value of type `never`. So, `0^3 = 0`.

Alright. We’re ready to tackle `0^0`. That would be `OmniMap<never, never>`. And … we can construct exactly one value of that type: the empty map, `{}`, with no keys and no values. And so, `0^0 = 1`. QED.

## Lightning Round#

The article proper’s over! But type algebra is so cool, here’s an unedited coredump of a bunch of other type algebra fun stuff.

### Functions Are Also Exponentiation#

This “omnimap” is actually the mathematical definition of a function; a mapping from one type to another. I chose to use omnimaps instead of functions for the example because I think it makes the `0^0` case easier to understand.

### Lists#

Lists are nice, easy types, right? What’s a list in type algebra? Well, let’s look at `List<bool>`:

• `[]`
• `[false]`
• `[false, false]`
• `[false, false, false]`

Whoops, looks like lists are infinite.

### Optional#

A lot of languages have an “optional” or “nullable” construct, meaning a value can be whatever value, or null. So, that’s adding one value to the number of values representable by the type.

Hey, how does Rust define its `Option<T>` type?

``````enum Option<T> {
Some(T),
None,
}
``````

AKA, `T | unit`.

### Orderings#

What about an ordering? That is, a list containing exactly one of each value of a type.

Well, for the first slot in the list, we have `T` options. For the next, we have `T-1` options, because one of them we already picked for the first slot. For the slot after that we have `T-2` … and so the total number of options for the ordering is `T * (T-1) * (T-2) * (T-3) * ... * 1`.

And that’s factorial! `Ordering<T> = T!`.5

Let’s examine the identity `(T + 1)! = (T + 1) * T!`. So, `Ordering<Z3> = (Z3, Ordering<bool>)`. And that’s the car/cdr definition of a list.

### You Can Take The Derivative Of Types#

http://strictlypositive.org/diff.pdf

I won’t pretend to understand this any more than you do.

1. Mathematicians call this “lossless conversion” function a “bijection,” as in “we can form a bijection from `i8` to `u8`.” ↩︎

2. I’m using TypeScript’s union type notation here, `T | U`. This is because Rust doesn’t let you define enums inline like this and I’ve never used Haskell. ↩︎

3. Actually, TypeScript will fold together identical types, so `number | number == number`. But I’ll ignore that. ↩︎

4. OK, Rust actually calls it `!`, but it’s pronounced `never`↩︎

5. An early version of this article was a proof that `0! = 1`. The proof is that an `Ordering<never>` has exactly one value, the empty list. ↩︎