3. The Type System🔗

Terms, also known as expressions, are the fundamental units of meaning in Lean's core language. They are produced from user-written syntax by the elaborator. Lean's type system relates terms to their types, which are also themselves terms. Types can be thought of as denoting sets, while terms denote individual elements of these sets. A term is well-typed if it has a type under the rules of Lean's type theory. Only well-typed terms have a meaning.

Terms are a dependently typed λ-calculus: they include function abstraction, application, variables, and let-bindings. In addition to bound variables, variables in the term language may refer to constructors, type constructors, recursors, defined constants, or opaque constants. Constructors, type constructors, recursors, and opaque constants are not subject to substitution, while defined constants may be replaced with their definitions.

A derivation demonstrates the well-typedness of a term by explicitly indicating the precise inference rules that are used. Implicitly, well-typed terms can stand in for the derivations that demonstrate their well-typedness. Lean's type theory is explicit enough that derivations can be reconstructed from well-typed terms, which greatly reduces the overhead that would be incurred from storing a complete derivation, while still being expressive enough to represent modern research mathematics. This means that proof terms are sufficient evidence of the truth of a theorem and are amenable to independent verification.

In addition to having types, terms are also related by definitional equality. This is the mechanically-checkable relation that equates terms modulo their computational behavior. Definitional equality includes the following forms of reduction:

β (beta): Applying a function abstraction to an argument by substitution for the bound variable
δ (delta): Replacing occurrences of defined constants by the definition's value
ι (iota): Reduction of recursors whose targets are constructors (primitive recursion)
ζ (zeta): Replacement of let-bound variables by their defined values

Terms in which all possible reductions have been carried out are in normal form.

Definitional equality includes η-equivalence of functions and single-constructor inductive types. That is, fun x => f x is definitionally equal to f, and S.mk x.f1 x.f2 is definitionally equal to x, if S is a structure with fields f1 and f2. It also features proof irrelevance, so any two proofs of the same proposition are definitionally equal. It is reflexive, symmetric, and a congruence.

Definitional equality is used by conversion: if two terms are definitionally equal, and a given term has one of them as its type, then it also has the other as its type. Because definitional equality includes reduction, types can result from computations over data.

Computing types

When passed a natural number, the function LengthList computes a type that corresponds to a list with precisely that many entries in it:

def LengthList (α : Type u) : Nat → Type u
  | 0 => PUnit
  | n + 1 => α × LengthList α n

Because Lean's tuples nest to the right, multiple nested parentheses are not needed:

example : LengthList Int 0 := ()

example : LengthList String 2 :=
  ("Hello", "there", ())

If the length does not match the number of entries, then the computed type will not match the term:

example : LengthList String 5 :=
  ("Wrong", "number", application type mismatch
  ("number", ())
argument
  ()
has type
  Unit : Type
but is expected to have type
  LengthList String 3 : Type())

application type mismatch
  ("number", ())
argument
  ()
has type
  Unit : Type
but is expected to have type
  LengthList String 3 : Type

The basic types in Lean are universes, function types, and type constructors of inductive types. Defined constants, applications of recursors, function application, axioms or opaque constants may additionally give types, just as they can give rise to terms in any other type.