Type Theory

Why This Matters

Type theory provides a single framework where programs and proofs are the same objects. A type is a specification; a term inhabiting that type is a program meeting that specification (or equivalently, a proof of the corresponding proposition). This is the Curry-Howard correspondence, and it is the foundation of modern proof assistants (Lean, Coq, Agda) and the theoretical basis for type systems in programming languages.

For ML researchers, type theory matters in two ways. First, formal verification of ML systems (proving correctness of gradient computations, verifying properties of neural network architectures) requires a logic powerful enough to express quantitative statements, and dependent type theory provides this. Second, the structure of type systems (polymorphism, higher-order types, linear types) directly influences the design of probabilistic programming languages used for Bayesian inference.

Simply Typed Lambda Calculus

Definition

Simple Types

The simple types over a set of base types $\{\alpha, \beta, \ldots\}$ are generated by the grammar:

$\tau ::= \alpha \mid \tau_1 \to \tau_2$

Here $\alpha$ is a base type (e.g., $\text{Nat}$, $\text{Bool}$) and $\tau_1 \to \tau_2$ is the function type: the type of functions taking input of type $\tau_1$ and returning output of type $\tau_2$. The arrow associates to the right: $\alpha \to \beta \to \gamma$ means $\alpha \to (\beta \to \gamma)$.

Definition

Simply Typed Lambda Calculus

The simply typed lambda calculus ($\lambda^{\to}$) extends the untyped lambda calculus with type annotations. Terms are:

$M ::= x \mid \lambda x:\tau.\, M \mid M\, N$

A typing judgment $\Gamma \vdash M : \tau$ states that term $M$ has type $\tau$ under context $\Gamma$ (a mapping from variables to types). The typing rules are:

1. Variable: If $x : \tau \in \Gamma$, then $\Gamma \vdash x : \tau$
2. Abstraction: If $\Gamma, x:\tau_1 \vdash M : \tau_2$, then $\Gamma \vdash (\lambda x:\tau_1.\, M) : \tau_1 \to \tau_2$
3. Application: If $\Gamma \vdash M : \tau_1 \to \tau_2$ and $\Gamma \vdash N : \tau_1$, then $\Gamma \vdash M\, N : \tau_2$

Definition

Type Safety (Progress and Preservation)

A type system is safe if it satisfies two properties:

• Progress: If $\vdash M : \tau$ (closed, well-typed term), then either $M$ is a value or $M$ steps to some $M'$.
• Preservation (Subject Reduction): If $\vdash M : \tau$ and $M \to M'$, then $\vdash M' : \tau$.

Together, these guarantee that well-typed programs do not get "stuck" (reach a state that is neither a value nor reducible).

The Curry-Howard Correspondence

Theorem

Curry-Howard Correspondence

Statement

There is an exact correspondence between the simply typed lambda calculus and intuitionistic propositional logic:

Type Theory	Logic
Type $\tau$	Proposition $P$
Term $M : \tau$	Proof of $P$
Function type $\tau_1 \to \tau_2$	Implication $P_1 \Rightarrow P_2$
Lambda abstraction $\lambda x:\tau_1.\, M$	Implication introduction (assume $P_1$, derive $P_2$)
Function application $M\, N$	Modus ponens ($P_1 \Rightarrow P_2$ and $P_1$ yield $P_2$)
Inhabited type	Provable proposition
Type checking	Proof verification
Type inference	Proof search

A proposition $P$ is provable in intuitionistic logic if and only if the corresponding type is inhabited (has a closed term of that type) in $\lambda^{\to}$.

Intuition

Building a term of type $A \to B$ means writing a function that takes an $A$ and returns a $B$. In logic, this is the same as assuming $A$ and deriving $B$, which is exactly an implication proof. The correspondence is not a metaphor; it is a formal isomorphism between two independently developed systems.

Proof Sketch

By structural induction on typing derivations and proof trees. Each typing rule corresponds to a proof rule:

• The variable rule corresponds to using an assumption from the context.
• The abstraction rule $\frac{\Gamma, x:A \vdash M : B}{\Gamma \vdash \lambda x:A.\, M : A \to B}$ corresponds exactly to implication introduction $\frac{\Gamma, A \vdash B}{\Gamma \vdash A \Rightarrow B}$.
• The application rule $\frac{\Gamma \vdash M : A \to B \quad \Gamma \vdash N : A}{\Gamma \vdash M\, N : B}$ corresponds to modus ponens.

This bijection extends to normalization: beta-reduction of terms corresponds to cut-elimination in the proof system.

Why It Matters

The Curry-Howard correspondence means that type checkers are proof checkers. When Lean verifies that a term has a given type, it is verifying a mathematical proof. This unification is the reason proof assistants work: you write proofs as programs, and the type checker verifies them automatically. It also means that any advance in type theory yields an advance in logic, and vice versa. The correspondence extends further through category theory, where types correspond to objects, functions to morphisms, and the entire structure forms a cartesian closed category.

Failure Mode

The simple Curry-Howard correspondence covers only intuitionistic propositional logic (implications). To handle quantifiers ("for all", "there exists"), you need dependent types. To handle classical logic (law of excluded middle), you need control operators (continuations). The basic correspondence does not cover these extensions without additional machinery.

System F: Polymorphism

Definition

System F (Polymorphic Lambda Calculus)

System F extends $\lambda^{\to}$ with type variables and universal quantification over types:

$\tau ::= \alpha \mid \tau_1 \to \tau_2 \mid \forall \alpha.\, \tau$

Terms gain type abstraction and type application:

$M ::= x \mid \lambda x:\tau.\, M \mid M\, N \mid \Lambda \alpha.\, M \mid M\, [\tau]$

The polymorphic identity function has type $\forall \alpha.\, \alpha \to \alpha$ and is written $\Lambda \alpha.\, \lambda x:\alpha.\, x$. Applying it to a specific type, say $[\text{Nat}]$, yields $\lambda x:\text{Nat}.\, x$.

Under Curry-Howard, $\forall \alpha.\, \tau$ corresponds to second-order universal quantification over propositions.

System F is strictly more expressive than $\lambda^{\to}$. It can encode natural numbers, booleans, pairs, and lists purely through polymorphism, without built-in data types. The Church numeral $n$ has type $\forall \alpha.\, (\alpha \to \alpha) \to \alpha \to \alpha$, representing "apply a function $n$ times."

A critical property: type inference in System F is undecidable (Wells, 1999). Languages like Haskell and ML use restricted variants (Hindley-Milner, System F with rank-1 polymorphism) where type inference is decidable and runs in near-linear time.

Type Checking vs. Type Inference

Definition

Type Checking vs. Type Inference

Type checking is the problem: given $\Gamma$, $M$, and $\tau$, decide whether $\Gamma \vdash M : \tau$.

Type inference is the problem: given $\Gamma$ and $M$ (with some type annotations possibly omitted), find a type $\tau$ such that $\Gamma \vdash M : \tau$, or report that none exists.

Type inference is strictly harder than type checking. For $\lambda^{\to}$, both are decidable. For System F, type checking is decidable but type inference is undecidable. For dependently typed systems, type checking is decidable (given enough annotations) but type inference is generally undecidable.

Toward Dependent Types

In $\lambda^{\to}$ and System F, types cannot mention values. You can write the type "list of natural numbers" but not "list of natural numbers of length 5." Dependent type theory lifts this restriction:

• Pi types $\prod_{x:A} B(x)$: the type of functions where the output type depends on the input value. This generalizes $A \to B$ (where $B$ does not depend on $x$).
• Sigma types $\sum_{x:A} B(x)$: the type of pairs $(a, b)$ where $a : A$ and $b : B(a)$. This generalizes $A \times B$.

Under Curry-Howard, $\prod_{x:A} B(x)$ corresponds to $\forall x.\, B(x)$ and $\sum_{x:A} B(x)$ corresponds to $\exists x.\, B(x)$.

Practical Systems

System	Types	Logic	Examples
$\lambda^{\to}$	Simple types	Propositional logic	Theoretical foundation
Hindley-Milner	Rank-1 polymorphism	Restricted second-order	Haskell, OCaml, ML
System F	Full polymorphism	Second-order logic	Theoretical, GHC Core
System $F_\omega$	Higher-kinded types	Higher-order logic	Haskell (partially)
CIC	Full dependent types	Higher-order predicate logic	Coq
MLTT	Full dependent types	Constructive type theory	Agda, Lean

Common Confusions

Watch Out

Types in programming vs. types in type theory

In most programming languages, types are a safety mechanism: they prevent adding a string to an integer. In type theory, types are propositions and carry logical content. The type $\text{Vec}(\mathbb{R}, n)$ does not just prevent misuse; it states that the vector has exactly $n$ components, and a term of that type is evidence of this fact. Programming language types are a degenerate case of the full type-theoretic picture.

Watch Out

Intuitionistic vs. classical logic

The Curry-Howard correspondence gives intuitionistic logic, not classical logic. In intuitionistic logic, the law of excluded middle ($P \vee \neg P$) is not provable, and there is no term of type $\forall \alpha.\, \alpha + \neg\alpha$ in plain $\lambda^{\to}$. This is because a proof of $P \vee \neg P$ would require either a proof of $P$ or a proof of $\neg P$, with no "middle ground" allowed. Classical logic corresponds to lambda calculus extended with control operators (call/cc), which is a non-trivial extension.

Watch Out

Decidability of type checking depends on the system

Type checking for $\lambda^{\to}$ is decidable in polynomial time. Type checking for System F is decidable but type inference is not. Type checking for dependent types requires term normalization, so it is decidable only if the type theory is strongly normalizing (all well-typed terms terminate). If you add general recursion to a dependent type theory, type checking becomes undecidable.

Exercises

ExerciseCore

Problem

Write a term of type $(A \to B \to C) \to (A \to B) \to A \to C$ in the simply typed lambda calculus. What logical tautology does this type represent?

Hint

Reveal Solution

ExerciseCore

Problem

Prove that the type $A \to \neg\neg A$ is inhabited in $\lambda^{\to}$, where $\neg A$ is defined as $A \to \bot$. Then explain why $\neg\neg A \to A$ is not inhabited.

Hint

Reveal Solution

ExerciseAdvanced

Problem

In System F, the Church encoding of natural numbers is $\text{Nat} = \forall \alpha.\, (\alpha \to \alpha) \to \alpha \to \alpha$. Write the terms for zero, successor, and addition, and verify their types.

Hint

Reveal Solution

ExerciseAdvanced

Problem

Explain why type inference for System F is undecidable, while type inference for the Hindley-Milner system (used in Haskell and ML) is decidable. What restriction does Hindley-Milner impose?

Hint

Reveal Solution

References

Canonical:

• Girard, Lafont, Taylor, Proofs and Types (1989), Chapters 1-11
• Pierce, Types and Programming Languages (2002), Chapters 9-11 (simply typed), 23-25 (System F)

Additional:

• Sorensen and Urzyczyn, Lectures on the Curry-Howard Isomorphism (2006), Chapters 1-8
• Barendregt, "Lambda Calculi with Types" in Handbook of Logic in Computer Science (1992), Volume 2

Connection to proof assistants:

• The Coq Development Team, The Coq Reference Manual (2024), Chapter 4 (CIC)
• de Moura and Ullrich, "The Lean 4 Theorem Prover and Programming Language" (CADE 2021)

Next Topics

• Proof theory and cut elimination: the logical side of the Curry-Howard correspondence, where normalization of proofs corresponds to computation
• Dependent type theory: the full extension where types can depend on values, enabling the encoding of mathematical theorems