Type Theory

Whether or not you are the type of person that is interested in types, you might find fun to explore various theories about them. Type Theory, not Set Theory, is generally the best way to organize knowledge and computations in Computer Science. It’s actually kind of cool, too. Really.

What is Type Theory?

TODO

Some Type Theories

There are many different type theories out there! The first was probably Russell’s from the very early 20th century, but the newer ones are the ones most associated with the term “Type Theory.” The influential and important type theories are these:

Some Basic Types

Here are the types of a basic (constructive) type theory (most type theories use these):

$\bot$ is a type, the empty type, the type of no inhabitants.
$()$ is a type, the unit type, the type of exactly one inhabitant.
You can inductively define types like $\textsf{Bool}$, $\textsf{Nat}$, $\textsf{Int}$, $\textsf{Char}$, $\textsf{String}$, etc.
If $A$ and $B$ are types, then $A \times B$ is a type. It is the type of pairs $(a, b)$ where $a\!:\!A$ and $b\!:\!B$.
If $A$ and $B$ are types, then $A + B$ is a type, called a discriminated union. It is the type containing terms of $A$ and terms of $B$ but they are tagged so you know whether they came from $A$ or $B$. One way to tag them is $(\textsf{true}, A)$ and $(\textsf{false}, B)$ for $a\!:\!A$ and $b\!:\!B$.
If $A$ and $B$ are types, then $A \rightarrow B$ is a type. It is the type of functions that take an argument of type $A$ and return a value of type $B$.
If $A$ is a type and $B$ is a type depending on $x\!:A$, then $\Pi_{x:A} B$ is a type.
- Example: $\mathsf{tuple}\;B\;n \equiv \Pi_{n:\textsf{Nat}} B^n$ is the type of tuples containing inhabitants of type $B$ of length $n$.
If $A$ is a type and $B$ is a type depending on $x\!:A$, then $\Sigma_{x:A} B$ is a type.
- Example: $\mathsf{list}\;B \equiv \Sigma_{n:\textsf{Nat}} B^n$ is the type of lists of any size containing inhabitants of type $B$.

Dependent Types

Propositions as Types

Oh, what does it mean that type theory has logic built-in? There’s this thing called ”Propositions as Types” (a.k.a. the Curry-Howard correspondence) that says that types are propositions and functions are proofs. Rather than dwell on it too deeply for now, here’s a table to get you the idea:

Logical Formula	Meaning	Type
$F$	Falsity	$\bot$
$T$	Truth	$()$
$A \wedge B$	Conjunction (And)	$A \times B$
$A \vee B$	Disjunction (Or)	$A + B$
$A \rightarrow B$	Implication	$A \rightarrow B$
$\forall x. ((x \in A) \supset B)$ where $x$ is free in $B$	Universal Quantification	$\Pi_{x: A} B$
$\exists x. ((x \in A) \wedge B)$ where $x$ is free in $B$	Existential Quantification	$\Sigma_{x: A} B$

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.

Type Theory is one of three kind 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

Summary

We’ve covered:

What Type Theory Is
History
Some of the popular type theories
Basic types
Dependent types
Connections to logic