What is the type of Type?

In many statically-typed languages, there is a typeof operator or a getType function which returns the type of a given value (e.g. typeOf("a") = String). But what happens if we try to determine the type of that type? In other words, what would typeof(String) return? And even further, what is type of the type after it? (typeOf(typeOf(String)) → ?)

Let's try that in a couple of popular programming languages:

csharp

Console.WriteLine("".GetType().Name);                     // String
Console.WriteLine("".GetType().GetType().Name);           // System.RuntimeType: System.Type
Console.WriteLine("".GetType().GetType().GetType().Name); // System.RuntimeType: System.Type

As you can see in the above code snippets, in many languages, type of a value returns its type (obviously), and then type of that type returns a type called Type (or a variant of it), and then type of that Type returns Type again, and the last step repeats forever.

However, this is not what happens in mathematically strong languages that are being used for theorem proving like Coq, Agda, or Idris. What we see there is that type of Type is Type 1, type of Type 1 is Type 2 and so on... But why is that?

Types and Sets

Types in programming languages come from a mathmatical theory, called Type Theory. A type theory is a formal system where every term has a type. In your favorite programming language, the term can be variables and the type, well, is the type of that variable. These theories are implemented as Type Systems in programming languages.

The languages mentioned in the previous section (Idris, Agda, Coq) use a type theory called Typed λ (Lambda) Calculus. Typed λ Calculus is closely related to mathematical logic, which has a subarea called Set theory. Set theory studies Sets, that are basically a collection of unique objects.

We can define the type Boolean as a set of { true, false }. That means a variable that is the type of Boolean, can either be true or false, and nothing else.

typescript

type Boolean = false | true

I can also have a set of values which the instances are themselves instance of other types/sets as well: { 1, "hello", false }.

typescript

type MySet = 1 | "hello" | false

const x : MySet = "bye"
// ---------------^
// Type check error: The set MySet does not contain the object "bye"

Naive Set Theory

There are multiple set theories that study sets. One of these theories is called Naive Set Theory which is one of the first things you face when learning about sets. As the name suggests, naive set theory is very simple and easy to understand. Unlike many other set theories that are defined using mathmatical formal logics and notations, naive set theory is defined in natural language: the language that humans speak.

This definition of sets goes back to Georg Cantor:

A set is a gathering together into a whole of definite, distinct objects of our perception or of our thought—which are called elements of the set.

– Georg Cantor, 1915

So we know what a Set is, we know Types are sets of values, what's all these Type 1, Type 2, ... about then?

Naive Set Theory doesn't work

The bad news is this simple and easy to understand Naive Set Thory has a bunch of flaws: it faces different contradictions and inconsistencies, and we don't like to encounter contradictions in our math.

We really want to keep it simple and straightforward, but oversimplifying something like Logic and Set theory which is complex by nature can be troublesome. Therefore, we need to look for other set theories that use a bunch of statements as rules, called Axioms. These axioms prevent us from falling in the trap of those contradictions.

"Hey! What are those contradictions you keep talking about? I still don't know why Naive set theory doesn't work!" you might ask, rightfully! But before answering that question in the next section, I want to quote the Good Math book by Mark C. Chu-Carrol:

Don't Keep It Simple, Stupid

There's an old mantra among engineers called the KISS principle. KISS stands for "Keep it simple, stupid!" The idea is that when you're building something useful, you should make it as simple as possible. The more moving parts something has, the more complicated corners it has, the more likely it is that an error will slip by. Looked at from that perspective, naive set theory looks great. It's so beautifully simple. [...]

Unfortunately, set theory in practice needs to be a lot more complicated. Why can't we stick with the KISS principle, use naive set theory, and skip that hairy stuff? The sad answer is, naive set theory doesn't work.

Russel's Paradox

Imagine the set $B$ where its elements are all the sets that are not the members of themselves.

B=\{x:x\not \in x\}

Can you see the paradox here?

If B isn't a member of itself, it should be a member of itself by its definition.
If B is a member of itself, it shouldn't be a member of itself by its definition.

The example above is a sample of Russel's paradox. However, Russel's Paradox is more general than the definition of the set $B$ we've talked about.

Russell's paradox shows that every set theory that contains an unrestricted comprehension principle (UCP) leads to contradictions. Here in the set $B$ , the predicate $¬(x ∈ x)$ is the UCP that causing the contradiction.

We don't enter the details of UCP and its general formula as we don't need it for the rest of the article. However we need to know that every set that defines these too open rules (UCPs) in their definition will face contradictions, and therefore we need some axiomatic set theories (instead of the naive ones.) that prevents us to face such contradictions.

Type Universes

As we've seen in the previous section, Russell’s paradox prevents us to accept the collection of all sets (let it be $M$ ) as a set itself, because then someone can define a subset of it called $A ⊆ M$ where $A$ equals to all sets that do not contain themselves.

Therefore a Set can not be a type of Set.

Set: Set // Leads to contradiction

Real world example

Imagine you want to define the cartesian product of multiple sets. Type definition of List is:

List<T> where T : Set returns Set =
    // member definitions...

and type signature of your product would look like something like this:

Prod : List Set → Set

However, there is a small problem here. Because the type definition of List asks A to be a type of Set, we already know that A can not be Set itself beacuse Set: Set is not valid. The solution is to define an special version of Set. This special version will be Set's own type, contains it and is larger than it.

List₁<T> where T : Set₁ returns Set₁ =
    // member definitions...

Prod : List₁ Set → Set

$Set_1$ is that special type which contains other types, and is called a Type Universe. The number 1 is its Universe Level.

Set_i : Set_{i+1}

In Agda and many other dependently typed languages, Type universes are built-in in the language. They either exist as a langugae construct as in Agda:

agda

open import Agda.Primitive

data List {n : Level} (A : Set n) : Set n where
  []   : List A
  _::_ : A → List A → List A

or are inferred by the language, and cannot be specified explicitly, as in Idris.

Conclusion

We've seen that type of Type in most of the statically typed language is Type itself; however this wasn't the case with logic based languages. We've investigated the reason and realized that having Type: Type will lead to contradictions in logic and set theories. After seeing the solution of the dependently typed languages, we learnt about Type Universes and the reason they can solve the issue of facing contradictions for proving theorems.

Discuss on Twitter