Type theory — from simple types to dependent types

Parent: logic

Add types to the λ-calculus and, via Curry–Howard, you get a logic — and, made dependent, a foundation for all of mathematics.

Simply-typed λ-calculus (STLC)

Types = base types + arrows A → B. Key fact: STLC is strongly normalizing — every term halts. You lose Turing-completeness and gain consistency: as a logic (Curry–Howard) STLC = intuitionistic propositional logic. Totality ⟺ consistency is the recurring threshold — general recursion would reintroduce ⊥.

The λ-cube (Barendregt) — three ways to add power

• terms depend on types → polymorphism (System F: ∀α. α→α);
• types depend on types → type operators;
• types depend on terms → dependent types. All three together = the Calculus of Constructions (CoC), the corner of the cube — the core of Lean/Coq.

(STLC at the near corner; each axis adds one dependency; CoC at the far corner has all three.)

Dependent types — types indexed by values

Vec A n = lists of A of length n; Π(x:A). B x = a function whose return type depends on the argument; Σ(x:A). B x = a pair whose second type depends on the first. By Curry–Howard, Π = ∀ and Σ = ∃, so a type can express any proposition, and a term of that type is its proof.

Martin-Löf type theory (MLTT)

The constructive foundation of mathematics: dependent types + inductive types (build ℕ, lists, trees) + identity types (a = b is itself a type — equality as a proposition to be proved) + a universe hierarchy (Type 0 : Type 1 : …, avoiding Russell-style paradox). An alternative to set theory — computational by construction (proofs run).

The trade

A total type theory (all terms halt) is a consistent logic but not Turing-complete; allowing non-termination buys general recursion at the cost of consistency. Proof assistants keep totality for the proof layer and sandbox partiality elsewhere. → proof-theory, lean4.