Type Theory

What is Type Theory?

A Type Theory is a system for classifying mathematical and computational objects by the kinds of things they are, and for governing how those objects can be combined and manipulated. Like Set Theory and Category Theory, Type Theory can be used as a foundation for mathematics.

There are many type theories, just like there are many set theories. We’ll see some later. Like modern set theories, type theories are designed to avoid the paradoxes of self-reference found in what is now called Naïve Set Theory.

The basic idea in type theory is that we bring objects into existence with their type, and define functions that manipulate (i.e., compute with) objects based on their type. Because every object has a type, the typing judgment

$ x\!: t $

(read “$x$ inhabits type $t$”) is central. New types are constructed carefully from existing types, avoiding paradoxes. Because functions are an integral feature rather than an afterthought, Type Theory has a naturally computational flavor, which makes it preferable, many say, as a foundation for computer science.

Roughly speaking, when Set Theory is used as a foundation for mathematics, we need a logical system to be in place to do our reasoning; with Type Theory, however, reasoning is done by deriving type judgments and evaluating functions within the system. Sometimes, functions return truth values, so evaluating them sure sounds like a proof. (It is.) We sometimes say “logic emerges from Type Theory.”

Logic emerges from Type Theory.

The Basics

Types are defined by exhaustive rules that create objects that inhabit the types. Let’s learn by example.

The Boolean Type

Here is our first type:

This definition states that the type $\textsf{Bool}$ is inhabited by exactly two individuals, $\textsf{true}$ and $\textsf{false}$. No more, no less. That’s what we mean when we say the rules are exhaustive. We have created two and only two inhabitants for this new type. Exhaustiveness is part of the structural metatheory. So too are the laws that define which rules we are allowed to make and which we cannot—we’ll cover them later.

Numbers

Here is the type of natural numbers:

This says “(1) $0$ is a natural number, (2) For any natural number $n$, $\mathsf{s\,}n$ is a natural number, and (3) nothing else is a natural number.” So the type of natural numbers is inhabited by $0$, $\mathsf{s\,}0$, $\mathsf{s\,s\,}0$, $\mathsf{s\,s\,s\,}0$, $\mathsf{s\,s\,s\,s\,}0$, and so on. We’ll write these as $0$, $1$, $2$, $3$, $4$, and so on. These abbreviations should be familiar to you. Next, here is the type of integers:

This type is inhabited by $\mathsf{pos\,}0$, $\mathsf{neg}\,(\mathsf{s}\,0)$, $\mathsf{pos}\,(\mathsf{s}\,0)$, $\mathsf{neg}\,(\mathsf{s\,s}\,0)$, $\mathsf{pos}\,(\mathsf{s\,s}\,0)$, $\mathsf{neg}\,(\mathsf{s\,s\,s}\,0)$, and so on. We’ll abbreviate these as $0$, $-1$, $1$, $-2$, $2$, $-3$, and so on. But what, then, is the type of $3$? We need to figure it out from context, or write $3_{\textsf{Nat}}$ or $3_{\textsf{Int}}$ to be explicit.

Here are the rationals:

So one-third is $\textsf{rat}\,1\,3$, which we can abbreviate as $\frac{1}{3}$.

We can build many more numeric types, including a few that are useful in programming languages, for example $\textsf{Int8}$, $\textsf{Int16}$, $\textsf{Int32}$, $\textsf{Int64}$, $\textsf{Int128}$, $\textsf{UInt8}$, $\textsf{UInt16}$, $\textsf{UInt32}$, $\textsf{UInt64}$, $\textsf{UInt128}$, $\textsf{Float16}$, $\textsf{Float32}$, $\textsf{Float64}$, $\textsf{Float128}$, and so on. Each of these have a finite number of elements, so, despite requiring a ridiculous number of rules, they can be defined in principle. (You could for example make your inhabitants in the Rust-style: e.g., -25i8, 32523u16, 8.23f64, etc.) So for example the signed 8-bit integer type is:

and the unsigned 8-bit integer type is:

Larger integer types and floats can be defined in a similar fashion, with thousands to quadrillions of rules (though there are clever ways to define them more succinctly). Floats will need special rules for $\textsf{NaN}$ and positive and negative infinities. Bounded complex numbers ($\textsf{Complex32}$, $\textsf{Complex64}$, $\textsf{Complex128}$, $\textsf{Complex256}$) can be defined as pairs of floats, for example:

Product Types

Now let’s build types from types. If $t_1$ and $t_2$ are types, then $t_1 \times t_2$ is a type, defined like so:

As a convention, we’ll take $\times$ to be right-associative, so the type expression $t_1 \times t_2 \times t_3$ sugars $t_1 \times (t_2 \times t_3)$, and, correspondingly, when writing inhabitants, $(a,b,c)$ sugars $(a,(b,c))$.

In general, $(a_1, \ldots, a_n)$, which sugars $(a_1, (a_2, (\ldots, (a_{n-1}, a_n)\ldots)))$, is called an $n$-tuple. Its length is $n$.

How nice: we can have variables for types, not just terms! Such types are polymorphic.

The Unit Type

So we have $2$-tuples and $3$-tuples and can keep going, as long as $n \geq 2$.

Can we go the other way?

Sure...a “$1$-tuple” would just have one component, which we can treat as the value itself, so $a = (a)$.

A “$0$-tuple” would look like this: $()$.

Let’s make that a value, and give it a type. Wait, people have already done this. The type is called $\textsf{Unit}$:

List Types

Next is the type “list of elements of type $t$” which we will write $t^*$:

We will write ${[x]}$ for $(x\,\textbf{::}\,[\,])$, ${[x,y,z]}$ for $(x\,\textbf{::}\,(y\,\textbf{::}\,(z\,\textbf{::}\,[\,])))$, and so on. For an empty list, we would need to rely on context to infer its type, or be explicit by writing, for example, $[\,]_{\textsf{Int}^*}$ or $[\,]_{(\textsf{Bool}\times\textsf{Unit})^*}$.

Map Types

Maps with key type $t_1$ and value type $t_2$ are inductively defined like so:

We will write:

• $\{\}$ for $\textsf{emptymap}$
• $m[k\mapsto v]$ for $\textsf{update}\;k\;v\;m$
• $\{k_1\!: v_1, k_2\!: v_2, \ldots, k_n\!: v_n\}$ for $\{\}[k_1\mapsto v_1][k_2\mapsto v_2]\cdots[k_n\mapsto v_n]$

Custom Types

We can make types. Here is one for primary colors:

You can define the type $\textsf{Unicode}$ whose inhabitants are, you guessed it, the characters of Unicode. That’d be a lot of rules! But it is indeed definable, as there are a finite number of such characters. You can do one rule for each of the 1,111,998 possible characters, something like:

Feel free to use the official character names instead of code points.

Types whose inhabitants have varying forms are easy to write. Here is a type for some simple two-dimensional shapes:

The idea is that $\mathsf{circle}\,5.0$ is a circle with radius 5.

Here is a type for “binary trees of type $t$”:

How about trees with any number of children?

The String Type

Imagine what the type $\textsf{Unicode}^*$ is. Got it? That’s right! We’ll use the abbreviation $\textsf{String}$ for this type.

Option Types

Now let’s do “option of type $t$” (also called an optional of type $t$) which we will write $t\texttt{?}$:

We thus have $\textsf{some}\:3\!:\mathsf{Nat}\texttt{?}$ and $\textsf{some}\:(-3,\textsf{true})\!:(\mathsf{Int \times Bool})\texttt{?}$. When writing $\textsf{none}$, we must rely on context to know which type is being referred to, or use subscripts to be explicit, e.g., $\mathsf{none_{Int?}}$.

Void

Here is something surprisingly quite useful: the empty type, $\textsf{Void}$, is the type with no inhabitants. As there are no inhabitants, there are no constructors, so no rules to write.

Don’t confuse Void and Unit

The type $\textsf{Void}$ has no inhabitants at all. The type $\textsf{Unit}$ has a single inhabitant, namely $()$.

This is despite the fact that some programming languages confuse the two, namely Swift, where $()$ inhabits the type Swift (unfortunately?) calls $\textsf{Void}$.

Subtypes

Philosophy question: should a thing inhabit just one type? Some mathematically-oriented theories impose this restriction. Pragmatically, though, it makes sense to allow things to be in more than one type. Like $3$. Why not let it inhabit $\textsf{Nat}$ and $\textsf{Int}$ and maybe even more numeric types? If we allow this, we would notice that every inhabitant of $\textsf{Nat}$ also inhabits $\textsf{Int}$. That is, $\textsf{Nat}$ is a subtype of $\textsf{Int}$, which we write:

$$ \textsf{Nat} \; \texttt{<:} \; \textsf{Int} $$

Conversely, $\textsf{Int}$ is a supertype of $\textsf{Nat}$.

Let’s get technical:

$t_1 \; \texttt{<:} \; t_2$ if and only if for every $v$ such that $v\!: t_1$, we have $v\!: t_2$.

Union and Intersection Types

If we allow individuals to inhabit multiple types, then it makes sense to define union types. The union $t_1 \mid t_2$ is inhabited by exactly all the inhabitants of $t_1$ and those of $t_2$. Yes, it’s possible for $t_1$ and $t_2$ to overlap. If we do allow $\textsf{Nat}\;\texttt{<:}\;\textsf{Int}$, then the type $\textsf{Nat} \mid \textsf{Int}$ is just $\textsf{Int}$.

But the type $\textsf{Int} \mid \textsf{String}$ is perhaps interesting. Maybe you can find a use for it?

In case you were wondering, yes, if you have union types, you can also have intersection types, also. We write them like this: $t_1\:\texttt{&}\:t_2$.

Are you getting set theory vibes?

Please calm down.

Types are not sets.

TYPES ARE NOT SETS.

We’ll talk about sets later. Please ffs do not let any preconceived notions of sets cloud your learning of the beauty of types. Keep. your. focus. on. types. TYPES!

That said, there does exist a body of work that exploits some of the similarity between types and sets. One is semantic subtyping, which you can read about in this seminal paper by Frisch, Castagna, and Benzaken. Rather than a thinking about a type being defined by its constructors (as $A+B$ is defined by $\mathsf{inl}$ and $\mathsf{inr}$), a type becomes a set of values, and $A \vee B$ is literally $[\![ A ]\!] \cup [\![ B ]\!]$, and similarly for the intersection type. The approach has several advantages, which you can read about in their paper. Check it out after you finish these notes.

Functions

To serve as a basis for computation, let alone for mathematics, we need to know more than which items inhabit which types. We need to know how the items behave. We specify behavior by defining functions on the types. We were introduced to functions briefly in our notes on mathematics for computation, where we saw this diagram:

To define a function, you show how to map each element of one type (the domain) to an element of another type (the codomain). If a function $f$ has domain $t_1$ and codomain $t_2$, then $f$ inhabits the type $t_1 \to t_2$. To apply or invoke the function $f$ on argument $x$, we write $f\,x$ or $f(x)$. To represent a function explicitly, we write:

$\lambda x_\alpha. e_\beta$

where $x$ is the parameter of the function, $\alpha$ is the type of the parameter, and $e$ is the expression that computes the output (of type $\beta$) based on $x$. Whenever the types are inferrable we can drop them. This is often the case for the body, but rarely the case for the parameter.

Matching

Generally, a function will compute different values depending on how the parameter is constructed. Remember the Boolean type? It has only two constructors, $\textsf{true}$ and $\textsf{false}$. The function for boolean negation, then, uses a case expression:

$ \lambda b_{\textsf{Bool}}. [\,b \ \Vert \ \textsf{true} \to \textsf{false} \mid \textsf{false} \to \textsf{true}\,] $

The type of natural numbers we saw above has two constructors: $0$ and $\textsf{s}$. Here is a function that computes whether its input is zero:

$ \lambda n_{\textsf{Nat}}. [\,n \ \Vert \ 0 \to \textsf{true} \mid \textsf{s}\,m \to \textsf{false}\,]$

There’s a convenient shorthand (syntactic sugar) for pattern matching on the parameter itself (which should be familiar to many programmers):

$ \lambda(\textsf{true} \to \textsf{false} \mid \textsf{false} \to \textsf{true})_{\textsf{Bool}\to \textsf{Bool}} $

$ \lambda(0 \to \textsf{true} \mid \textsf{s}\,m \to \textsf{false})_{\textsf{Nat}\to \textsf{Bool}} $

We can make our life a little easier by giving names to functions, for example:

$\textsf{not} =_{\small{\textrm{def}}} \lambda b_{\textsf{Bool}}.[\,b \ \Vert \ \textsf{true} \to \textsf{false} \mid \textsf{false} \to \textsf{true}\,]$

$\textsf{isZero} =_{\small{\textrm{def}}} \lambda n_{\textsf{Nat}}.[\,n \ \Vert \ 0 \to \textsf{true} \mid \textsf{s}\,m \to \textsf{false}\,] $

We can get fancy by moving the parameter to the left of the equals sign, like this:

$\textsf{not}\;b =_{\small{\textrm{def}}} [\,b \ \Vert \ \textsf{true} \to \textsf{false} \mid \textsf{false} \to \textsf{true}\,] $

$\textsf{isZero}\;n =_{\small{\textrm{def}}} [\,n \ \Vert \ 0 \to \textsf{true} \mid \textsf{s}\,m \to \textsf{false}\,] $

It’s more common, though, to break up the case expression and write a definition by cases. This can be quite readable, especially when we move the typing information to its own line:

$\begin{array}{l} \textsf{not}\!: \textsf{Bool} \rightarrow \textsf{Bool} \\ \textsf{not}\;\textsf{true} = \textsf{false} \\ \textsf{not}\;\textsf{false} = \textsf{true} \end{array}$

$\begin{array}{l} \textsf{isZero}\!: \textsf{Nat} \rightarrow \textsf{Bool} \\ \textsf{isZero}\;0 = \textsf{true} \\ \textsf{isZero}\;(\textsf{s}\,n) = \textsf{false} \end{array}$

Parameters can be tuples:

$\begin{array}{l} \textsf{and}\!:(\textsf{Bool} \times \textsf{Bool}) \rightarrow \textsf{Bool} \\ \textsf{and}\;(\textsf{true}, \textsf{true}) = \textsf{true} \\ \textsf{and}\;(\textsf{true}, \textsf{false}) = \textsf{false} \\ \textsf{and}\;(\textsf{false}, \textsf{true}) = \textsf{false} \\ \textsf{and}\;(\textsf{false}, \textsf{false}) = \textsf{false} \end{array}$

But since functions are objects, we can do without tuple parameters, and define functions more simply. Study this:

$\begin{array}{l} \textsf{and}\!: \textsf{Bool} \rightarrow (\textsf{Bool} \rightarrow \textsf{Bool}) \\ \textsf{and}\;\textsf{true} = \lambda b_{\textsf{Bool}}.\,b \\ \textsf{and}\;\textsf{false} = \lambda b_{\textsf{Bool}}.\,\textsf{false} \end{array}$

Make sure you understand why that works, then move on to this definition:

$\begin{array}{l} \textsf{or}\!: \textsf{Bool} \rightarrow (\textsf{Bool} \rightarrow \textsf{Bool}) \\ \textsf{or}\;\textsf{true} = \lambda b_{\textsf{Bool}}.\,\textsf{true} \\ \textsf{or}\;\textsf{false} = \lambda b_{\textsf{Bool}}.\,b \end{array}$

We can keep moving parameters to the left, squeezing out the lambda expressions:

$\begin{array}{l} \textsf{and}\!: \textsf{Bool} \rightarrow \textsf{Bool} \rightarrow \textsf{Bool} \\ \textsf{and}\;\textsf{true}\;b = b \\ \textsf{and}\;\textsf{false}\;b = \textsf{false} \end{array}$

$\begin{array}{l} \textsf{or}\!: \textsf{Bool} \rightarrow \textsf{Bool} \rightarrow \textsf{Bool} \\ \textsf{or}\;\textsf{true}\;b = \textsf{true} \\ \textsf{or}\;\textsf{false}\;b = b \end{array}$

We slipped in some sugar there: When writing function types, the arrow associates to the right, so $t_1 \rightarrow t_2 \rightarrow t_3$ is the same as $t_1 \rightarrow (t_2 \rightarrow t_3)$. And when writing function calls, application associates to the left, so $f\,x\,y$ is the same as $(f\,x)\,y$.

Not every function has to be defined with cases. Consider a function that adds two to its argument. In both the $0$ and $\textsf{s}\,n$ case, we prefix two successors so we can write:

$\textsf{plusTwo}\;n_{\textsf{Nat}} = \textsf{s}\;\textsf{s}\;n$

or:

$\begin{array}{l} \textsf{plusTwo}\!: \textsf{Nat} \rightarrow \textsf{Nat} \\ \textsf{plusTwo}\;n = \textsf{s}\;\textsf{s}\;n \end{array}$

Now let’s write the function $\textsf{plus}\;m$ that will add $m$ to its argument. Here we do have to use pattern matching. The idea is: $\textsf{plus}\;m\;0$ is just $m$, but if the argument is of the form $\textsf{s}\,n$, our result is $m+n+1$. The function will be recursive, but well-defined since the recursive portion operates on a component that is structurally smaller than the argument of the clause in which it appears:

$\begin{array}{l} \textsf{plus}\!: \textsf{Nat} \rightarrow \textsf{Nat} \rightarrow \textsf{Nat} \\ \textsf{plus}\;m\;0 = m \\ \textsf{plus}\;m\;(\textsf{s}\,n) = \textsf{s}\;(\textsf{plus}\;m\;n) \end{array}$

Multiplication is similar:

$\begin{array}{l} \textsf{times}\!: \textsf{Nat} \rightarrow \textsf{Nat} \rightarrow \textsf{Nat} \\ \textsf{times}\;m\;0 = 0 \\ \textsf{times}\;m\;(\textsf{s}\,n) = \textsf{plus}\;m\;(\textsf{times}\;m\;n) \end{array}$

Exponentiation:

$\begin{array}{l} \textsf{exp}\!: \textsf{Nat} \rightarrow \textsf{Nat} \rightarrow \textsf{Nat} \\ \textsf{exp}\;b\;0 = 1 \\ \textsf{exp}\;b\;(\textsf{s}\,e) = \textsf{times}\;b\;(\textsf{exp}\;b\;e) \end{array}$

This is cool, right? The function $\textsf{exp}\;2$ is the function that when given an argument, raises $2$ to that power.

Function names

Even though functions don’t have to have names, they sure make things more readable.

But there is another advantage. Writing recursive functions is much easier when they have names. Think about it. How might you write the $\textsf{plus}$ function on natural numbers without naming it?

For less-than, we pattern match both parameters:

$\begin{array}{l} \textsf{lt}\!: \textsf{Nat} \rightarrow \textsf{Nat} \rightarrow \textsf{Bool} \\ \textsf{lt}\;0\;0 = \textsf{false} \\ \textsf{lt}\;0\;(\textsf{s}\,n) = \textsf{true} \\ \textsf{lt}\;(\textsf{s}\,m)\;0 = \textsf{false} \\ \textsf{lt}\;(\textsf{s}\,m)\;(\textsf{s}\,n) = \textsf{lt}\;m\;n \end{array}$

For less-than-or-equal, we can use a wildcard parameter:

$\begin{array}{l} \textsf{le}\!: \textsf{Nat} \rightarrow \textsf{Nat} \rightarrow \textsf{Bool} \\ \textsf{le}\;0\;\_ = \textsf{true} \\ \textsf{le}\;(\textsf{s}\,m)\;0 = \textsf{false} \\ \textsf{le}\;(\textsf{s}\,m)\;(\textsf{s}\,n) = \textsf{le}\;m\;n \end{array}$

Subtraction on natural numbers has to cap differences at zero (e.g., $3 - 5 = 0$). This operation is sometimes called monus. The definition is recursive with two base cases:

$\begin{array}{l} \textsf{monus}\!: \textsf{Nat} \rightarrow \textsf{Nat} \rightarrow \textsf{Nat} \\ \textsf{monus}\;m\;0 = m \\ \textsf{monus}\;0\;(\textsf{s}\,n) = 0 \\ \textsf{monus}\;(\textsf{s}\,m)\;(\textsf{s}\,n) = \textsf{monus}\;m\;n \end{array}$

This operation gives us a nice way to make our less-than-or-equal function more concise:

$\begin{array}{l} \textsf{le}\!: \textsf{Nat} \rightarrow \textsf{Nat} \rightarrow \textsf{Bool} \\ \textsf{le}\;m\;n = \textsf{isZero}\;(\textsf{monus}\;m\;n) \end{array}$

Matching on integers is a little more complex, since there is a boundary between positive and negative numbers. We’ll not visit all the arithmetic operations, but we’ll show how the boundary is handled by implementing the successor and predecessor functions on integers::

$\begin{array}{l} \textsf{succ}\!: \textsf{Int} \rightarrow \textsf{Int} \\ \textsf{succ}\;(\textsf{pos}\;n) = \textsf{pos}\;(\textsf{s}\,n) \\ \textsf{succ}\;(\textsf{neg}\;(\textsf{s}\;0)) = \textsf{pos}\;0 \\ \textsf{succ}\;(\textsf{neg}\;(\textsf{s}\;(\textsf{s}\,m))) = \textsf{neg}\;(\textsf{s}\,m) \end{array}$

$\begin{array}{l} \textsf{pred}\!: \textsf{Int} \rightarrow \textsf{Int} \\ \textsf{pred}\;(\textsf{neg}\;n) = \textsf{neg}\;(\textsf{s}\,n) \\ \textsf{pred}\;(\textsf{pos}\;(\textsf{s}\;0)) = \textsf{pos}\;0 \\ \textsf{pred}\;(\textsf{pos}\;0) = \textsf{neg}\;(\textsf{s}\;0) \\ \textsf{pred}\;(\textsf{pos}\;(\textsf{s}\;(\textsf{s}\,m))) = \textsf{pos}\;(\textsf{s}\,m) \end{array}$

Now, some list functions. First length:

$\begin{array}{l} \textsf{length}\!: t^* \rightarrow \textsf{Nat} \\ \textsf{length}\;[\,] = 0 \\ \textsf{length}\;(x\,\textbf{::}\,y) = (\textsf{length}\;y) + 1 \end{array}$

And appending two lists:

$\begin{array}{l} \textsf{append}\!: t^* \rightarrow t^* \rightarrow t^* \\ \textsf{append}\;[\,]\;z = z \\ \textsf{append}\;(x\,\textbf{::}\,y)\;z = x\,\textbf{::}\,(\textsf{append}\;y\;z) \end{array}$

Reversing a list:

$\begin{array}{l} \textsf{reverse}\!: t^* \rightarrow t^* \\ \textsf{reverse}\;[\,] = [\,] \\ \textsf{reverse}\;(x\,\textbf{::}\,y) = \textsf{append}\;(\textsf{reverse}\;y)\;[x] \end{array}$

Mapping a function over a list (in other words, applying a function to each element of a list):

$\begin{array}{l} \textsf{map}\!: (t_1 \rightarrow t_2) \rightarrow t_1^* \rightarrow t_2^* \\ \textsf{map}\;f\;[\,] = [\,] \\ \textsf{map}\;f\;(x\,\textbf{::}\,y) = (f\;x)\,\textbf{::}\,(\textsf{map}\;f\;y) \end{array}$

Filtering a list:

$\begin{array}{l} \textsf{filter}\!: (t \rightarrow \textsf{Bool}) \rightarrow t^* \rightarrow t^* \\ \textsf{filter}\;p\;[\,] = [\,] \\ \textsf{filter}\;p\;(x\,\textbf{::}\,y) = \textsf{if}\;(p\;x)\;\textsf{then}\;(x\,\textbf{::}\,(\textsf{filter}\;p\;y))\;\textsf{else}\;\textsf{filter}\;p\;y \end{array}$

For your custom types, matching takes place on constructors as expected:

$\begin{array}{l} \textsf{area}\!:\textsf{Shape} \rightarrow \textsf{Float64} \\ \textsf{area}\;(\textsf{circle}\;r) = \pi r^2 \\ \textsf{area}\;(\textsf{rectangle}\;w\;h) = wh \\ \textsf{area}\;(\textsf{triangle}\;a\;b\;c) = \textsf{let}\;s = \frac{a + b + c}{2} \;\textsf{in}\; \sqrt{s(s-a)(s-b)(s-c)} \\ \end{array}$

$\begin{array}{l} \textsf{perimeter}\!:\textsf{Shape} \rightarrow \textsf{Float64} \\ \textsf{perimeter}\;(\textsf{circle}\;r) = 2 \pi r \\ \textsf{perimeter}\;(\textsf{rectangle}\;w\;h) = 2 (w + h) \\ \textsf{perimeter}\;(\textsf{triangle}\;a\;b\;c) = a + b + c \\ \end{array}$

The Conditional Function

One of the most useful functions is $\textsf{cond}$:

$\begin{array}{l} \textsf{cond}\!: \textsf{Bool} \rightarrow t \rightarrow t \rightarrow t \\ \textsf{cond}\;\textsf{true}\;x\;y = x \\ \textsf{cond}\;\textsf{false}\;x\;y = y \end{array}$

Composition

Have you ever noticed that greater-than and less-than-or-equal are opposites? And ditto for greater-than-or-equal and less-than. If we already have a definition for less-than, we can define greater-than-or-equal as:

$\begin{array}{l} \textsf{ge}\!: \textsf{Nat} \rightarrow \textsf{Nat} \rightarrow \textsf{Bool} \\ \textsf{ge}\;m\;n = \textsf{not}\;(\textsf{lt}\;m\;n) \end{array}$

This looks exactly like function composition, because it is, so we can even write:

$\begin{array}{l} \textsf{ge}\!: \textsf{Nat} \rightarrow \textsf{Nat} \rightarrow \textsf{Bool} \\ \textsf{ge}\;m\;n = (\textsf{not} \circ \textsf{lt})\;m\;n \end{array}$

And finally:

$\begin{array}{l} \textsf{ge}\!: \textsf{Nat} \rightarrow \textsf{Nat} \rightarrow \textsf{Bool} \\ \textsf{ge} = \textsf{not} \circ \textsf{lt} \end{array}$

This literally says ”greater-than-or-equal is not less-than.”

Sugar

Ok hold up! It’s time to introduce some notation to make things a bit more familiar. From now on, we’re going to use some sugar, writing:

$\begin{array}{lll} \neg b & \text{for} & \textsf{not}\;b \\ a \land b & \text{for} & \textsf{and}\;a\;b \\ a \lor b & \text{for} & \textsf{or}\;a\;b \\ a \supset b & \text{for} & \textsf{or}\;(\textsf{not}\;a)\;b \\ \textsf{if}\;b\;\textsf{then}\;x\;\textsf{else}\;y & \text{for} & \textsf{cond}\;b\;x\;y \\ n + 1 & \text{for} & \textsf{s}\;n \\ m + n & \text{for} & \textsf{plus}\;m\;n \\ m \times n & \text{for} & \textsf{times}\;m\;n \\ m^n & \text{for} & \textsf{exp}\;m\;n \\ m \uparrow\uparrow n & \text{for} & \textsf{tetrate}\;m\;n \\ m \lt n & \text{for} & \textsf{lt}\;m\;n \\ m \le n & \text{for} & \textsf{le}\;m\;n \\ m \gt n & \text{for} & \textsf{gt}\;m\;n \\ m \ge n & \text{for} & \textsf{ge}\;m\;n \\ a \,\mathtt{+\!+}\, b & \text{for} & \textsf{append}\;a\;b \\ \textsf{let}\;x = e\;\textsf{in}\;e' & \text{for} & (\lambda x.\,e')\;e \\ e'\;\mathsf{where}\;x = e & \text{for} & (\lambda x.\,e')\;e \end{array}$

Heck we’ll even write $xy$ for $x \times y$ except when it makes things too confusing.

Type Inference

When defining functions by cases, the type annotation on the function name gives us enough context to infer the types of the clauses in the definition. When the function stands alone, explicit type annotations are often necessary, especially when using operators that are overloaded across multiple types (e.g., $+$, $\times$, $\bmod$ across $\textsf{Nat}$, $\textsf{Int}$, $\textsf{Float64}$, etc.):

Sometimes, annotating only the parameters is sufficient, since the types of the bodies are often inferrable:

An alternative to explicitly providing type annotations is to rely entirely on context. Do so at your own risk. It’s sometimes okay in informal settings, but when programming or using automated proof assistants you can run into trouble, since the inferred type in these languages or systems might not be what you expect.

Polymorphic Functions

Here’s a fun one. Try to infer the type of $\lambda f. \lambda x. f(f(x))$. What do you think it is?

Well, $(\textsf{Int} \rightarrow \textsf{Int}) \rightarrow \textsf{Int} \rightarrow \textsf{Int}$ works. But so does $(\textsf{Float64} \rightarrow \textsf{Float64}) \rightarrow \textsf{Float64} \rightarrow \textsf{Float64}$. And so does $(\textsf{Bool} \rightarrow \textsf{Bool}) \rightarrow \textsf{Bool} \rightarrow \textsf{Bool}$. And so on.

To say that this function works on any type, we introduce type variables. The type is then $\forall \alpha. (\alpha \rightarrow \alpha) \rightarrow \alpha \rightarrow \alpha$. You don’t have to write the $\forall$ though. But it is a nice way to say, “you can substitute any type you like for the type variable $\alpha$.” We say this function is polymorphic.

We’ve actually seen quite a few polymorphic functions already.

Partial Functions

A partial function does not map every element of its domain to an element of its codomain. Type Theory doesn’t like partial functions. Fortunately, you can always find a corresponding total function. There are at least four ways to do it: (1) use the option type we saw above for the codomain, (2) use a custom type with an error value variant for the codomain, (3) use a union type for the codomain, adding in a distinct element (usually called $\bot$) to stand in when the operation is not defined, or (4) restrict the domain.

For option 3, we pre-define a type called $\textsf{Bottom}$ with one inhabitant, $\bot$:

$$\dfrac{}{\bot\!: \textsf{Bottom}}$$

We often abbreviate the type as $\bot$ despite the ambiguity. (It’s not too hard to resolve the ambiguity in context.)

Although we have not yet defined the type $\textsf{Real}$, let’s do all four approaches for $\lambda x_{\textsf{Real}}. \frac{1}{x}$ and $\lambda x_{\textsf{Real}}. \sqrt{x}$.

Let’s define some common list and map functions, comparing strategies 1 and 3:

Option-style	Union-style
$\begin{array}{l} \textsf{head}\!: t^* \rightarrow t\texttt{?} \\ \textsf{head}\;[\,] = \textsf{none} \\ \textsf{head}\;(x\,\textbf{::}\,y) = \textsf{some}\;x \end{array}$	$\begin{array}{l} \textsf{head}\!: t^* \rightarrow t \mid \bot \\ \textsf{head}\;[\,] = \bot \\ \textsf{head}\;(x\,\textbf{::}\,y) = x \end{array}$
$\begin{array}{l} \textsf{tail}\!: t^* \rightarrow t^*\texttt{?} \\ \textsf{tail}\;[\,] = \textsf{none} \\ \textsf{tail}\;(x\,\textbf{::}\,y) = \textsf{some}\;y \end{array}$	$\begin{array}{l} \textsf{tail}\!: t^* \rightarrow t^* \mid \bot \\ \textsf{tail}\;[\,] = \bot \\ \textsf{tail}\;(x\,\textbf{::}\,y) = y \end{array}$
$\begin{array}{l} \textsf{lookup}\!: k\to\mathsf{Map}\;k\;v \to v\texttt{?} \\ \textsf{lookup}\;k\;\{\} = \textsf{none} \\ \textsf{lookup}\;k\;m[k\mapsto v] = \textsf{some}\;v \\ \textsf{lookup}\;k'\;m[k\mapsto v] = \textsf{lookup}\;k'\;m \quad (k' \neq k) \end{array}$	$\begin{array}{l} \textsf{lookup}\!: k\to\mathsf{Map}\;k\;v \to v \mid \bot \\ \textsf{lookup}\;k\;\{\} = \bot \\ \textsf{lookup}\;k\;m[k\mapsto v] = v \\ \textsf{lookup}\;k'\;m[k\mapsto v] = \textsf{lookup}\;k'\;m \quad (k' \neq k) \end{array}$

We will sugar $\textsf{lookup}\;k\;m$ as $m(k)$.

Sums, Products, and Exponents

Here are two types, $C$ (for color, with 3 inhabitants $\mathsf{r}$, $\mathsf{g}$, and $\mathsf{b}$) and $D$ (for direction, with 2 inhabitants $\mathsf{l}$ and $\mathsf{r}$):

$$ \dfrac{}{\mathsf{r}\!: C} \quad\quad\quad \dfrac{}{\mathsf{g}\!: C} \quad\quad\quad \dfrac{}{\mathsf{b}\!: C} $$ $$ \quad\quad\quad \dfrac{}{\mathsf{l}\!: D} \quad\quad\quad \dfrac{}{\mathsf{r}\!: D} $$

The inhabitants of $C \times D$ are:

$ ( \mathsf{r},\mathsf{l}),\;(\mathsf{r},\mathsf{r}),\;(\mathsf{g},\mathsf{l}),\;(\mathsf{g},\mathsf{r}),\;(\mathsf{b},\mathsf{l}),\;(\mathsf{b},\mathsf{r}) $

Did you notice that $C$ has 3 inhabitants and $D$ has 2 inhabitants and $C\times D$ has $3 \times 2 = 6$ inhabitants? See why we call these product types? Right? RIGHT?

Since we have products, maybe we should have sums. We’d like $C + D$ to be a type with $3 + 2 = 5$ inhabitants. You might think a union would work, but wait, it doesn’t because the union ($C \mid D$) only has four elements: $\mathsf{r}$, $\mathsf{g}$, $\mathsf{b}$, and $\mathsf{l}$. A true sum type needs to have two distinct $\mathsf{r}$’s. We have to tag the “source” of each element of the sum. So the type $C+D$ has these inhabitants:

$ \mathsf{inl}\,\mathsf{r},\;\mathsf{inl}\,\mathsf{g},\;\mathsf{inl}\,\mathsf{b},\;\mathsf{inr}\,\mathsf{l},\;\mathsf{inr}\,\mathsf{r} $

In general, we define a sum type like so:

$$ \dfrac{x: t_1}{\textsf{inl}\:x\!: t_1 + t_2} \quad\quad \dfrac{x: t_2}{\textsf{inr}\:x\!: t_1 + t_2} $$

Read $\textsf{inl}$ as “inject left” and $\textsf{inr}$ as “inject right”.

Sum types are rarely used, because in practice, you would create a type with readable, meaningful constructor names.

As we did with product types in extending the notion of product to 0 elements yielding the unit type, extending the notion of sum to 0 elements yields the sum type over no types, which is...the type $\textsf{Void}$ referred to above!

Does this remind you of basic number theory?

Void is the empty sum type, the sum of no types, and has zero elements. Just like the number 0 is the sum over a list of no elements, the additive identity.

Unit is the empty product type, the product of no types, and has one element. Just like the number 1 is the product over a list of no elements. The multiplicative identity.

In some theories the void type is actually called $\mathbf{0}$ and the unit type is actually called $\mathsf{1}$.

So, we have sums and products, but what about exponential types? Could there be types $C^D$ and $D^C$? There are, and it’s kind of interesting what they turn out to be. Let’s list all the inhabitants of $C \rightarrow D$:

$\begin{array}{ll} (000) & \lambda(\mathsf{r} \to \mathsf{l} \mid \mathsf{g} \to \mathsf{l} \mid \mathsf{b} \to \mathsf{l}) \\ (001) & \lambda(\mathsf{r} \to \mathsf{l} \mid \mathsf{g} \to \mathsf{l} \mid \mathsf{b} \to \mathsf{r}) \\ (010) & \lambda(\mathsf{r} \to \mathsf{l} \mid \mathsf{g} \to \mathsf{r} \mid \mathsf{b} \to \mathsf{l}) \\ (011) & \lambda(\mathsf{r} \to \mathsf{l} \mid \mathsf{g} \to \mathsf{r} \mid \mathsf{b} \to \mathsf{r}) \\ (100) & \lambda(\mathsf{r} \to \mathsf{r} \mid \mathsf{g} \to \mathsf{l} \mid \mathsf{b} \to \mathsf{l}) \\ (101) & \lambda(\mathsf{r} \to \mathsf{r} \mid \mathsf{g} \to \mathsf{l} \mid \mathsf{b} \to \mathsf{r}) \\ (110) & \lambda(\mathsf{r} \to \mathsf{r} \mid \mathsf{g} \to \mathsf{r} \mid \mathsf{b} \to \mathsf{l}) \\ (111) & \lambda(\mathsf{r} \to \mathsf{r} \mid \mathsf{g} \to \mathsf{r} \mid \mathsf{b} \to \mathsf{r}) \\ \end{array}$

There are 8 of these, which is not coincidentally $2^3$, exactly the number of inhabitants of $D$ raised to the power of the number of inhabitants of $C$. Therefore, $C \rightarrow D$ is sometimes written $D^C$.

It works the other way, too. $D \rightarrow C$ can be written $C^D$, as it has $3^2 = 9$ inhabitants:

$\begin{array}{ll} (00) & \lambda(\mathsf{l} \to \mathsf{r} \mid \mathsf{r} \mapsto \mathsf{r}) \\ (01) & \lambda(\mathsf{l} \to \mathsf{r} \mid \mathsf{r} \mapsto \mathsf{g}) \\ (02) & \lambda(\mathsf{l} \to \mathsf{r} \mid \mathsf{r} \mapsto \mathsf{b}) \\ (10) & \lambda(\mathsf{l} \to \mathsf{g} \mid \mathsf{r} \mapsto \mathsf{r}) \\ (11) & \lambda(\mathsf{l} \to \mathsf{g} \mid \mathsf{r} \mapsto \mathsf{g}) \\ (12) & \lambda(\mathsf{l} \to \mathsf{g} \mid \mathsf{r} \mapsto \mathsf{b}) \\ (20) & \lambda(\mathsf{l} \to \mathsf{b} \mid \mathsf{r} \mapsto \mathsf{r}) \\ (21) & \lambda(\mathsf{l} \to \mathsf{b} \mid \mathsf{r} \mapsto \mathsf{g}) \\ (22) & \lambda(\mathsf{l} \to \mathsf{b} \mid \mathsf{r} \mapsto \mathsf{b}) \\ \end{array}$

And there you have it: function types are the exponential types. 🤯

In Type Theory, functions are exponential types. $A\to B$ is $B^A$.

Sets

Given a function $A$ of type $t \rightarrow \mathsf{Bool}$, gathering all of the inhabitants $x$ of type $t$ for which $A\,x = \textsf{true}$. That’s a set.

Yes, that’s what a set is in Type Theory.

It is that simple.

We can use set notation in Type Theory. Just remember those curly braces and other bits are just syntactic sugar for functions.

Type Notation	Set Notation	Explanation
$\lambda x_{\textsf{Nat}}.\,x\lt 1$	$\{0\}$	The function returns true only for $0$
$\lambda x_{\textsf{Nat}}.\,x\ge 2 \land x\le 5$	$\{2, 3, 4, 5\}$	The function returns true only for $2$, $3$, and $5$
$\lambda x_{\textsf{Nat}}.\,\textsf{true}$	$\mathbb{N}$	The function returns true only for all natural numbers
$\lambda x_{\textsf{Nat}}.\,x > 5$	$\{ x \in \mathbb{N} \mid x > 5 \}$	The function returns true only for all natural numbers greater than $5$
$\lambda x_{\textsf{Int}}.\,\textsf{true}$	$\mathbb{Z}$	The function returns true only for all integers
$\lambda x_t.\,\textsf{false}$	$\varnothing$	The function returns true for no arguments
$(A\,x)_{\textsf{Bool}}$	$x \in A$	The application returns true if and only if $x$ is in the set $A$

In Type Theory, sets are functions with codomain Bool.

Equality

If $x\!:\textsf{Nat}$, we know that $(x+5)\!:\textsf{Nat}$ and $(x\lt 5)\!:\textsf{Bool}$. But what is the type of $x = 5$? Woah! We have not defined equality yet. We never defined a function to determine equality and never stated what equality even meant. When doing foundations, you do not get this for free. The concept is philosophically deep.

How we get equality into our foundations varies by system. We’ll see details later, but can say that (1) in some type theories, like $Q_0$, it is just straight up defined as a primitive and many of its properties derived; and (2) in others, equality is...wait for it...a type.

For now, go ahead and use the notation $x = y$ when, you know, $x$ and $y$ have that reflexive, symmetric, and transitive relation you feel from experience. You probably don’t have feels for equality when $x$ and $y$ are functions, but here’s a good-to-know: in most type theories, two functions $f_{\alpha\to \beta}$ and $g_{\alpha\to \beta}$ are equal ($f=g$) if and only if $f\,x = g\,x$ for all $x\!:\alpha$.

Real Numbers

In computer science, we almost always approximate the real numbers using finite types like $\textsf{Float64}$ or $\textsf{Float128}$ (which contain $\textsf{NaN}$ and positive and negative infinities). But if Type Theory is to serve as a complete foundation for mathematics, it must be able to represent the true, exact mathematical continuum ($\mathbb{R}$). Can it?

Yes, but not with the simple, finite inductive definitions that we’ve seen earlier. Instead, we can adapt the approach we saw in Set Theory: defining a real number as a Dedekind Cut—the set of all rational numbers less than the real number we are interested in. In Type Theory, this means a real number is represented as a function of type $\textsf{Rat} \rightarrow \textsf{Bool}$.

However, not every random mapping of rationals to booleans is a valid real number. To make it precise, the function must be bundled with structural proofs showing that the cut is non-empty, bounded, downward closed, and contains no greatest element. This bundling relies heavily on dependent types which we will see soon. We will leave the dense mathematical details of these proofs to external research; you can begin by investigating how modern proof assistants rigorously formalize the continuum by exploring the standard library implementations of real numbers in systems like Rocq (formerly named Coq) or Lean’s Mathlib.

Programming Language Values

When we get to formally specifying the semantics of programming languages, we’ll need the notion a custom type to encompass the values that we would process in a programming language. Type Theory can help us. We could define a type $\textsf{Value}$ that encompasses all the primitive and composite types we care about. For example, we might try:

However, this definition is illegal.

To say that the type $\textsf{Value}$ is inhabited by, among other things, all sets of values, is straight up paradoxical. Cantor’s Theorem tells us there are more sets of values than there are values: $|A| \lt |\mathcal{P}(A)|$ for every $A$. Ditto for the type of functions: there must be more $A\to A$ inhabitants than $A$ inhabitants. The last two rules above are illegal.

The rules for $\textsf{set}$ and $\textsf{fun}$ are illegal because they are not strictly positive. Strict positivity is the condition that the type being defined does not appear on the left-hand side of a function arrow in any of the premises of its constructors. This is a syntactic check that prevents us from running into Cantor’s Theorem paradoxes.

Why is strict positivity required?

The function type $A \rightarrow B$ is the same as exponential $B^A$. When defining a type $C$, we are fine as long as $C$ appears only as a base ($C^A$), as we are safely multiplying or copying the type (like making pairs or arrays of $C$).

But if $C$ ever appears as an exponent ($A^C$), Cantor’s Theorem applies: $2^{|C|}$ is strictly larger than $|C|$, creating an immediate mathematical contradiction. Strict positivity says that the type $C$ being defined is forbidden from ever appearing “up” above the line as an exponent, no matter how deeply nested or buried inside a function expression it might be.

So how do we deal with a desire to have sets and functions as values in a programming language? This is something Dana Scott thought about deeply. He came up with a brilliant breakthrough: restrict the meaning of $A \rightarrow B$. Instead of letting it represent the type of all possible mathematical functions from $A$ to $B$, restrict it to the type of all continuous functions over partial orders. The space of all such continuous functions is drastically smaller than the full, unrestricted exponential space, allowing recursive function types to safely exist without hitting Cantor’s barrier. For the mathematical details on Scott’s construction, see this Handbook of Domain Theory.

Which rules are legal?

We’re now ready to state which rules are legal for defining types using inductive rules. There are two requirements: the set of rules must be (1) well-founded, i.e., every inhabitant must be buildable by a finite number of applications of the rules, and (2) strictly positive, i.e., has no premise containing the type being defined on the left-hand side of any function arrow.

We could also state there needs to be a finite number of rules, and that no rule has an infinite number of premises, and so on.

Uncountable types

It’s tempting to think that these rules force types to be inhabited only by a countable number of inhabitants, but this is not the case. Consider:

$$ \dfrac{s\!: \textsf{Unicode}^*}{\textsf{str}\,s\!: \textsf{Doc}} \quad\quad\quad \dfrac{f\!: \textsf{Nat}\to \textsf{Doc}}{\textsf{fun}\,f\!: \textsf{Doc}} $$

Both rules are strictly positive ($\textsf{Doc}$ is only ever the codomain of an arrow, never the domain), and both have exactly one premise. The definition is legal. And yet, $|\textsf{Doc}| = 2^{\aleph_0}$, the cardinality of $\mathbb{R}$.

The well-foundedness condition only requires that each individual inhabitant have a finite, well-founded derivation—and every element of $\textsf{Doc}$ genuinely does. It says nothing about how large, or how many stages, the type as a whole needs to be built up.

Summary of the Basic Types

Now let’s package things up in a slightly different, and more abstract, fashion—a useful exercise when building up a theory. As we build our catalog, we’ll add some new important information.

Here are some types shared by almost all constructive type theories:

• $\textsf{Void}$, sometimes written $\bot$, or $\textbf{0}$, is a type, called the empty type, the type of no inhabitants.
• $\textsf{Unit}$, sometimes written $()$, or $\textbf{1}$, is a type, called the unit type, the type of exactly one inhabitant.
• You can inductively define types with exhaustive (so the “nothing else is an inhabitant” is implicit) construction rules, for instance $\textsf{Bool}$, $\textsf{Nat}$, $\textsf{Int}$, $\textsf{Unicode}$, $\textsf{Float64}$, etc., provided the rules are well-founded and strictly positive.
• If $t_1$ and $t_2$ are types, then $t_1 \times t_2$ is a type, called a product type. It is the type of tuples $(a, b)$ where $a\!:\!t_1$ and $b\!:\!t_2$.
• If $t_1$ and $t_2$ are types, then $t_1 + t_2$ is a type, called a sum type. It is the type of values $\textsf{inl}\,a$ for $a\!:\!t_1$ and $\textsf{inr}\,b$ for $b\!:\!t_2$.
• If $t_1$ and $t_2$ are types, then $t_1 \rightarrow t_2$ is a type, known as a function type. It is the type of functions that take an argument of type $t_1$ and return a value of type $t_2$. Function types cannot be defined inductively, but they can be used to define other types in an inductive definition, e.g., $\dfrac{f\!: \textsf{Nat}\to \textsf{Bool}}{\textsf{predicate}\,f\!: \textsf{Filter}}$ is perfectly legal, since $\textsf{Filter}$ never appears inside $\textsf{Nat}\to \textsf{Bool}$.

The union type and intersection types we saw before do not exist in all type theories:

• If $t_1$ and $t_2$ are types, then $t_1 \mid t_2$ is a type, called a union type. It is the type of values that are either of type $t_1$ or of type $t_2$.
• If $t_1$ and $t_2$ are types, then $t_1\,\texttt{&}\, t_2$ is a type, called an intersection type. It is the type of values that are of both type $t_1$ and type $t_2$.

Each of the types above are either primitive or constructed from constituent types. Nice and clean.

But we can do more.

We can make a type dependent not just on another type, but upon a value. That’s a topic for the next section. It’s wild.

Dependent Types

Time for something cool.

Motivation

Remember our definition of the type “lists of type $t$”:

$$ \dfrac{}{[\,]\!: t^*} \quad\quad\quad \dfrac{x\!: t \quad y\!: t^*}{(x :: y)\!: t^*} $$

It says that the type of lists (of type $t$) is inhabited by lists of any length whatsoever. This means that the $\textsf{head}$ and $\textsf{tail}$ functions require an option type (like we saw above) or be defined to return a custom type with an error variant, or worse, just be undefined or crash on an empty list. Ditto for accessing an element out of bounds. Not only that, but this type gives us no guarantees that reversing a list preserves its length. If we could make types such as “lists of length $5$” or “lists of length $8$”, then all these functions could be made safe without needing complicated machinery or risking a crash.

But making a separate type for each $n$ is infeasible. We need a single expression that can make the type of lists of length $n$ for any given $n$—that is, a type dependent upon a value, not just on other types.

This can be done!

A First Dependent Type

Here is how to define $\mathsf{Vec}\;t\;n$, the type of length-$n$ vectors of $t$ (note that we normally use the term vector instead of list when talking about fixed-length sequences):

$$ \dfrac{}{\mathsf{nil}\!:\mathsf{Vec}\;t\;0} \quad\quad\quad \dfrac{x\!:t \quad\;\; y\!:\mathsf{Vec}\;t\;n}{(x :: y)\!:\mathsf{Vec}\;t\;(n+1)} $$

$\mathsf{Vec}\;t\;n$ is a dependent type, so named because the type “depends on” a term.

This is a crazy powerful idea. Look at everything we get.

• The vector length is now part of the type itself. For example $\textsf{Vec}\;\textsf{Nat}\;3$ is the type of all length-$3$ vectors of natural numbers, inhabited by vectors like $(2\!::\!(1\!::\!(3\!::\!\textsf{nil})))$. $\textsf{Vec}\;\textsf{Nat}\;5$ is a completely different type.
• Because $\textsf{Vec}\;t\;n$ for each different $n$ is a genuinely different type, $\textsf{Vec}\;t$, all by itself, is a mapping from $\textsf{Nat}$ to types—not a type itself, but a family of types indexed by a natural number.
• You cannot even write down a $\textsf{Vec}\;t\;3$ with four elements in it; there’s simply no rule that would let you derive it. This is wild: we’re getting to where we can capture some program correctness rules, that we thought might have to wait until runtime to check, in the compile-time (static) type checker!
• The operation to fetch the first element (remember the function we called $\textsf{head}$ above?) can be typed as $\mathsf{Vec}\;t\;(n+1) \rightarrow t$ (more precisely, $\Pi_{n:\textsf{Nat}} (\mathsf{Vec}\;t\;(n+1) \rightarrow t)$, as we’ll see below). The $n+1$ in the domain guarantees the sequence is non-empty at the type level with no runtime check needed, no option type needed for the codomain, and no special custom error type needed. Compare to $t^*$, where nothing stops you from asking for the first element of $[\,]$.

Dependent Types allow a compile-time type checker to find errors one would typically expect to occur at runtime.

More Examples

Besides $\textsf{Vec}\;t\;n$, here are a few more examples of dependent types.

• $\textsf{Fin}\;n$ is the type of natural numbers less than $n$. For example, $\textsf{Fin}\;3$ is inhabited by $0$, $1$, and $2$, but not $3$ or any larger number.
• $\textsf{Matrix}\;m\;n$ is the type of $m \times n$ matrices. For example, $\textsf{Matrix}\;2\;3$ is the type of $2$-by-$3$ matrices.
• Height-balanced trees of a given height
• The type of pairs in which the first element is a natural number $n$, and the type of the second element is $\textsf{Bool}$ if $n$ is even, and $\textsf{Nat}$ if $n$ is odd

A few more, with a slightly different flavor, that are handled differently in practice:

• The type of pairs of numbers whose first element is less than the second
• The type of pairs of numbers that add up to a specific number $n$
• The type of sorted lists
• The type of theorems of a logical system

A Definition

Definition time. A dependent type is a family of types $B$ indexed by terms $x\!:\!A$, that is, for each different $a\!:\!A$, $B(a)$ may be a genuinely different type. So $B$ is less of a type than a type family. Think of $B$ as a function from terms of type $A$ to types: for a given value $a$, $B(a)$ is a type.

In the example above, $\textsf{Vec}\;t$ maps natural numbers to types, and is a dependent type. For each specific $n$, $\textsf{Vec}\;t\;n$ is a distinct type representing vectors of length $n$, e.g., $\textsf{Vec}\;t\;3$.

You will frequently see functions that operate on dependent types, and pairs containing elements from a dependent type. These constructs have a special notation: $\Pi$ (dependent functions) will extend $\to$ and $\Sigma$ (dependent pairs) will extend $\times$.

Relax, the notation is not scary at all.

Dependent Function Types ($\Pi$)

$\Pi_{x:A} B$ is the dependent type of functions that, given $a\!:\!A$, return a term whose type is specifically $B[x\mapsto a]$. When $B$ doesn’t actually depend on $x$, $\Pi_{x:A} B$ is just $A \rightarrow B$, so $\Pi$ is a strict generalization of the ordinary function type.

Let’s look at the types of some common vector operations, and see how dependent types make them more precise.

What is the $\Pi$ for?

It’s just the notation that people use to denote dependent function types. It’s a binding operator, just like $\lambda$, $\forall$, and $\exists$ that you may have seen before. Without it, the $n$ would be free and just hanging there. The $\Pi$ makes it clear it’s a bound variable, and the type depends on it in a controlled way.

Ok, so yes, you may ask: “isn’t the $t$ also free?” We probably should have bound it too, something like $\Pi_{t:\textsf{Type}} \Pi_{n:\textsf{Nat}} (\mathsf{Vec}\;t\;(n+1) \rightarrow t)$, or we could use a simple $\forall$ like we saw above in our section on polymorphic types. It’s often elided in practice.

Dependent Pair Types ($\Sigma$)

$\Sigma_{x:A} B(x)$ is the dependent type of pairs $(a, b)$ where $a\!:\!A$ and $b\!:\!B(a)$, that is, the type of the second component depends on the value of the first. When $B$ doesn’t depend on $x$, $\Sigma_{x:A} B$ is just $A \times B$, so $\Sigma$ generalizes the ordinary pair type the same way $\Pi$ generalizes $\rightarrow$.

The classic example is a pair of a length $n$ and a vector of that exact length: $\Sigma_{n:\textsf{Nat}} (\textsf{Vec}\,A\,n)$.

So: $\Pi$ says “for every $a\!:\!A$, here’s a function that will produce something of the type $B(a)$ specific to that $a$.” $\Sigma$ says “here is some particular $a\!:\!A$, paired with a value of the type $B(a)$ specific to that $a$.” Hey...looks like $\Pi$ gives $\forall$ vibes and $\Sigma$ gives $\exists$ vibes. We’ll see soon that that is more than a coincidence.

Refinement Types

A refinement type is a subtype formed from its supertype by applying a restriction based on a value. A good example is “the positive naturals” which we write as $\Sigma_{n:\textsf{Nat}} (n > 0)$ — a pair of a number together with a proof that it’s positive. This only makes sense once you allow a proposition ($n > 0$) to appear as a type—something we’ll see how to do soon.

In Programming Languages

Think of the correctness and security implications of dependent types! You can encode invariants directly in a function’s type rather than checking them at runtime or just asserting them in a comment. A sort function can be typed to guarantee its output is a permutation of its input, a matrixMultiply function can be typed to reject mismatched dimensions at compile time, and so on.

There’s a deeper connection, though. It has to do with Propositions as Types, which is coming up next.

Propositions as Types

Much of our type theory discussion so far seems like more than just looking for foundations of mathematics and computer science. There’s something that looks pretty practical too. Type systems in programming languages seem to come from this idea. So does logical reasoning. There seems to be a connection here.

Perhaps you’ve heard of the Lean theorem prover / proof assistant / programming language? Or Rocq (formerly known as Coq)? Or HOL, Isabelle, Agda, or Idris? These systems and languages enable proofs that are so complex that they are beyond an individual human’s ability to produce in their lifetime. And they perform formal verification (i.e., full correctness proofs) on systems that are not allowed to fail (think medicine and avionics). Running programs in these languages prove theorems. This is starting to get interesting.

These systems are direct applications of Type Theory. Not Set Theory. Specifically, they come from a discovery of a deep relationship between logic, type theory, and computation. A relationship people figured out over time as they noticed some interesting similarities between these fields. Similarities that had to be more than coincidences:

The Logical Formula	which means	is like the type	which is
$F$	Falsity	$\textsf{Void}$	the empty type (sometimes written $\bot$)
$T$	Truth	$\textsf{Unit}$	the type with only one inhabitant $()$
$A \wedge B$	Conjunction (And)	$A \times B$	the pair type
$A \vee B$	Disjunction (Or)	$A + B$	the sum type
$A \supset B$	Implication	$A \rightarrow B$	the function type
$\forall x. ((x \in A) \supset B)$ where $x$ is free in $B$	Universal Quantification	$\Pi_{x: A} B$	the dependent function type
$\exists x. ((x \in A) \wedge B)$ where $x$ is free in $B$	Existential Quantification	$\Sigma_{x: A} B$	the dependent pair type

It turns out that you can prove a formula (in this context formulas and propositions are the same thing) by constructing an inhabitant of the corresponding type. Inferring the typing judgments is exactly the same as working through the logical inferences.

The fact that formulas corresponded directly with types was noticed by Haskell Curry and William Alvin Howard at various times during the 1930s through the 1960s. This observation is now known as the Curry-Howard Correspondence, or the Curry-Howard Isomorphism. Here’s a video showing why it is amazing:

The correspondence shows that not only:

Propositions are Types

but that:

Proofs are Programs

and further that:

Computation is Proof Normalization

Another video, which covers a bit more, including a worked out example:

To really go deeper and to see more technical details of this correspondence, you really need to read Philip Wadler’s detailed but very accessible paper on the subject.

Next, read the the Wikipedia page on the Curry-Howard Correspondence, to see not only the extent of the correspondence, but also to find how much hardcore computer research has come out of this discovery.

So propositions-as-types gives us the ability to make propositions such as $(x\lt 5)$ a type. But there’s something even deeper. Remember how we haven’t defined equality yet? Well we can make equality a type! It will have a single constructor:

$$ \dfrac{x\!: t}{\textsf{refl}\,x\!: (x = x)} $$

If you’re starting to “get” the correspondence (it’s fine if you are still getting used to it!), you’ll read this as saying that for any $x$ of type $t$, there is a proof of the proposition that $x$ is equal to itself. This is called reflexivity.

You’ll want to go deeper into Intuitionistic Type Theory to continue with this. This is enough for now. 😅

Universes

On the one hand, it seems like values and types are very different things. But we’ve been using $t$ in places as if it were a variable, but of a type. Can types be values of a type?

In our discussion of dependent function types, we mentioned that the free-floating $t$ was really a variable and needed to be bound with something like $\Pi_{t:\textsf{Type}} \Pi_{n:\textsf{Nat}} (\mathsf{Vec}\;t\;(n+1) \rightarrow t)$. For that to typecheck, $\textsf{Type}$ has to be a type whose inhabitants are types (like $\textsf{Bool}$ or $\textsf{Nat}$). Let’s try to define this type:

Every type we’ve built is an inhabitant of $\textsf{Type}$. So what type is $\textsf{Type}$ itself? You might say:

Okay that looks pretty suspicious. It feels like an instance of the same self-reference (“set of all sets”) that doomed Naive Set Theory. In fact, $\textsf{Type}\!:\!\textsf{Type}$ is inconsistent, as was shown in 1972 by Jean Yves Girard, who demonstrated that from that assumption, you can find an inhabitant of the empty type $\textsf{Void}$, which by Propositions-as-Types is the same as proving $F$. This is now known as Girard’s paradox. The original work was awesome but complex, and though simplified by Antonin Hurkens in 1995, is still too long to show here. As expected, it comes about by cleverly employing self-reference.

The way we get consistent type theories is the same way that some folks get consistent set theories: stratification. Instead of one self-swallowing $\textsf{Type}$, build an infinite tower of universes, each classified by the next one up:

$$ \dfrac{}{\textsf{Type}_i\!:\textsf{Type}_{i+1}} $$

So $\textsf{Bool}\!:\!\textsf{Type}_0$, and $\textsf{Type}_0\!:\!\textsf{Type}_1$, and $\textsf{Type}_1\!:\!\textsf{Type}_2$, and so on, forever. No universe is ever a member of itself, so the self-reference of Girard’s Paradox cannot occur.

We need to add one more rule so that values and types can live together in any universe they need to, namely cumulativity:

$$ \dfrac{t\!:\textsf{Type}_i}{t\!:\textsf{Type}_{i+1}} $$

Cumulativity says every universe’s inhabitants are also inhabitants of every universe above it.

AMBIGUOUS NOTATION ALERT

Writing the subscript every single time is unbearable, especially since you rarely care which level you’re at, so in practice, people just write $\textsf{Type}$, unsubscripted, and mean it ambiguously: “some $\textsf{Type}_i$, for whichever $i$ makes this typecheck.” This is known as typical ambiguity. It looks frightening because you see $\textsf{Type}\!:\!\textsf{Type}$. You just have to remember it abbreviates $\textsf{Type}_i\!:\!\textsf{Type}_{i+1}$ for some $i$.

Modern proof assistants make the convention rigorous instead of merely informal, under the name universe polymorphism: a definition like $\mathsf{Vec}$ is parameterized by an explicit level variable $i$, giving it a type like $\mathsf{Vec} : \Pi_{i:\mathbb{N}}\, \textsf{Type}_i \rightarrow \textsf{Nat} \rightarrow \textsf{Type}_i$, and each use site instantiates $i$ to whatever level is needed, with the typechecker solving for consistent levels behind the scenes.

Do be careful with the terminology. A universe is one level (a $\textsf{Type}_i$ for some specific $i$). The cumulative hierarchy is the whole tower, $\textsf{Type}_0, \textsf{Type}_1, \textsf{Type}_2, \ldots$. Unsubscripted $\textsf{Type}$ is a placeholder standing for one unspecified universe in the hierarchy, resolved by context or by the typechecker.

Type Theories Throughout History

Just like there are many set theories, there are quite a few type theories. Here is a catalog placed into a rough timeline:

Russell’s Theory of Types

(1908) Bertrand Russell’s paper Mathematical logic as based on the theory of types, introduced a “ramified” theory of types—meaning that the theory stratifies types into levels (based on whether the object is an individual, a property, or a property of properties) and further subdivided them into orders (ramification). He did this to resolve Russell’s Paradox by ensuring a set can never contain itself or be defined in terms of a totality it belongs to. He wanted all definitions to be predicative. But this was too restrictive! He had to introduce the clunky “axiom of reducibility” just to recover ordinary mathematics (like natural numbers), so no one uses it anymore, but it’s the historical root of everything that follows.

Simple Theory of Types

(Ramsey, 1925; later streamlined by Tarski) A simplification of Russell’s theory that drops the orders and keeps only the type hierarchy, eliminating the need for the axiom of reducibility. While it admits impredicativity, it is vastly more useful: one needs only a stack of types $T_0, T_1, T_2, \ldots$ where each type’s members are sets of the type below it. Every other subsequent type theory recognizes this.

Exercise: Define predicative and impredicative. Why is impredicativity considered more useful in practice? And how to we make it okay?

Church’s Simple Theory of Types (STT)

(1940) Alonzo Church combined his untyped lambda calculus with a simple type discipline, partly to avoid the usual paradoxes. He made Type Theory interesting again! Before Church, people found Zermelo’s work on Set Theory to be just too good, so Type Theory had been somewhat neglected. STT was powerful, useful, elegant, and the direct ancestor of every typed programming language! Really!

System F / The Polymorphic Lambda Calculus

(Girard, 1972; independently, Reynolds, 1974) Jean-Yves Girard (for proof theory) and John Reynolds (for programming languages) independently extended simply typed lambda calculus with universal quantification over types, giving parametric polymorphism, which you might sometimes hear called generics. This is the theoretical basis for polymorphism in the ML family of languages (including Haskell), and (in a restricted form) Java’s and C#’s and Rust’s generics.

Martin-Löf Type Theory (MLTT)

(Per Martin-Löf, 1972 onward) An elegant and highly influential intuitionistic type theory that takes dependent types ($\Pi_{x:A} B$ and $\Sigma_{x:A} B$) as primitive, intended as a full foundation for constructive mathematics. MLTT is the direct ancestor of dependently typed proof assistants like Agda and, via the Calculus of Constructions, Rocq.

Andrews’ $Q_0$ and $Q_0^{\infty}$

(Peter Andrews, 1986, refined in the 2nd edition, 2002) A simply-typed higher-order logic descending directly from Church’s 1940 simple theory of types, with a more minimal basis—fewer symbols, fewer axioms, and fewer rules—everything is built from equality! Unlike MLTT and CoC, $Q_0$ stays classical (not constructive) and non-dependent, making it a useful counterpoint to intuitionistic and dependent theories which dominate the field.

The Calculus of Constructions (CoC)

(Coquand and Huet, 1988) Combines Martin-Löf-style dependent types with System F-style polymorphism into a single, very expressive type theory. It’s the theoretical core of the Rocq (formerly Coq) proof assistant.

Homotopy Type Theory (HoTT)

(Developed through the 2000s, crystallizing around 2006–2013, with Vladimir Voevodsky’s univalence axiom as a key turning point) Reinterprets Martin-Löf’s identity types through the lens of Homotopy Theory, where types are spaces, terms are points, and equalities are paths. This is the newest major branch. There is a very well-known book on this topic.

Case Studies

Let’s look at some type theories. We’ll see two main flavors: (1) Church’s STT, Andrews’ $Q_0$ and $Q_0^{\infty}$, and HOL, which are classical and non-dependent, and (2) Martin-Löf Type Theory, the Calculus of Constructions, and Homotopy Type Theory, which are constructive and dependent. The first group are built like logical systems that have types on terms; the latter build up universes according to the ways we’ve seen above.

Church’s Simple Type Theory

Church’s type theory was introduced in this awesome paper from 1940.

In it, Church presents a type theory from which classical logic emerges. Despite an extremely minimal notation, his system allows logic, sets, and numbers to be represented. We won’t go over his theory here, because there’s a direct successor worth looking at.

Andrews’ $Q_0$

Peter Andrews was a student of Church’s. His $Q_0$ is pretty much the same as Church’s Simple Type Theory, but with a smaller basis. Instead of defining a handful of constants, he builds everything from functions and the notion of equality. Impressive!

Syntax

Here’s the syntax, modernized a bit so the function type $(\beta\alpha)$ is now $\alpha \to \beta$, and $\iota$ is now $\textsf{the}$.

Some vocabulary:

• $\imath$ is the type of individuals.
• $o$ is the type of truth values.
• $(\alpha\to\beta)$ is the type of functions from type $\alpha$ to type $\beta$.
• $(F\,A)$ is an application of term $F$ to term $A$.
• $(\lambda x. B)$ is an abstraction, representing a function with parameter $x$ and body $B$.

We can express various objects and formulae from our earlier notes on Logic:

• $r_\imath$ is Romeo from the type of individuals
• $j_\imath$ is Juliet from the type of individuals
• $R_o$ is the proposition “It is raining” (note its type!)
• $I_{\imath\to o}$ is the predicate “is Italian”—a particular function from individuals to truth values
• $L_{\imath\to(\imath\to o)}$ is “likes”
• ($L_{\imath\to(\imath\to o)}r_\imath)_{\imath\to o}$ is a function, that when given an individual, will produce whether Romeo likes that individual
• (($L_{\imath\to(\imath\to o)}r_\imath)_{\imath\to o} j_\imath)_o$ is the truth value of “Romeo likes Juliet”

Some allowable sugar:

• The $\to$ in function types is right associative, so $\alpha \to \beta \to \gamma$ is interpreted as $\alpha \to (\beta \to \gamma)$ rather than $(\alpha \to \beta) \to \gamma$.
• Application is left associative, so $A\,B\,C$ is interpreted as $((A\,B)\,C)$ rather than $(A\,(B\,C))$.
• You can drop type symbols only when it is absolutely clear and unambiguous from the context what the types should be

Some of the conventional logical operators seem to be missing from the syntax, but that’s only because they are really just abbreviations, or sugar, for other terms. Here are the common ones, defined in order, since later ones may depend on earlier ones.

Term	What it sugars	Intuition
$A_\alpha = B_\alpha$	$\textsf{Q}_{\alpha\to \alpha\to o}A_\alpha B_\alpha$	Equality is primitive
$A_o \equiv B_o$	$A_o = B_o$	Material equivalence is just boolean equality
$T_o$	$\textsf{Q}_{o\to o\to o}=\textsf{Q}_{o\to o\to o}$	$\textsf{Q}$ equals itself is true
$F_o$	$(\lambda x_o.\,T_o) = (\lambda x_o.\,x_o)$	These two functions are not equal
$\forall x_\alpha.\, A_o$	$(\lambda x_\alpha.\,T_o) = (\lambda x_\alpha.\,A_o)$	For these functions to be equal, $A$ must be true for all $x_\alpha$
$A_o \land B_o$	$\lambda f_{o\to o\to o}. f\,T\,T = \lambda f_{o\to o\to o}. f\,A\,B$	Only way so far to get “both of these are true”
$A_o \supset B_o$	$A = (A \land B)$	Material implication
$\neg A_o$	$A_o = F_o$	Negation
$A_o \lor B_o$	$\neg(\neg A \land \neg B)$	De Morgan way to get “$A$ or $B$”
$\exists x_\alpha. A_o$	$\neg(\forall x_\alpha. \neg A)$	There exists at least one $x_\alpha$ such that $A$ holds
$A_\alpha \neq B_\alpha$	$\neg(A_\alpha = B_\alpha)$	Not equals
$\exists_1 x_\alpha. A_o$	$\exists x_\alpha. \forall y_\alpha. A[x\mapsto y] \equiv y = x$	There exists exactly one $x_\alpha$ such that $A$ holds
$\iota x_\alpha. A_o$	$\textsf{the}_{(\alpha\to o)\to \alpha} (\lambda x_\alpha. A)$	The unique element $x_\alpha$ such that $A$ holds, if it exists

Hilbert-style Axiomatization

Andrews axiomatized this theory in what’s known as the Hilbert style: separating axioms and inference rules, defining both without hypothetical judgments. His axioms are:

He has only one rule of inference:

In his book, Andrews shows how all of the theorems and rules of first-order logic are derived from these five simple axioms and single rule!

Remember why this is interesting

In Set Theory, we assumed first-order to already exist (with its own axioms and inference rules), then gave approximately 10 axioms to define what sets were and how to make new sets. Do you remember the axioms? Can you recite them?

In the Type Theory $Q_0$, we need only define what a function is and how it behaves, then we define all of the logical operators as functions (in many cases, just as sugared expressions). Functions first, then logic.

Gentzen-style Inference Rules

Let’s translate from Andrews’ Hilbert-style presentation of his theory to the Gentzen-style display of inference rules that we’ve encountered before:

The notation $\mathcal{C}[\ldots A_\alpha \ldots]$ in a rule premise denotes a term $\mathcal{C}$ in which a single, distinguished occurrence of the subterm $A_\alpha$ has been singled out. $\mathcal{C}[\ldots B_\alpha \ldots]$ in a rule conclusion means the same term $\mathcal{C}$ with that one occurrence of $A_\alpha$ replaced by $B_\alpha$, provided that no binder binds a free variable of $A$ or captures a free variable of $B$. Any other occurrences of $A_\alpha$ elsewhere in $\mathcal{C}$ are left alone.

Make sure you understand both provisos on replacement notation. When trying to use $A=B$ to replace an $A$ occurrence with a $B$ occurrence:

• No free variable of $A$ must be in the scope of a binder. You cannot use $bc=z$ for replacement into $\lambda c.abcd$ since the $c$ in the body is not replaceable—it’s tied to the $\lambda c$.
• No free variable in $B$ must be captured. You cannot use $b=cz$ for replacement into $\lambda c.abcd$ since the resulting $\lambda c.aczcd$ means something different.

A note on the translation

In converting from the original Hilbert-style to the Gentzen style, we took a few liberties. We’ve (1) added structural inference rules for convenience in managing hypotheses, (2) split Axiom 3, the equation $(f = g) = \forall x_\alpha.\,f\,x = g\,x$, into two directional rules ABS and EXT, (3) replaced Axiom 1 stating there are only two boolean values ($gT_o \land gF_o = \forall x_o.\,gx$) with CASES, and (4) introduced our own R rule as a mashup of his Rule R and his derived rule RR. The resulting system proves the same theorems.

This is a bold statement that we are offering without proof, so you are invited to show the equivalence between the two presentations!

Here’s an explanation for each rule:

• $\textbf{BETA}$: Applying a function to an argument yields the value of the function’s body with the argument substituted for the parameter.
• $\textbf{R}$: If two terms are equal, then any property that holds of one should hold of the other. This is Leibniz’s law.
• $\textbf{ABS}$: Equal bodies give equal functions. This is what lets us generalize: it is the only rule that can build an equation between two abstractions whose bound variable actually occurs in the body.
• $\textbf{EXT}$: Two functions are equal if they yield equal outputs for all inputs, i.e., extensionally equal.
• $\textbf{CASES}$: If a desired conclusion $B$ holds when a proposition $A$ is assumed True, and the same conclusion $B$ holds when $A$ is assumed False, then $B$ holds unconditionally.
• $\textbf{DESC}$: If there exists exactly one element that satisfies a property, then that element can be denoted with a description.

Derived Rules of Inference

All of the rules from propositional and predicate logic above are derived rules in $Q_0$. Let’s go through just a few. When using rule R, we’ll underline the occurrence being replaced. We’ll used dashed lines when all we are doing is sugaring or desugaring.

We’ll begin by deriving rules that allow us to use the basic equality rules: reflexivity, symmetry, and transitivity. Then we’ll continue to some of the familiar rules you know from propositional and predicate logic, introducing a few convenient rules along the way.

REFL $\frac{}{\vdash A_\alpha = A_\alpha}$

SYM $\frac{\mathcal{H} \vdash A_\alpha = B_\alpha}{\mathcal{H} \vdash B_\alpha = A_\alpha}$

TRANS $\frac{\mathcal{H_1} \vdash A_\alpha = B_\alpha \quad \mathcal{H_2} \vdash B_\alpha = C_\alpha}{\mathcal{H_1}, \mathcal{H_2} \vdash A_\alpha = C_\alpha}$

APPLY $\frac{\mathcal{H} \vdash F = G}{\mathcal{H} \vdash FA = GA}$

TRUE-INTRO $\frac{}{\vdash T}$

NEG-ELIM (FALSE-INTRO) $\frac{\mathcal{H_1} \vdash \neg A \quad \mathcal{H_2} \vdash A}{\mathcal{H_1}, \mathcal{H_2} \vdash F}$

EQ-T-ELIM $\frac{\mathcal{H} \vdash A = T}{\mathcal{H} \vdash A}$

FALSE-ELIM $\frac{\mathcal{H} \vdash F}{\mathcal{H} \vdash A}$

EQ-T-INTRO $\frac{\mathcal{H} \vdash A}{\mathcal{H} \vdash A = T}$

EQ-T-INTRO-HYP: $\frac{\mathcal{H},\, A \vdash C}{\mathcal{H},\, A = T \vdash C}$

NEG-INTRO $\frac{\mathcal{H},\,A \vdash F}{\mathcal{H} \vdash \neg A}$

AND-INTRO $\frac{\mathcal{H_1} \vdash A\quad\mathcal{H_2} \vdash B}{\mathcal{H_1}, \mathcal{H_2} \vdash A \land B}$

AND-ELIM-1 $\frac{\mathcal{H} \vdash A_o \land B_o}{\mathcal{H} \vdash A_o}$

AND-ELIM-2 $\frac{\mathcal{H} \vdash A_o \land B_o}{\mathcal{H} \vdash B_o}$

OR-INTRO-1 $\frac{\mathcal{H} \vdash A}{\mathcal{H} \vdash A \lor B}$

Left as an exercise for you

OR-INTRO-2 $\frac{\mathcal{H} \vdash B}{\mathcal{H} \vdash A \lor B}$

Left as an exercise for you

OR-ELIM $\frac{\mathcal{H_1} \vdash A \lor B \quad \mathcal{H_2},\,A \vdash C \quad \mathcal{H_3},\,B \vdash C}{\mathcal{H_1}, \mathcal{H_2}, \mathcal{H_3} \vdash C}$

Left as an exercise for you

FALSE-AND $\frac{}{F = F \land A}$

Left as an exercise for you

AND-TRUE $\frac{}{A = A \land T}$

Left as an exercise for you

IMPL-ELIM (MP) $\frac{\mathcal{H_1} \vdash A \supset B \quad \mathcal{H_2} \vdash A}{\mathcal{H_1}, \mathcal{H_2} \vdash B}$

IMPL-INTRO (CP) $\frac{\mathcal{H},\,A \vdash B}{\mathcal{H} \vdash A \supset B}$

UNIV-ELIM (SPEC): $\frac{\mathcal{H} \vdash \forall x_\alpha.\,A}{\mathcal{H} \vdash A[x_\alpha \mapsto t_\alpha]}$ where $t_\alpha$ is free for $x$ in $A$

UNIV-INTRO (GEN) $\frac{\mathcal{H} \vdash A}{\mathcal{H} \vdash \forall x_\alpha.\,A}$ where $x_\alpha$ is not free in $\mathcal{H}$

Did you notice GEN is basically ABS? Do you see why it is? Why it should be?

EXISTS-INTRO $\frac{\mathcal{H} \vdash A[x \mapsto t]}{\mathcal{H} \vdash \exists x_\alpha.\,A}$

TODO: Derive using the definition $\exists x. A \equiv \neg\forall x.\neg A$ and NEG-ELIM/GEN mechanics.

EXISTS-ELIM $\frac{\mathcal{H}_1 \vdash ∃ x_\alpha. A \quad\;\; \mathcal{H}_2,\,A[x \mapsto y] \vdash C}{\mathcal{H}_1, \mathcal{H}_2 \vdash C}$ where $y$ is not free in $\mathcal{H}_1$, $\mathcal{H}_2$, $C$, or $\exists x_\alpha. A$

TODO: Fill out the proof tree by combining the hypothetical subproof with INDIRECT-PROOF.

DESC-SPEC: $\frac{\mathcal{H} \vdash \exists_1 x_\imath.\, p\,x}{\mathcal{H} \vdash p\,(\textsf{the}\;p)}$

Left as an exercise for you

Sets

Not only can we derive the logic rules, but we can define sets, tuples, relations, numbers, and many more kinds of mathematical objects. Sets in type theory are just functions to booleans (The type $o$ in $Q_0$), so our notation for sets is recovered as sugar:

Term	What it sugars	Intuition
$x_\alpha \in A_{\alpha\to o}$	$A_{\alpha\to o}\,x$	$x$ has property $A$. Set membership is function application!
$\{ x_\alpha \mid A_o \}$	$\lambda x_\alpha. A_o$	A set is simply a boolean-valued characteristic function
$A_{\alpha\to o} \cup B_{\alpha\to o}$	$\forall x_\alpha. (x \in A \lor x \in B)$	Set union
$A_{\alpha\to o} \cap B_{\alpha\to o}$	$\forall x_\alpha. (x \in A \land x \in B)$	Set intersection
$A_{\alpha\to o} \subseteq B_{\alpha\to o}$	$\forall x_\alpha.\, (x \in A \supset x \in B)$	Subset
$\mathcal{P}\,A_{\alpha\to o}$	$\{ B_{\alpha\to o} \mid B \subseteq A \}$	Powerset (the set of all subsets) of $A$

We have sets, but numbers and arithmetic are still needed to have a Type Theory strong enough to formalize mathematics. Gaining these features requires an extension to $Q_0$, which Andrews calls $Q_0^\infty$. The extension adds a new type $\sigma$ for numbers, and adds axioms to define the natural numbers and arithmetic. The new type $\sigma$ is defined as the type of sets of sets of individuals, so that a number is represented as a set of sets of individuals. This is a very different approach from Church’s, which used a type of functions from booleans to booleans to represent numbers. We’ll visit Church’s approach when we look at the Lambda Calculus.

Andrews’ $Q_0^\infty$

It’s time to step things up a little. We haven’t actually claimed you can have as many individuals as you want. Infinity must be axiomatized. Once this is done, everything else about numbers is simply defined, with no new constants and no new axioms.

The natural numbers will be encoded like so:

• $0$ is the set containing the empty set of individuals
• $1$ is the set of all one-element sets of individuals
• $2$ is the set of all two-element sets of individuals
• $3$ is the set of all three-element sets of individuals
• and so on

Since the type “set of individuals” is $\imath \to o$, the type of natural numbers, that is, sets of sets of individuals is $(\imath \to o) \to o$.

Here’s the notation:

Type or Term	What it sugars	Intuition
$\sigma$	$(\imath\to o)\to o$	The type of numbers, represented as sets of sets of individuals
$0_\sigma$	$\lambda p_{\imath\to o}.\,\forall x_\imath.\,\neg\,p\,x$ or, equivalently, $Q_{\imath\to o\to\sigma}(\lambda x_\imath. F)$	The number zero: the collection whose only member is the empty set of individuals
$S_{\sigma\to\sigma}$	$\lambda n_\sigma \lambda p_{\imath\to o}.\,\exists x_\imath.\,p\,x \wedge n\,(\lambda y_\imath.\,p\,y \wedge y \neq x)$	The successor function: $p$ counts as $n+1$ when you can pull one element out of $p$ and what is left counts as $n$
$\mathbb{N}_{\sigma\to o}$	$\lambda n_\sigma.\,\forall q_{\sigma\to o}.\,(q\,0 \wedge \forall m_\sigma.\,(q\,m \supset q\,(S\,m))) \supset q\,n$	The set of natural numbers: what is in every collection containing $0$ and closed under $S$ — the intersection of all inductive sets

Note that mathematical induction is not an axiom but rather shows up in the definition of $\mathbb{N}$, so induction is free. If you’re familiar with the “Peano postulates” you’ll note in Type Theory they are theorems, not axioms. Addition and multiplication are defined by ordinary recursive functions like we saw above.

HOL

HOL is an interactive theorem prover. There is an underlying logic with a syntax, semantics, and inference rules. Unlike Church’s and Andrews’ systems above, HOL’s logic is given with axioms and Gentzen-style inference rules. The inference rules use sequents in which the assumptions are explicitly unordered sets, so no EXCHANGE and CONTRACT rules are needed to manage them, and discharge is handled via set subtraction. The focus here is not on formalizing all of mathematics per se, but in being able to prove everything.

The logic is organized into many theories, each a collection of axioms, definitions, and theorems. Proofs are written as functions in the meta language ML which return objects of type thm. The only possible values of type thm are those created via functions that implement the inference rules of the logic. This is Propositions as Types in real life.

HOL is more broadly a family of theorem provers, including HOL4, HOL Light, and Isabelle/HOL.

Martin-Löf Type Theory (MLTT)

The Swedish philosopher and logician Per Martin-Löf did such great work in developing intuitionistic type theory (as opposed to Church’s and Andrews’ which are classical), that the term is pretty much synonymous with his own branch of the field: Martin-Löf Type Theory (MLTT). There’s a lot of history behind the development of MLTT, including how original versions were found inconsistent due to Girard’s Paradox, how the theory (or theories) have evolved, and how the theory ended up powering many fields of computer science including formal verification, software security, and advanced programming languages.

The core idea of MLTT is propositions-as-types (with the dependent types we saw above), which fits perfectly with intuitionistic logic. As expected, the type theory generates a logic: every (constructive) demonstration of an inhabitant of a type is a proof of the corresponding proposition.

Good overviews of MLTT can be found at Wikipedia, nLab, the Stanford Encyclopedia of Philosophy, and lecture slides from Sergey Goncharov and Jacob Neumann. But here’s a quick summary of its highlights for the impatient:

• Type Judgments. You’ll see four primitive judgment forms: $\Gamma \vdash A\;\textsf{type}$, $\Gamma \vdash a : A$, and the definitional equalities $\Gamma \vdash A \equiv B$ and $\Gamma \vdash a \equiv b : A$.
• Rules. You’ll see formation rules (when is this a type?), introduction rules (how do you build an inhabitant?), elimination rules (how do you use one?), and computation rules (what does eliminating a constructed thing reduce to?).
• Quantifiers emerge from Dependent Types. The dependent function type $\Pi_{x:A}B(x)$ generalizes $A \to B$ and reads as $\forall$; the dependent pair type $\Sigma_{x:A}B(x)$ generalizes $A \times B$ and reads as $\exists$. An inhabitant of a $\Sigma$ is literally a witness paired with evidence, which is how existence proofs are truly constructive and not indirect.
• Data types are inductive, and their eliminators are induction. $\mathbb{N}$, lists, trees, and the general W-types are given by constructors. The eliminator for $\mathbb{N}$ is precisely the principle of mathematical induction. Recursion and induction are the same rule read two ways.
• Equality is a type. For $a, b : A$ there is an identity type $\textsf{Id}_A(a,b)$, introduced by $\textsf{refl}$ and eliminated by the rule $J$. There’s a distinction made between propositional equality and definitional equality ($\equiv$) which is a big deal.
• It is constructive on purpose. Negation is $A \to \mathbf{0}$ (yes that $\mathbf{0}$ is the empty type), and disjunction is the sum type $A + B$. There’s no rule that gives you $A + (A \to \mathbf{0})$. So no excluded middle! You can consistently assume excluded middle, but you lose canonicity: proofs stop being programs that compute. Perhaps they...loop forever?
• A hierarchy of universes. $\textsf{Type}_0 : \textsf{Type}_1 : \textsf{Type}_2 : \cdots$, exactly the cumulative hierarchy from our Universes section above, because $\textsf{Type} : \textsf{Type}$ is inconsistent by Girard’s Paradox.
• The theory is a programming language. Terms normalize, type checking is decidable, and a closed term of type $\mathbb{N}$ evaluates to an actual numeral. That is what makes Agda, Rocq, and Lean possible at all: checking a proof is running a type checker.

Quite a few proof assistants, provers, and programming languages are based on MLTT, including Agda, Rocq, Lean, Nuprl, Matita.

Many new research directions have grown out of Martin-Löf’s work. One of the newer directions is Homotopy Type Theory (HoTT), which you can read about at Wikipedia, nLab, and its very own HoTT website.

Type Theory in Practice

Type systems for real programming languages are actually applied type theories. We won’t go into depth here, but rather just drop a few items of interest.

• In languages with static type systems, type checking a program is proving (yes, that thing mathematicians do) it well-typed. That’s a big part of Curry-Howard, remember?
• Statically-typed languages with direct support for functional languages (e.g., Haskell, OCaml, Standard ML) are very much influenced by Church’s type theories. These languages are lauded for being secure, and often extremely efficient (see why Jane Street uses OCaml for high-frequency trading).
• The power of dependently typed languages (e.g., Idris) and proof systems with dependent types (e.g., Rocq, Agda, Lean, Nuprl, Matita) derive from research in type theory. These proof systems are incredibly important in modern computational research, as people work on proofs far too complex for any human to scribble on a few pages of paper. (Example: The proof that $BB(5)=47176870$ required 20,000 lines of Coq.)

By now you’re aware of how important Type Theory is in both Computer Science and Mathematics. It may even be the foundation of the intersection of the two fields:

The video is worth watching because you will see somewhere in it, how to pronounce Martin-Löf’s name correctly. 😀🎉🙌💪

Current Research

Two research threads are particularly active right now: people are (1) working on Homotopy Type Theory and (2) putting dependent types to work in some surprisingly different, very practical places. Very briefly, here are some things to note:

• Cubical Type Theory
• Quantitative Type Theory
• Community-built libraries of formalized mathematics (e.g., Lean’s Mathlib)
• Combining provers with LLMs, e.g., AlphaProof

Further Reading

Type Theory is too rich of a topic to cover in a single page. Browse the following resources to go more in-depth.

• History:
  • Wikipedia’s History of Type Theory
• Overview Articles and Portals:
  • Wikipedia: Type Theory
  • Stanford Encyclopedia of Philosophy: Type Theory
  • nLab: Type Theory
  • Daniel Gratzer, Learn Type Theory
• Required Reads:
  • Propositions as Types by Philip Wadler
  • The Rise of Type Theory
  • From Set Theory to Type Theory
  • Dependent Types at Work by Ana Bove and Peter Dybjer
• Other articles:
  • Set-like Mathematics in Type Theory
• Books:
  • Peter Andrews, An Introduction to Mathematical Logic and Type Theory
  • Type Theory Books on Goodreads
  • Robert Harper, Practical Foundations for Programming Languages
  • Rob Nederpelt and Herman Geuvers, Type Theory and Formal Proof
• Courses:
  • Robert Harper’s Types and Programming Languages course
  • Thorsten Altenkirch’s Naive Type Theory course
  • Herman Geuvers’ Introduction to Type Theory
• Videos (in addiiton to the ones embedded above):
  • Type Theory and the Algebra of Types by All Angles
  • The Curry-Howard Correspondence by Michael Ryan Clarkson (45:32)
  • Propositions as Types by Philip Wadler, presenting the paper you hopefully already read at Lambda Daλs 2016, with some additional content (56:57)
  • Another Propositions as Types video, this one from Computerphile (17:45)
• Information on specific type theories:
  • Simple Theory of Types (STT)
    • Simply typed Lambda Calculus at Wikipedia
    • nLab: Simply Typed Lambda Calculus
  • Martin-Löf Type Theory (MLTT)
    • nLab: Martin-Löf Type Theory
    • SEP article on ITT
    • Quick Intro to MLTT
    • Martin-Löf Type Theory Handout
  • System F
    • System F at Wikipedia
  • Homotopy Type Theory (HoTT)
    • nLab: Homotopy Type Theory
    • The HoTT Book

Recall Practice

Here are some questions useful for your spaced repetition learning. Many of the answers are not found on this page. Some will have popped up in lecture. Others will require you to do your own research.

1. Type Theory is one of three kinds of theories that can be said to have a claim as a theoretical foundation for all of mathematics. What are the other two?
   Set Theory and Category Theory
2. What is the central idea of Type Theory?
   Types classify terms, and the theory provides rules for constructing and reasoning about these types and terms.
3. What does a typing judgment look like?
   $x\!: t$
4. Why do some people find Type Theory more appealing as a foundation for mathematics and computation than Set Theory?
   Because Type Theory integrates logic and computation directly into the foundation, giving it a computational flavor ideal in describing and reasoning about programming languages.
5. What does the definition of the type $\textsf{Bool}$ look like?
   $$\dfrac{}{\textsf{true}\!: \textsf{Bool}} \quad\quad\quad \dfrac{}{\textsf{false}\!: \textsf{Bool}}$$
6. What are the inhabitants of the type $\textsf{Bool}$?
   $\textsf{true}$ and $\textsf{false}$.
7. What are the two constructors of the type $\textsf{Nat}$?
   0 and $\textsf{s}$.
8. How is the type of integers defined?
   $$\dfrac{n\!: \textsf{Nat}}{\textsf{pos}\,n\!: \textsf{Int}} \quad\quad\quad \dfrac{n\!: \textsf{Nat}}{\textsf{neg}\,(\textsf{s}\,n)\!: \textsf{Int}}$$
9. How is the type of rational numbers defined?
   $$\dfrac{n\!: \textsf{Int} \quad d\!: \textsf{Nat}}{\textsf{rat}\,n\,(\textsf{s}\,d)\!: \textsf{Rat}}$$
10. What kind of a type do tuples belong to?
    A product type.
11. What are the constructors of the list type?
    The empty list [] and the prefix operator ::.
12. What does the notation [2, 3, 5] abbreviate?
    2::3::5::[]
13. What is the sole inhabitant of the type Unit?
    ().
14. What is the difference between the types Void and Unit?
    Void has no inhabitants, Unit has one.
15. What are the inhabitants of $\mathsf{Bool \times Unit}$? Of $\mathsf{Bool + Unit}$?
    The product type has $2 \times 1 = 2$ inhabitants: $(\mathsf{true, ()})$ and $(\mathsf{false, ()})$. The sum has three inhabitants: $\mathsf{inl\,true}, \mathsf{inl\,false}$, and $\mathsf{inr\,()}$.
16. What does it mean for $t_1$ to be a subtype of $t_2$?
    Every inhabitant of type $t_1$ is also an inhabitant of type $t_2$.
17. How do we write that $t_1$ is a subtype of $t_2$?
    $t_1\:\texttt{<:}\:t_2$
18. How do we write the type that is the union of $t_1$ and $t_2$?
    $t_1 \mid t_2$
19. How do we write the type that is the intersection of $t_1$ and $t_2$?
    $t_1\:\texttt{&}\:t_2$
20. What is the difference between a union type and a sum type?
    A union type is simply made up of all of the elements of its constituent types. A sum type’s elements are tagged.
21. What is another way to write the type $A \rightarrow B$?
    $B^A$
22. What is a set in Type Theory?
    A function with codomain $\mathsf{Bool}$. The members of the set are all values $x$ for which $f\,x = \mathsf{true}$, where the set is identified with the function $f$.
23. How do we represent the set $\{ (x, y) \mid x \in \mathbb{N} \land y \in \mathbb{N} \land x > y \}$ as a function in Type Theory?
    $\lambda (x, y)_{\small \mathsf{nat \times nat}}. x > y$
24. What are abstraction, congruence, and extensionality in Type Theory?
    Abstraction creates the functions, congruence ensures we can safely substitute equals for equals, and extensionality dictates when two distinct functions should be considered identical
25. If a function $f$ has domain $t_1$ and codomain $t_2$, what type does $f$ inhabit?
    $t_1 \to t_2$
26. In $\lambda x_\alpha.\,e_\beta$, which part (the parameter’s type or the body’s type) is more often dropped when inferrable?
    The body’s type ($\beta$) is often dropped; the parameter’s type ($\alpha$) rarely is.
27. How does the arrow associate in a function type like $t_1 \to t_2 \to t_3$?
    Right-associatively: $t_1 \to (t_2 \to t_3)$.
28. How does function application associate, e.g. in $f\,x\,y$?
    Left-associatively: $(f\,x)\,y$.
29. What notation does a case expression on a Boolean $b$ use to define, e.g., negation?
    $[\,b \ \Vert \ \textsf{true} \to \textsf{false} \mid \textsf{false} \to \textsf{true}\,]$
30. Why is “definition by cases” (splitting clauses onto separate lines) usually preferred over one big case expression?
    It is more readable, especially once the type signature is moved to its own line.
31. What does moving a function’s parameters to the left of $=$ and out of a tuple let you do to definitions like $\textsf{and}$?
    Write its type using $\to$ instead of $\times$, and eventually drop the $\lambda$s entirely by writing multiple parameters directly in each clause.
32. How is $\textsf{plus}$ defined recursively on $\textsf{Nat}$?
    $\textsf{plus}\;m\;0 = m$; $\;\textsf{plus}\;m\;(\textsf{s}\,n) = \textsf{s}\;(\textsf{plus}\;m\;n)$
33. Why is the recursion in $\textsf{plus}$ guaranteed to terminate?
    The recursive call is made on $n$, which is structurally smaller than the clause’s argument $\textsf{s}\,n$.
34. How is $\textsf{times}$ defined in terms of $\textsf{plus}$?
    $\textsf{times}\;m\;0=0$; $\;\textsf{times}\;m\;(\textsf{s}\,n)=\textsf{plus}\;m\;(\textsf{times}\;m\;n)$
35. What is the monus operation, and how does it differ from ordinary subtraction?
    It’s subtraction on naturals capped at zero rather than going negative, e.g. $3-5=0$.
36. How can $\textsf{le}$ be defined concisely using $\textsf{minus}$ (monus)?
    $\textsf{le}\;m\;n = \textsf{isZero}\;(\textsf{minus}\;m\;n)$
37. What does the underscore in $\textsf{le}\;0\;\_ = \textsf{true}$ mean?
    A wildcard parameter — it matches anything without binding a name.
38. What sugar stands for $\textsf{cond}\;b\;x\;y$?
    $\textsf{if}\;b\;\textsf{then}\;x\;\textsf{else}\;y$
39. What sugar stands for $(\lambda x.\,e')\,e$?
    $\textsf{let}\;x = e\;\textsf{in}\;e'$ (equivalently, $e'\;\textsf{where}\;x = e$)
40. Why does $\textsf{head}$ have type $t^* \to t\texttt{?}$ instead of $t^* \to t$?
    Because the empty list has no head, so the result type must allow for no answer.
41. How is $\textsf{map}$ defined on lists?
    $\textsf{map}\;f\;[\,] = [\,]$; $\;\textsf{map}\;f\;(x\,\textbf{::}\,y) = (f\;x)\,\textbf{::}\,(\textsf{map}\;f\;y)$
42. In the definition of $\textsf{indexOf}$, why is $\textsf{map}\,(\lambda n.\,n+1)$ applied to the recursive call?
    To bump the found index by one as the recursion returns back up through each skipped element.
43. What three strategies does Type Theory offer for turning a partial function into a total one?
    (1) Use an option type for the codomain, (2) use a custom type with an error variant for the codomain, or (3) restrict the domain.
44. Why are explicit type annotations often needed on a standalone function definition, even though they’re often skippable inside a definition by cases?
    Operators like $+, \times, \bmod$ are overloaded across many types, so context alone may not determine which is meant.
45. What is the inferred type of $\lambda f.\,\lambda x.\,f(f(x))$?
    $\forall \alpha.\,(\alpha \to \alpha) \to \alpha \to \alpha$
46. What does the $\forall$ in a polymorphic type like $\forall \alpha. (\alpha\to\alpha)\to\alpha\to\alpha$ mean, informally?
    You may substitute any type you like for $\alpha$.
47. How does $(a_1, \ldots, a_n)$ desugar?
    $(a_1, (a_2, (\ldots, (a_{n-1}, a_n)\ldots)))$
48. What abbreviation is used for the type $\textsf{Unicode}^*$?
    $\textsf{String}$
49. What are the two constructors of the option type $t\texttt{?}$?
    $\textsf{none}$ and $\textsf{some}\,x$ (for $x\!:\!t$)
50. Why does $\textsf{Void}$ need no construction rules at all?
    It has no inhabitants, so there is nothing for a rule to construct.
51. Which mainstream programming language conflates $\textsf{Void}$ and $\textsf{Unit}$, and how?
    Swift — its type called Void is actually inhabited by a single value $()$, i.e. it’s really Unit.
52. What does it mean for $x$ to be a member of a set $A$, where $A\!:\!t\to\textsf{Bool}$?
    $A\,x = \textsf{true}$
53. Why is equality not free when doing foundations?
    We never defined a function to compute it, nor stated what it even means — it has to be built into or derived within the system.
54. When are two functions $f_{\alpha\to\beta}$ and $g_{\alpha\to\beta}$ considered equal in most type theories?
    When $f\,x = g\,x$ for all $x\!:\!\alpha$ (extensional equality).
55. How can real numbers be represented in Type Theory, echoing the approach from Set Theory?
    As a Dedekind cut — a function of type $\textsf{Rat}\to\textsf{Bool}$ — bundled with proofs that the cut is non-empty, bounded, downward closed, and has no greatest element.
56. Which two rules in the naive $\textsf{Value}$ type definition are illegal, and why?
    The $\textsf{set}$ and $\textsf{fun}$ rules, since $\textsf{Value}\to\textsf{Bool}$ and $\textsf{Value}\to\textsf{Value}$ put $\textsf{Value}$ on the left of a function arrow, which by Cantor’s Theorem creates a cardinality paradox.
57. What is strict positivity?
    The condition that the type being defined never appears on the left-hand side (domain) of a function arrow in any premise of its own constructors.
58. Why don’t pairs and lists run into the same cardinality trouble that sets and functions do?
    $|T\times T|$ and $|T^*|$ don’t outgrow $|T|$ the way $|\mathcal{P}(T)| = 2^{|T|}$ does — you’re multiplying/copying $T$, not putting $T$ in the exponent.
59. What breakthrough did Dana Scott offer so that sets and functions could still exist as values in a programming language?
    Restrict $A\to B$ to mean only the continuous functions over partial orders — a much smaller space than all mathematical functions, avoiding Cantor’s barrier.
60. What two properties must a set of inductive rules satisfy to legally define a type?
    Well-foundedness (every inhabitant buildable in finitely many rule applications) and strict positivity.
61. Which type constructor can be used to build other inductively-defined types but cannot itself be defined inductively?
    The function type $t_1 \to t_2$.
62. What are the alternate notations for $\textsf{Void}$ and $\textsf{Unit}$ given in the Summary of Basic Types?
    $\textsf{Void}$: $\bot$ or $\mathbf{0}$.   $\textsf{Unit}$: $()$ or $\mathbf{1}$.
63. Why doesn’t a plain union $C \mid D$ give the right count of inhabitants for a sum of $C$ (3 elements) and $D$ (2 elements)?
    Shared symbols (like $r$ appearing in both types) get merged rather than kept distinct, so the union has fewer than $3+2=5$ elements.
64. What do $\textsf{inl}$ and $\textsf{inr}$ stand for?
    inject left and inject right
65. What type has zero elements and corresponds to a sum over zero types? What type has one element and corresponds to a product over zero types?
    $\textsf{Void}$ (empty sum); $\textsf{Unit}$ (empty product)
66. Why is $C \to D$ written $D^C$?
    Because the number of functions from $C$ to $D$ is $|D|^{|C|}$ — exactly the exponential.
67. What everyday problem with $\textsf{head}$ and $\textsf{tail}$ motivates dependent types?
    With plain lists $t^*$, nothing in the type guarantees non-emptiness, so $\textsf{head}$/$\textsf{tail}$ need an option type (or risk crashing).
68. How is $\mathsf{Vec}\;t\;n$, the type of length-$n$ vectors, defined?
    $\textsf{nil}\!:\!\mathsf{Vec}\;t\;0$; $\;(x::y)\!:\!\mathsf{Vec}\;t\;(n+1)$ given $x\!:\!t$ and $y\!:\!\mathsf{Vec}\;t\;n$
69. Why is $\mathsf{Vec}\;t$ (without the length) called a “family of types” rather than a type?
    It’s a mapping from $\textsf{Nat}$ to types — for each different $n$, $\mathsf{Vec}\;t\;n$ is a genuinely different type.
70. What compile-time guarantee does the type $\mathsf{Vec}\;t\;(n+1) \to t$ give $\textsf{head}$ that $t^* \to t\texttt{?}$ cannot?
    Non-emptiness is checked statically — you cannot even write down a $\mathsf{Vec}$ with the wrong number of elements, so no runtime check or option type is needed.
71. What is $\textsf{Fin}\;n$?
    The type of natural numbers strictly less than $n$ (e.g. $\textsf{Fin}\;3 = \{0,1,2\}$)
72. What does $\Pi_{x:A} B$ mean, and how does it relate to $\to$?
    The type of functions that, given $a\!:\!A$, return a term of type $B[x\mapsto a]$; when $B$ doesn’t depend on $x$, it’s just $A\to B$ — $\Pi$ generalizes $\to$.
73. What does $\Sigma_{x:A} B(x)$ mean, and how does it relate to $\times$?
    The type of pairs $(a,b)$ where $a\!:\!A$ and $b\!:\!B(a)$; when $B$ doesn’t depend on $x$, it’s just $A\times B$ — $\Sigma$ generalizes $\times$.
74. What is a refinement type? Answer with the example of the type of positive naturals.
    A subtype formed by restricting a supertype with a value-based condition; $\Sigma_{n:\textsf{Nat}}(n>0)$ — a number paired with a proof that it’s positive.
75. Informally, $\Pi$ gives $\forall$ vibes. What does $\Sigma$ give?
    $\exists$ vibes
76. Who is credited with discovering the correspondence between formulas and types, and what is it called?
    Haskell Curry and William Alvin Howard; the Curry-Howard Correspondence (or Isomorphism)
77. In the Curry-Howard table, what type corresponds to conjunction? To disjunction? To implication?
    Product type $A\times B$; sum type $A+B$; function type $A\to B$
78. What type corresponds to universal quantification $\forall x.((x\in A)\supset B)$? To existential quantification?
    The dependent function type $\Pi_{x:A}B$; the dependent pair type $\Sigma_{x:A}B$
79. Under Propositions as Types, what does it mean to “prove a formula”?
    To construct an inhabitant of the corresponding type.
80. What three slogans do the notes give for the depth of the Curry-Howard correspondence?
    Propositions are Types
    Proofs are Programs
    Computation is Proof Normalization
81. How is equality given a single constructor as a type, and what is that constructor called?
    $\dfrac{x\!: t}{\textsf{refl}\,x\!: (x = x)}$ — reflexivity: a proof that $x$ equals itself.
82. Why can’t $\textsf{Type}$ itself be given the rule $\dfrac{}{\textsf{Type}\!:\!\textsf{Type}}$?
    It’s inconsistent — Girard showed (1972) that from $\textsf{Type}\!:\!\textsf{Type}$ you can construct an inhabitant of $\textsf{Void}$, i.e. prove $F$. This is Girard’s Paradox.
83. How does stratification into universes avoid Girard’s Paradox?
    By building an infinite tower $\textsf{Type}_i\!:\!\textsf{Type}_{i+1}$, so no universe is ever a member of itself.
84. What does cumulativity say, and what rule expresses it?
    Every universe’s inhabitants are also inhabitants of every universe above it; $\dfrac{t\!:\!\textsf{Type}_i}{t\!:\!\textsf{Type}_{i+1}}$
85. What is typical ambiguity?
    Writing unsubscripted $\textsf{Type}$ to mean “some $\textsf{Type}_i$, for whichever $i$ makes this typecheck,” rather than writing out the level every time.
86. What is the difference between a universe and the cumulative hierarchy?
    A universe is one level ($\textsf{Type}_i$ for a specific $i$); the cumulative hierarchy is the whole tower $\textsf{Type}_0, \textsf{Type}_1, \ldots$
87. What does universe polymorphism let a definition like $\mathsf{Vec}$ do?
    Be parameterized by an explicit level variable $i$, with the typechecker solving for consistent levels at each use site.
88. What problem was Russell’s ramified Theory of Types (1908) trying to solve, and what clunky axiom did he need to recover ordinary mathematics?
    Russell’s Paradox, by making definitions predicative; he needed the axiom of reducibility.
89. What did the Simple Theory of Types (Ramsey, later Tarski) drop from Russell’s system?
    The orders/ramification, keeping only the type hierarchy — eliminating the need for the axiom of reducibility.
90. What did Church combine to create his Simple Theory of Types (1940)?
    Untyped lambda calculus with a simple type discipline.
91. Who independently discovered System F, and in what two contexts?
    Jean-Yves Girard (1972, proof theory) and John Reynolds (1974, programming languages) — giving parametric polymorphism / generics.
92. What does Martin-Löf Type Theory take as primitive, and what is it meant to be a foundation for?
    Dependent types ($\Pi$ and $\Sigma$); a full foundation for constructive mathematics.
93. How does Andrews’ $Q_0$ differ philosophically from MLTT and the Calculus of Constructions?
    $Q_0$ is classical (not constructive) and non-dependent, built from a minimal basis where everything reduces to equality.
94. What does the Calculus of Constructions combine?
    Martin-Löf-style dependent types with System F-style polymorphism.
95. What key idea does Homotopy Type Theory bring to Martin-Löf’s identity types?
    Reinterpreting them through Homotopy Theory: types as spaces, terms as points, equalities as paths.
96. What are the three forms a $Q_0$ type can take?
    $\imath$, $o$, or $(\alpha\to\beta)$
97. What do the base types $\imath$ and $o$ represent in $Q_0$?
    $\imath$ is the type of individuals; $o$ is the type of truth values.
98. What are the only two constants in $Q_0$?
    $\textsf{Q}_{\alpha\to\alpha\to o}$ (equality) and $\textsf{the}_{(\alpha\to o)\to \alpha}$ (description), for every type $\alpha$
99. What does $A_\alpha = B_\alpha$ sugar, showing that equality is primitive in $Q_0$?
    $\textsf{Q}_{\alpha\to\alpha\to o}\,A_\alpha\,B_\alpha$
100. How is $T_o$ (truth) defined in $Q_0$?
     $\textsf{Q}_{o\to o\to o} = \textsf{Q}_{o\to o\to o}$ — $\textsf{Q}$ equals itself, trivially true
101. How is $F_o$ (falsity) defined in $Q_0$?
     $(\lambda x_o.\,T_o) = (\lambda x_o.\,x_o)$ — these two functions genuinely disagree, so the equation is false
102. How is $\forall x_\alpha.\,A_o$ encoded as an equation between two functions?
     $(\lambda x_\alpha.\,T_o) = (\lambda x_\alpha.\,A_o)$ — for the constantly-true function to equal the $A$-function, $A$ must be true everywhere
103. How is $A_o \lor B_o$ defined in terms of $\land$ and $\neg$?
     $\neg(\neg A \land \neg B)$ — De Morgan
104. How is $\exists x_\alpha.\,A_o$ defined in terms of $\forall$?
     $\neg(\forall x_\alpha.\,\neg A)$
105. What does $\iota x_\alpha.\,A_o$ (definite description) sugar?
     $\textsf{the}_{(\alpha\to o)\to \alpha}\,(\lambda x_\alpha.\,A)$
106. What does Axiom 1 of $Q_0$ assert about booleans?
     There are exactly two truth values — if a predicate on booleans holds at both $T$ and $F$, it holds at every boolean.
107. What does Axiom Schema 2 assert, and why is it a schema?
     Equal things have the same properties (Leibniz-style substitution); it’s a schema because there’s one instance per type $\alpha$.
108. What does Axiom Schema 3 (extensionality) say about functions?
     Two functions are equal exactly when they agree on every input — there is no other way for functions to differ.
109. What does Axiom Schema 4 (Beta Conversion) say?
     Applying a function to an argument literally is capture-avoiding substitution of the argument for the parameter in the body.
110. What does Axiom 5 (Description) say?
     $\textsf{the}\,(\lambda x_\imath.\,x_\imath=y_\imath) = y_\imath$, i.e., “the individual equal to $y$” is $y$
111. What is Andrews’ single rule of inference (Rule R), and what proviso does it carry?
     From $C$ and $A_\alpha=B_\alpha$, infer the result of replacing one occurrence of $A_\alpha$ in $C$ with $B_\alpha$ — provided that occurrence isn’t a variable immediately preceded by $\lambda$.
112. What is the overall shape of Andrews’ foundation, contrasted with Set Theory’s?
     Set Theory assumes first-order logic already in place, then gives axioms defining sets. $Q_0$ defines what a function is and gets all logical operators as sugar over equality — functions first, then logic.
113. What four liberties did the notes take converting Andrews’ Hilbert-style presentation to Gentzen style?
     (1) added structural rules for hypothesis management, (2) split Axiom 3 into directional ABS and EXT, (3) replaced Axiom 1 with CASES, (4) merged Rule R and derived rule RR into one R rule
114. What does the BETA rule say?
     Applying a function to an argument yields the body with the argument substituted for the parameter.
115. What does the ABS rule require about the bound variable $x$?
     That $x$ is not free in $\mathcal{H}$
116. What does the EXT rule require about the variable $x$ used to test pointwise equality?
     That $x$ is not free in $A$, $B$, or $\mathcal{H}$
117. What does the CASES rule let you conclude, and from what two premises?
     $B$ unconditionally, from a proof of $B$ assuming $A=T$ and a proof of $B$ assuming $A=F$
118. What does the DESC rule assert?
     If there’s exactly one $x$ satisfying $p$, then $p$ holds of $\textsf{the}\;p$
119. What two provisos govern replacing an occurrence of $A_\alpha$ with $B_\alpha$ using rule R inside a context $\mathcal{C}$?
     No free variable of $A$ may fall inside the scope of a binder at that occurrence, and no free variable of $B$ may be captured by a binder there.
120. What does $x_\alpha \in A_{\alpha\to o}$ sugar?
     $A_{\alpha\to o}\,x$ — set membership is just function application
121. What does $\{ x_\alpha \mid A_o \}$ sugar?
     $\lambda x_\alpha.\,A_o$
122. What does $\mathcal{P}\,A_{\alpha\to o}$ (powerset) sugar?
     $\{ B_{\alpha\to o} \mid B \subseteq A \}$ — the set of all subsets of $A$
123. What does Axiom 6 (Infinity) assert exists?
     A relation $r$ on individuals that is irreflexive and transitive, where every individual has an $r$-successor — guaranteeing $\imath$ is infinite
124. What is the type $\sigma$ of numbers in $Q_0^\infty$, and what does it represent set-theoretically?
     $(\imath\to o)\to o$ — a number is a set of sets of individuals
125. How does the successor function $S$ work, intuitively?
     $p$ counts as $n+1$ when you can pull one element out of $p$ and what’s left counts as $n$
126. In $Q_0^\infty$, is mathematical induction an axiom?
     No, it falls out of the definition of $\mathbb{N}$ as that which is in every collection containing $0$ and closed under $S$. The Peano postulates end up as theorems rather than axioms.
127. How does Andrews’ encoding of numbers as sets of sets differ from Church’s approach?
     Andrews represents a number as a set of sets of individuals; Church instead used a type of functions from booleans to booleans (Church numerals).
128. How does HOL’s presentation of assumptions differ from $Q_0$’s Gentzen rules, and what does that eliminate the need for?
     HOL’s sequents use explicitly unordered assumption sets, so no EXCHANGE or CONTRACT rules are needed.
129. In HOL, what does a proof actually look like, mechanically?
     A function in the meta-language ML that returns an object of type thm, where the only way to construct a thm is via functions implementing the logic’s inference rules.
130. What are the four primitive judgment forms in MLTT?
     $\Gamma \vdash A\;\textsf{type}$, $\Gamma \vdash a : A$, $\Gamma \vdash A \equiv B$, and $\Gamma \vdash a \equiv b : A$
131. What four kinds of rules appear for each type former in MLTT?
     Formation, introduction, elimination, and computation rules
132. The identity type $\textsf{Id}_A(a,b)$ is introduced by what, and eliminated by what?
     Introduced by $\textsf{refl}$; eliminated by the rule $J$
133. What happens to canonicity if you assume excluded middle in MLTT?
     You lose it — proofs stop being programs guaranteed to compute (normalize).
134. What makes MLTT a programming language in a strong sense?
     Terms normalize, type checking is decidable, and a closed term of type $\mathbb{N}$ evaluates to an actual numeral — checking a proof is running a type checker.
135. What is negation defined as in MLTT (constructively)?
     $A \to \mathbf{0}$, i.e. a function from $A$ to the empty type
136. What real-world achievement is cited as an example of a proof too complex for a human to scribble on paper?
     The proof that $BB(5) = 47176870$, which required 20,000 lines of Coq
137. What two research threads does the notes call out as particularly active right now?
     Homotopy Type Theory, and putting dependent types to work in practical places

Summary