A Proof that 0^0 = 1 using Type Algebra

… 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.¹

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

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.³ 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 Left and Rright:
  • 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.⁴ 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.

An Aside About Generics#

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 OmniMaps 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!.⁵

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.