← Universes Index Next: Definitional vs propositional equality →

Recall

Formal definitions cited in this section, gathered here for quick reference (full citations in the Bibliography):

Chapters 1–4 have relied on Lean’s type checking constantly without ever seeing its rules written down. This section makes two things precise: the actual rules Lean’s kernel checks a term against (using a small, representative fragment, the simply typed λ-calculus, STLC), and the specific rule governing the universe hierarchy Section 2 just introduced informally.

An untyped calculus has a serious defect: it permits terms that reduce forever (Chapter 1, Section 4 mentioned β-reduction; nothing there stopped a term from β-reducing to itself, endlessly), and nothing prevents applying one kind of value where a completely different kind was intended. STLC fixes this by attaching a type to every term and requiring application to respect types — the direct ancestor of Chapter 1’s “every expression has a type.”

Types

\[\tau ::= \iota \;\mid\; \tau \to \tau\]

where $\iota$ ranges over some fixed collection of base types (think Nat, Bool) and $\tau_1 \to \tau_2$ is the type of functions from $\tau_1$ to $\tau_2$ — exactly Lean’s →. Every type is built from base types and arrows. There is not yet any way to quantify over all types the way Chapter 1’s identity {α : Type} (x : α) : α := x did — that extra generality is exactly Chapter 1, Section 5’s Π-types, already covered.

Programmer’s corner (Python), before the formal rules. Python’s own type hints plus mypy are a light version of exactly this system, worth seeing first since this Python tooling runs today, without any Lean installation at all:

def apply_twice(f: int, x: int) -> int:  # pretend f is Callable[[int], int]
    ...

def to_str(n: int) -> str:
    return str(n)

# mypy accepts this: to_str's declared input type (int) matches what
# it is given (an int literal).
to_str(5)

# mypy rejects this with an error, WITHOUT running anything:
# error: Argument 1 to "to_str" has incompatible type "str"; expected "int"
to_str("already a string")

mypy’s check on to_str("already a string") is exactly the (App) rule below, refusing to combine a function with an argument of the wrong type, caught by reading the code rather than running it. The difference is that Python’s hints are optional and only checked when mypy is run at all; Lean’s type system is not optional, is checked on every single elaboration, and is a real part of the language’s meaning rather than an add-on linter. STLC below is what is actually going on, underneath both.

Typing judgments and rules

A typing judgment $\Gamma \vdash t : \tau$ reads “in context $\Gamma$ (a list of variable-type assignments $x_1:\tau_1, \ldots, x_n:\tau_n$), the term $t$ has type $\tau$.” This is precisely what Lean’s #check reports, and precisely the “context” that appears above the line in every tactic goal state since Chapter 4. The rules that generate valid judgments:

\[\dfrac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau} \;\text{(Var)} \qquad \dfrac{\Gamma, x:\tau_1 \vdash t : \tau_2}{\Gamma \vdash \lambda x.\, t : \tau_1 \to \tau_2} \;\text{(Abs)} \qquad \dfrac{\Gamma \vdash t_1 : \tau_1 \to \tau_2 \quad \Gamma \vdash t_2 : \tau_1}{\Gamma \vdash t_1\, t_2 : \tau_2} \;\text{(App)}\]

Each rule, read as a Lean fact already familiar from earlier chapters:

Type preservation and progress: the payoff

Two theorems about STLC are the entire reason to bother with a type system at all:

Together, progress and preservation are the formal content of “well-typed programs do not go wrong,” and, viewed through Curry–Howard (Chapter 3), “well-typed proof terms do not prove something other than what they claim to prove.” The entire reliability of Lean as a proof assistant rests on an extended version of exactly these two theorems, proved once for Lean’s kernel and then trusted for every proof checked thereafter.

What STLC still cannot do

STLC cannot type identity from Chapter 1 polymorphically. One could write identity_Nat : Nat → Nat and separately identity_Bool : Bool → Bool, one arrow-type definition per base type. But there is no single term of a single STLC type that captures “the identity function, at every type.”

Programmer’s corner (Python), on the same limitation. Plain Python never runs into this, because it has no static types to begin with — def identity(x): return x already works on anything, at runtime, with zero declarations. But the instant type hints are added, wanting mypy to check the general claim “this returns whatever type it was given” requires a dedicated feature, TypeVar, precisely because bare hints have the same limitation as STLC:

from typing import TypeVar
T = TypeVar("T")

def identity(x: T) -> T:   # one signature, valid at every type
    return x

identity(5)        # T := int
identity("hello")  # T := str

Without TypeVar, the only option would be writing identity_int(x: int) -> int and identity_str(x: str) -> str separately — exactly STLC’s one-arrow-type-per-base-type wall. TypeVar is Python typing’s escape hatch for this specific gap, and it is a useful anchor: a much lighter version of the same extra generality Lean’s identity {α : Type} (x : α) : α := x uses, where α is filled in silently every call, the same way mypy silently solves T := int above.

This is precisely the gap Chapter 1, Section 5 already closed: dependent types let a type itself depend on a term (here, the type argument α). That is exactly the extra generality identity {α : Type} (x : α) : α := x uses, and it is unavailable in STLC (or in Python’s TypeVar, which is real but considerably less powerful — it cannot let a return type depend on an ordinary value argument the way Chapter 1, Section 3’s Vec.replicate does).

Universes, as a typing rule

Section 2 introduced the hierarchy $\mathtt{Type} : \mathtt{Type}\,1 : \mathtt{Type}\,2 : \cdots$ to avoid a Russell-style paradox (a “type of all types” that contains itself leads to the same contradiction as “the set of all sets that do not contain themselves”), and showed Group : Type → Type had to live in Type 1. In the calculus of constructions — the formal system CoC/CIC that Chapter 1, Section 5 named, extending STLC above with Π-types and universes — this is stated as a typing rule for the universes themselves:

\[\dfrac{}{\mathtt{Type}\,i : \mathtt{Type}\,(i+1)}\]

together with a rule saying Π-types (function types, including ordinary →) stay inside a suitable universe:

\[\dfrac{\Gamma \vdash A : \mathtt{Type}\,i \quad \Gamma, x:A \vdash B : \mathtt{Type}\,j} {\Gamma \vdash \big(\textstyle\prod_{x:A} B\big) : \mathtt{Type}\,(\max(i,j))}\]

This is exactly Section 2’s Group : Type → Type computation spelled out as a general rule: with $A = \mathtt{Type}$ (itself living in Type 1) and $B = \mathtt{Type}$ again, the rule gives $\max(1, 1) = 1$, so Type → Type lands in Type 1, one level above Type itself.

Programmer’s corner (Python), on why this is genuinely a type-theory concern and not a Python one. In Python, type(3) is int, and type(int) is type — and, unlike Lean’s stratified hierarchy, type(type) is also type:

>>> type(3)
<class 'int'>
>>> type(int)
<class 'type'>
>>> type(type)
<class 'type'>

Python allows type to be its own type, with no stratification at all, because Python’s type system is not being used as a proof system — there is no soundness property at stake that a Russell-style paradox could break. Lean’s Type cannot self-apply this way (Type : Type is inconsistent — it allows encoding Girard’s paradox and proving False), which is exactly why the infinite, strictly increasing hierarchy above is load-bearing rather than pedantry. This is one of the few places where the Python comparison genuinely runs out: it is not that Python does the same thing more simply, it is that Python does not need to solve this problem at all, because nothing checks proofs against it.

References

Full citations in the Bibliography. Formal definitions are gathered in Recall, above.

← Universes Index Next: Definitional vs propositional equality →
Try Lean
Lean playground · v1.4.18 ↗