ClickCease

ELI5: What is type theory?

Type theory is a difficult topic, and one that’s definitely challenging to explain to a 5 year old. But let’s give it a try. For sake of brevity, please read the prerequisite below.

Prerequisite: Read our ELI5: What is set theory?

Imagine that you have two universes. One is called “Universe of Sets” and the other is called “Universes of Types”. In each universes, you have a rocket with two wings. They are identical to one another.

You would say that: “There is a rocket with two wings in Universe of Sets. There is a rocket with two wings in Universe of Types.” This is a correct statement.

Now let’s add another identical rocket with two wings to each universe, and join this new rocket with the existing rocket. You now have one rocket with four wings, or two rockets with two wings each, in each universe. This is where the two universes diverge.

You would now say that: “There is a rocket with four wings in Universe of Sets. There are two rockets, where each rocket has two wings, in Universe of Types.”

As you can see, the object (i.e. the combined rocket) is the same in both universes. The difference is how we describe and view them. In Universe of Sets, we’ve “added” them together and now view them as one. However, in Universe of Types, we have joined the rockets together, and now view it as a new combined rocket.

ELI15: Extrapolating this to set theory and type theory

Let’s get a bit more technical with this analogy.

Set theory allows you do to arithmetic on objects. For example, adding { 1 } and { 2 } in set theory will give you { 1, 2 }. Now, you can also write { 1 } + { 2 } = { 1, 2 }. This is 100% correct.

But this is not the case in type theory.

Let 1 and 2 be types. You can think of types 1 and 2 as labels, where the type 1 means that something is of type 1. You can then try to “combine” them by some sort of arithmetic such as: 1 + 2. (Note that this doesn’t mean “adding types”, but rather “combining types”.)

Now let’s say that 1 + 2 = { 1 } + { 2 }, since we may want to see the addition of types in a similar notation as we would in set theory. However, 1 + 2 = { 1 } + {2 } != { 1, 2 }. Instead, 1 + 2, or { 1 } + { 2 }, is a new type, that is completely different from { 1, 2 }. They could be equivalent, but they are of different types in type theory.

This is where the concept of equivalent but not identical comes in. In set theory, if something is equivalent, they are identical. But in type theory, if something is equivalent, they may or may not be identical.

{ 1 } + { 2 } may be equivalent to { 1, 2 } in type theory, but they are not identical. Since they are not identical, they are of different types.

ELI18: Using integers and real numbers to demonstrate the differences between set theory and type theory

An integer is any whole number that can be positive, negative or zero. A real number is a number that can be used to measure any continuous quantity.

In set theory, you could say that “Integers and real numbers are both numbers”. So one could say that both integers and real numbers are subset of all numbers. That’s true.

But you cannot say that in type theory. “Integers and real numbers are two different types, and they have no relationship with numbers”. As far as we are concerned, integers and real numbers are two independent types, that do not have any relation with one another, because they have different properties.