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 dripfed 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 8bit integer, would equal 2^8 = 256
.
Also, note that i8
, a signed 8bit 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:
{ foo: false, bar: 0 }
{ foo: false, bar: 1 }
{ foo: false, bar: 2 }
{ foo: true, bar: 0 }
{ foo: true, bar: 1 }
{ 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 propertybased 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 withfoo
beforebar
orbar
beforefoo
. Let’s examine
(bool, (Z3, Z4))
. We know(Z3, Z4)
has12 = 3*4
possibilities (we could enumerate them if we want), and so(bool, (Z3, Z4))
has24 = 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 to24 = 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 normalmathland. 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
vs0, 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 optionsL
andR
forL
eft andR
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 benull
.  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 typechecking
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 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 T1
options, because one of them we already picked for the first slot.
For the slot after that we have T2
… and so the total number of options for the ordering is T * (T1) * (T2) * (T3) * ... * 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.

Mathematicians call this “lossless conversion” function a “bijection,” as in “we can form a bijection from
i8
tou8
.” ↩︎ 
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. ↩︎ 
Actually, TypeScript will fold together identical types, so
number  number == number
. But I’ll ignore that. ↩︎ 
OK, Rust actually calls it
!
, but it’s pronouncednever
. ↩︎ 
An early version of this article was a proof that
0! = 1
. The proof is that anOrdering<never>
has exactly one value, the empty list. ↩︎