Dependent Type Theory

Why This Matters

In simply typed lambda calculus, types and values live in separate worlds: the type $\mathbb{N} \to \mathbb{N}$ does not know which natural number you pass in. Dependent type theory erases this boundary. A type can mention a value: $\text{Vec}(\mathbb{R}, n)$ is the type of real-valued vectors of length $n$, where $n$ is a natural number.

This fusion of types and values has a profound consequence: propositions become types, and proofs become terms. The statement "for all $n$, $n + 0 = n$" becomes a dependent function type $\prod_{n : \mathbb{N}} (n + 0 =_\mathbb{N} n)$, and a proof of this statement is a term of that type. This is why Lean, Coq, and Agda use dependent type theory: mathematical assertions and their proofs live in the same language.

Prerequisites

This page assumes familiarity with lambda calculus, specifically simply typed lambda calculus and the basic Curry-Howard correspondence (types as propositions, terms as proofs, function types as implications).

Core Definitions

Definition

Dependent Function Type (Pi Type)

The Pi type $\prod_{x:A} B(x)$ is the type of functions that take an input $x$ of type $A$ and return an output of type $B(x)$, where the output type depends on the input value.

A term $f : \prod_{x:A} B(x)$ is a function such that for each $a : A$, we have $f(a) : B(a)$.

When $B$ does not depend on $x$, this reduces to the ordinary function type $A \to B$.

Definition

Dependent Pair Type (Sigma Type)

The Sigma type $\sum_{x:A} B(x)$ is the type of pairs $(a, b)$ where $a : A$ and $b : B(a)$. The type of the second component depends on the value of the first.

When $B$ does not depend on $x$, this reduces to the ordinary product type $A \times B$.

Definition

Propositions as Types (Curry-Howard for Dependent Types)

In dependent type theory, logical connectives correspond to type formers:

Logic	Type theory
$\forall x \in A.\, P(x)$	$\prod_{x:A} P(x)$
$\exists x \in A.\, P(x)$	$\sum_{x:A} P(x)$
$P \implies Q$	$P \to Q$
$P \land Q$	$P \times Q$
$P \lor Q$	$P + Q$ (sum type)
True	Unit type $\mathbf{1}$
False	Empty type $\mathbf{0}$

A proposition is "true" if its corresponding type is inhabited (has a term). A proof of $\forall x.\, P(x)$ is a function that takes any $x$ and produces a proof of $P(x)$.

Definition

Identity Type (Propositional Equality)

The identity type $a =_A b$ is the type of proofs that $a$ and $b$ are equal as elements of type $A$. It is inhabited if and only if $a$ and $b$ are (propositionally) equal. The canonical constructor is $\text{refl}_a : a =_A a$.

Main Theorems

Theorem

Curry-Howard Correspondence (Dependent Version)

Statement

There is a precise correspondence between:

1. Propositions in constructive predicate logic and types in dependent type theory.
2. Proofs and terms (programs): a proposition $P$ is provable if and only if the type $P$ is inhabited.
3. Proof simplification (cut-elimination) and program evaluation (beta-reduction).

In particular, type-checking a term verifies that a proof is correct. The problem of theorem proving reduces to the problem of term construction.

Intuition

Writing a proof and writing a program are the same activity. When you prove "for all natural numbers $n$, $n + 0 = n$" in Lean, you construct a function that takes $n : \mathbb{N}$ and returns a term of type $n + 0 =_\mathbb{N} n$. The type-checker verifies correctness.

Proof Sketch

The correspondence is structural, not a single theorem to prove. For each logical rule (introduction and elimination of connectives), there is a corresponding typing rule for lambda terms. Universal quantification introduction corresponds to lambda abstraction for Pi types. Existential quantification introduction corresponds to pair formation for Sigma types. Modus ponens corresponds to function application. The meta-theorem is that derivations in constructive logic biject with well-typed terms.

Why It Matters

This correspondence is the reason proof assistants work. Lean's kernel is a type-checker: it does not search for proofs, it verifies that a proposed term has the claimed type. The entire trust base of a proof assistant is a type-checker, which can be small and auditable. This is a much smaller trusted computing base than a general-purpose automated theorem prover.

Failure Mode

The correspondence holds for constructive logic, not classical logic. Classical principles like the law of excluded middle ($P \lor \neg P$) and double negation elimination ($\neg\neg P \implies P$) do not have computational content in the standard sense. They can be added as axioms, but the resulting "proofs" are not programs that compute witnesses. Lean and Coq allow classical reasoning by adding these axioms, at the cost of losing computational extraction for classical proofs.

Calculus of Inductive Constructions

Coq (now Rocq) and Lean are based on the Calculus of Inductive Constructions (CIC), which extends dependent type theory with:

1. Inductive types: datatypes defined by their constructors. Natural numbers are defined by $\text{zero} : \mathbb{N}$ and $\text{succ} : \mathbb{N} \to \mathbb{N}$. Lists, trees, and other data structures are similarly defined.

2. Pattern matching and recursion: functions on inductive types are defined by matching on constructors and recursing on structurally smaller arguments. Structural recursion guarantees termination.

3. A universe hierarchy: types themselves have types. $\mathbb{N} : \text{Type}_0$, $\text{Type}_0 : \text{Type}_1$, etc. This avoids Girard's paradox (the type-theoretic analogue of Russell's paradox).

The key property of CIC is strong normalization: every well-typed term reduces to a normal form in finite steps. This means that type-checking is decidable (the type-checker always terminates), and proofs cannot loop forever.

What Lean Looks Like

In Lean 4, a proof that addition is commutative looks like a function definition:

theorem add_comm : forall (n m : Nat), n + m = m + n := by
  intro n m
  induction n with
  | zero => simp
  | succ n ih => simp [Nat.succ_add]; exact ih

The by keyword enters tactic mode, where tactics construct the proof term incrementally. The kernel then verifies the resulting term has the correct type.

Why This Matters for ML

Dependent types are not directly used in most ML systems today. The connection is indirect:

1. Formal verification of ML systems: Projects like VeriML and verified neural network properties use dependent types to state and prove properties about ML algorithms.

2. Proof assistants for mathematical ML theory: The Lean Mathematics Library (Mathlib) formalizes significant portions of analysis, measure theory, and probability. The long-term goal is to formalize all of ML theory.

3. Neuro-symbolic integration: Systems that combine neural networks with symbolic reasoning increasingly use type-theoretic frameworks to ensure that the symbolic component is correct by construction.

Common Confusions

Watch Out

Dependent types are not just generics

In Java or Python, generic types like List<T> are parameterized by types. Dependent types are parameterized by values: Vec(n) depends on the number $n$. You cannot express "a function that takes a number $n$ and returns a vector of length $n$" with generics alone. You need $\prod_{n:\mathbb{N}} \text{Vec}(\mathbb{R}, n)$.

Watch Out

Constructive does not mean weak

Constructive logic rejects the law of excluded middle as an axiom. This does not mean constructive proofs are weaker in practice. A constructive proof of $\exists x.\, P(x)$ actually produces a witness $x$, which is computationally more informative than a classical existence proof by contradiction. Most theorems in analysis and algebra have constructive proofs, though some require more work.

Watch Out

Lean and Coq allow classical reasoning

Although their foundations are constructive, both Lean and Coq allow you to assume classical axioms (excluded middle, choice). When you do, you lose the ability to extract programs from proofs of existence statements, but you gain the full power of classical mathematics. Most formalization projects freely use classical reasoning.

Exercises

ExerciseCore

Problem

Write the type (in dependent type theory notation) corresponding to the logical statement: "for every natural number $n$, there exists a natural number $m$ such that $m > n$."

Hint

Reveal Solution

ExerciseAdvanced

Problem

Explain why Girard's paradox (Type : Type) makes a type theory inconsistent, and how the universe hierarchy $\text{Type}_0 : \text{Type}_1 : \text{Type}_2 : \cdots$ avoids it.

Hint

Reveal Solution

ExerciseAdvanced

Problem

In the Curry-Howard correspondence, what does beta-reduction of a lambda term correspond to in logic? What does the Church-Rosser theorem (confluence) mean for proofs?

Hint

Reveal Solution

References

Canonical:

• Martin-Lof, Intuitionistic Type Theory (1984)
• The Univalent Foundations Program, Homotopy Type Theory (2013), Chapters 1-2

Practical:

• Avigad, Theorem Proving in Lean 4 (2023)
• Coquand & Huet, "The Calculus of Constructions" (1988)

Accessible:

• Pierce, Types and Programming Languages (2002), Chapters 23, 29-30

Next Topics

The main extensions of dependent type theory:

• Formal verification of ML: applying these ideas to prove properties of ML systems
• Proof theory and cut-elimination: the structural theory underlying the Curry-Howard correspondence