- Published on

# What is the type of Type?

- Authors
- Name
- Aryan Ebrahimpour
- GitHub
- @avestura

- 10 min read

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 get the type of that type?
`typeOf(String) → ?`

. And even further, what is type of the type after it? (`typeOf(typeOf(String)) → ?`

)

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

```
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 }`

.

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

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

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:

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