Type Theory

Type theory is a family of formal systems in which expressions are assigned types that govern how they may be constructed and used. It provides foundations for mathematics, languages for expressing logical reasoning, and frameworks for studying computation. Unlike a single fixed theory, it encompasses systems with different rules for functions, equality, quantification, and data. Its central judgment, commonly written $a:A$, states that the term $a$ has type $A$. In some systems, terms represent mathematical objects; in others, they also represent programs and proofs. (archive-pml.github.io)

Origins and development

Early type theories addressed paradoxes arising from unrestricted definitions and self-reference. Bertrand Russell’s 1908 formulation organized expressions into levels, restricting which objects could occur as arguments to which functions. This approach blocked problematic self-application by imposing distinctions between types and, in his ramified theory, between orders of definition. It formed part of an effort to establish consistent logical foundations for mathematics. (upload.wikimedia.org)

Alonzo Church’s 1940 paper, A Formulation of the Simple Theory of Types, presented a simpler typed logical framework built around function abstraction and application. It combined typed lambda calculus with logical constants, providing a formulation of higher-order logic. Later, Martin-Löf’s intuitionistic type theory developed a constructive framework incorporating dependent types, in which mathematical propositions and their proofs can be expressed alongside objects and computations. (classes.cs.uchicago.edu)

Judgments, terms, and rules

A typing judgment is usually written

where $\Gamma$ is a context listing assumptions such as $x:A$. The judgment means that, under those assumptions, $a$ has type $A$. A theory specifies inference rules for deriving valid judgments rather than treating typing as an informal classification. Dependent theories may also include judgments asserting that a type is well formed or that two expressions are definitionally equal. (archive-pml.github.io)

A function type $A\to B$ describes functions taking arguments of type $A$ to results of type $B$. If $f:A\to B$ and $a:A$, application gives $f(a):B$. Abstraction constructs functions: an expression $b:B$ depending on $x:A$ yields $\lambda x.b:A\to B$. Applying this abstraction to an argument computes by substitution, a rule known as beta reduction. (leanprover.github.io)

Product types represent pairs, while sum types represent alternatives distinguished by constructors. These constructions resemble Cartesian products and disjoint unions, but a type theory specifies their introduction, elimination, and computation rules directly. Inductive types define objects through constructors; for example, natural numbers can be generated by zero and successor, with corresponding principles of recursion and induction. (docs.lean-lang.org)

Propositions and proofs

The Curry–Howard correspondence relates propositions to types and proofs to terms. In its basic constructive interpretation, a proof of $P\to Q$ is a function transforming a proof of $P$ into a proof of $Q$. A proof of a conjunction contains proofs of both components, while a proof of a disjunction identifies an alternative and supplies its proof. Thus, rules of natural deduction have counterparts in typed term construction. (docs.lean-lang.org)

This connection makes constructing a formal proof closely related to constructing a well-typed expression. It also explains the relationship between computational type theories and intuitionistic logic: existence and disjunction carry explicit evidence. Nevertheless, type theory is not necessarily intuitionistic. Classical principles, including the law of excluded middle, can be introduced through additional axioms or other logical mechanisms. (docs.lean-lang.org)

Dependent types and universes

In dependent type theory, a type may depend on a term. For example, $\mathrm{Vec}(A,n)$ can describe sequences of elements of $A$ having length $n$. Length then becomes part of the type rather than merely an externally stated property. Dependent function types, written $\prod_{x:A}B(x)$, assign an output type that may vary with the input; ordinary function types are the special case where it does not vary. (archive-pml.github.io)

Dependent pair types, written $\sum_{x:A}B(x)$, contain an object $a:A$ together with an object of type $B(a)$. Under propositions-as-types, dependent functions express universal quantification, while dependent pairs express existence with a witness and supporting evidence. (archive-pml.github.io)

Type universes allow types themselves to occur as objects. Many systems organize universes into a hierarchy, such as $\mathcal U_0:\mathcal U_1:\mathcal U_2:\cdots$, rather than permitting an unrestricted universe of all types that contains itself. Universe formation and inclusion rules vary between theories. (leanprover.github.io)

Equality and homotopical interpretations

Many dependent theories distinguish definitional equality, determined by computation rules, from propositional equality, expressed by an identity type whose terms are equality proofs. Two expressions may therefore compute to the same result without requiring a separate proof, whereas other equalities must be established by constructing evidence. (archive-pml.github.io)

Homotopy type theory interprets types as spaces and equality proofs as paths. Equalities between equality proofs then resemble homotopies between paths, producing higher-dimensional structure. Its univalence axiom states that the canonical map from equality between types to equivalence between them is itself an equivalence. This connects typed foundations with topology and permits equivalent structures to be identified through equality in a universe. (homotopytypetheory.org)

Computation and proof checking

In computer science, type theory supplies mathematical tools for designing programming languages and establishing properties of evaluation. A standard type-safety argument combines preservation—evaluation preserves typing—with progress—a closed, well-typed expression is a value or can take an evaluation step. These guarantees concern specified operational behavior; they do not imply that every program terminates or fulfills its intended purpose. (cs.cmu.edu)

Type-theoretic proof assistants, including Lean, use typing to check mathematical proofs. Their core checker verifies proof terms against the propositions they claim to establish. This supports formal verification, while leaving the correctness of the chosen specification and the acceptability of assumed axioms as separate questions. (lean-lang.org)