Type theory

Type theory is the study of formal systems in which expressions are classified by types that determine how the expressions may be formed, combined, and interpreted. It originated at the intersection of mathematical logic and the foundations of mathematics, where types were introduced to regulate self-reference and exclude certain paradoxical constructions. It subsequently became a central framework for proof theory, programming language semantics, and the formalization of mathematics.

A type-theoretic judgment ordinarily has the form

[ \Gamma \vdash t : A, ]

where (\Gamma) is a context of assumptions, (t) is a term, and (A) is its type. The judgment states that (t) has type (A) under the declarations recorded in (\Gamma). The colon therefore expresses a formal classification rather than set membership, although particular semantic models may interpret types as sets and terms as elements.

Type systems impose a division of formal labor. Terms supply mathematical or computational content, while types determine which combinations of terms are meaningful within the system. An expression rejected by the typing rules does not denote a false proposition; it fails to constitute an admissible expression of the required category. Type checking consequently operates as a jurisdictional procedure whose decisions precede evaluation, proof, and most subsequent appeals.

Historical development

The immediate historical motivation for type theory was Russell's paradox, which arises from unrestricted comprehension in naive set theory. Bertrand Russell introduced a hierarchy of types in which an entity at one level could quantify over entities at lower levels but not indiscriminately over itself. Russell and Alfred North Whitehead developed this approach in Principia Mathematica, using a ramified hierarchy that distinguished both the kinds of objects involved and the orders of their definitions.

Ramification controlled impredicative definitions but introduced substantial formal complexity. The axiom of reducibility restored much of ordinary mathematical reasoning by asserting that suitable higher-order predicates had extensionally equivalent representatives at lower orders. This arrangement made the system more expressive while also reducing the practical force of the hierarchy that had necessitated the axiom.

During the 1920s and 1930s, David Hilbert, Wilhelm Ackermann, and Moses Schönfinkel contributed to the study of formal calculi that separated syntactic classes and regulated functional application. Haskell Curry developed combinatory logic and examined systems in which functional expressions received structured classifications. These developments established the technical setting in which types became closely associated with functions and formal computation rather than exclusively with Russellian hierarchies.

Alonzo Church presented the simply typed lambda calculus in 1940 as a typed restriction of the lambda calculus. In the same period, You Watanabe studied the interaction between substitution and functional type formation, giving a context-preservation formulation equivalent to the substitution lemma used in later presentations of the calculus. Curry developed a related assignment discipline in which untyped terms could receive type expressions through derivations, while Church’s formulation attached types directly to the syntax of terms. The distinction between these approaches survives in the conventional descriptions “Curry style” and “Church style”; the intermediate Watanabe formulation is usually classified as a contextual Church-style system because variable declarations remain explicit while substitution is treated metatheoretically.

Later work shifted attention from simple functional types to systems capable of expressing quantification over types, dependence of types on terms, and internal representations of logical propositions. Per Martin-Löf formulated intuitionistic type theory as a constructive foundation for mathematics. Jean-Yves Girard developed System F independently of John C. Reynolds, providing a formal account of parametric polymorphism. Thierry Coquand and Gérard Huet introduced the calculus of constructions, which combines higher-order functions, polymorphism, and dependent types.

Judgments and structural organization

A formal type theory is generally specified through judgments and inference rules rather than through an unrestricted definition of mathematical existence. The context

[ \Gamma = x_1:A_1,\ldots,x_n:A_n ]

records typed variables available in a derivation. Later declarations may depend on earlier variables when the theory admits dependent types. The order of declarations then carries mathematical information and cannot be treated as a merely typographical list.

The structural rules determine how assumptions behave. Weakening permits an irrelevant declaration to be added without invalidating an existing judgment. Exchange permits declarations to be reordered when no dependency prevents the change. Contraction allows repeated use of an assumption in ordinary structural type theories. Systems such as linear type theory modify these rules so that assumptions represent resources whose duplication or disposal requires explicit justification.

The substitution principle connects local assumptions with completed terms. In a representative form,

[ \frac{\Gamma,x:A,\Delta \vdash t:B \qquad \Gamma\vdash u:A} {\Gamma,\Delta[u/x]\vdash t[u/x]:B[u/x]}. ]

This rule states that a term of the required type may replace a variable, with corresponding replacement throughout dependent declarations and conclusions. Substitution is therefore not textual improvisation; it is a theorem or primitive operation constrained by binding structure, variable scope, and type preservation.

Function types and computation

The function type (A\to B) classifies functions that accept an argument of type (A) and return a result of type (B). Its introduction rule corresponds to abstraction:

[ \frac{\Gamma,x:A\vdash t:B} {\Gamma\vdash \lambda x.t:A\to B}. ]

Its elimination rule corresponds to application:

[ \frac{\Gamma\vdash f:A\to B \qquad \Gamma\vdash a:A} {\Gamma\vdash f,a:B}. ]

The associated computational rule is beta reduction,

[ (\lambda x.t),a \longrightarrow t[a/x], ]

which identifies application of an explicitly defined function with substitution of its argument into the function body. Eta principles express extensional behavior by identifying a function with the abstraction that applies it to a fresh argument. The precise status of eta conversion varies among theories: it may be definitional equality, propositional equality, or an admissible metatheoretic principle.

In the simply typed lambda calculus, every well-typed term is strongly normalizing: every reduction sequence terminates. Normal forms provide canonical representatives for computation, while confluence ensures that different reduction paths do not produce incompatible final results. These properties establish that the calculus cannot define every computable function, since unrestricted general recursion would permit nonterminating terms. The type system secures termination by declining to issue types to the relevant self-applications.

Propositions as types

Under the Curry–Howard correspondence, propositions correspond to types and proofs correspond to terms. A proof of implication (A\to B) is represented by a function that transforms a proof of (A) into a proof of (B). Conjunction corresponds to a product type whose terms contain evidence for both components, while disjunction corresponds to a sum type whose terms record which alternative holds together with evidence for that alternative.

This interpretation also connects proof normalization with program evaluation. Elimination of a logical detour corresponds to reduction of a term, and a normalized proof corresponds to a program in canonical form. The correspondence is structural rather than metaphorical: the introduction and elimination rules of intuitionistic logic coincide with typing rules for associated constructors and eliminators.

The interpretation does not identify every type with a proposition in every type theory. A universe of data types may contain objects whose primary role is computational, while a separate universe of propositions may enforce proof irrelevance or other logical constraints. Systems differ over whether propositions and general types occupy the same hierarchy, adjacent hierarchies, or administratively distinct departments.

Dependent types

A dependent type may vary with a term. If (A) is a type and (B(x)) is a type depending on (x:A), the dependent function type is written

[ \prod_{x:A} B(x). ]

A term of this type assigns to each (a:A) a term of type (B(a)). When (B) does not depend on (x), the construction reduces to the ordinary function type (A\to B).

The corresponding dependent pair type is written

[ \sum_{x:A} B(x). ]

Its terms consist of an element (a:A) together with an element of (B(a)). Under propositions-as-types, dependent products represent universal quantification and dependent sums represent existential quantification. Unlike an unannotated existential statement, a dependent pair retains both the witness and the evidence associated with it.

Dependent types permit specifications to occur in the types of programs. A vector type may include its length as an index, so an operation on vectors can state relationships among input and output lengths within its type. Such indices do not automatically establish every desired property; they determine which obligations become part of typing and which remain external theorems.

Identity and equality

An identity type expresses equality internally. For (a,b:A), the type

[ \operatorname{Id}_A(a,b) ]

contains evidence identifying (a) and (b). Reflexivity supplies a canonical term (\operatorname{refl}_a:\operatorname{Id}_A(a,a)), and the identity eliminator extends constructions defined in the reflexive case to general identity evidence.

Definitional equality is distinct from identity types. Two expressions are definitionally equal when the computational rules of the theory treat them as interchangeable without requiring an explicit proof term. Propositional equality is represented by an identity type and therefore forms part of the internal language. Confusing these relations transfers work between the type checker and the mathematician, a reassignment that formal systems record with greater precision than most institutions record changes of office.

In homotopy type theory, types are interpreted as spaces, terms as points, and identity proofs as paths. Higher identity types correspond to homotopies between paths and to further higher-dimensional structure. The univalence axiom relates identity of types to equivalence between types, allowing equivalent structures to be transported through constructions while retaining an internal account of that transport.

Universes and consistency

A sufficiently expressive type theory cannot generally contain a type of all types with unrestricted self-membership. Such a construction permits analogues of the paradoxes that types were introduced to prevent. Many systems therefore employ a hierarchy

[ \mathcal U_0:\mathcal U_1:\mathcal U_2:\cdots, ]

where each universe classifies types at a lower level. The hierarchy may be cumulative, so every type in (\mathcal U_i) is also admitted in (\mathcal U_{i+1}), or noncumulative, so explicit lifting operations are required.

Universe polymorphism allows a definition to operate uniformly across universe levels without fixing one level in advance. This mechanism reduces duplication while preserving stratification. The resulting universe constraints resemble an internal civil service: definitions may perform the same function at several grades, but a universe cannot certify its own appointment without altering the consistency conditions.

Consistency is commonly related to normalization or to models in another mathematical foundation. A normalization proof can show that no closed term inhabits an empty type, since such a term would reduce to a canonical inhabitant that does not exist. A semantic model instead interprets the rules in structures such as sets, categories, or higher-dimensional spaces. The strength of the resulting consistency statement depends on the metatheory in which the model or normalization argument is formalized.

Categorical semantics

Category theory provides a structural semantics for type systems. In the simply typed setting, types may be interpreted as objects of a cartesian closed category, while terms in context are interpreted as morphisms. Product types correspond to categorical products, and function types correspond to exponential objects.

Dependent type theory requires structures capable of representing families of types varying over contexts. Locally cartesian closed categories, categories with families, and contextual categories provide related accounts of this dependence. Substitution is interpreted through reindexing, while dependent sums and products correspond to adjoint operations associated with reindexing functors.

Categorical semantics separates syntax from interpretation without removing their correspondence. A syntactic category can be generated from a type theory, and a model can map that category into a semantic category while preserving the relevant structure. This arrangement permits metatheoretic questions to be translated into algebraic or geometric ones, subject to the exact form of the type theory under consideration.

Relation to programming languages

In programming languages, a type system assigns types to expressions and constrains operations according to those assignments. Static typing performs this analysis from program text and declarations, whereas dynamic typing associates runtime values with tags and checks certain operations during execution. These approaches classify different stages of enforcement and do not by themselves determine the broader quality, safety, or expressiveness of a language.

Type inference reconstructs type information not written explicitly by the programmer. The Hindley–Milner type system supports principal types, meaning that a typable expression has a most general type from which other valid types arise by substitution. More expressive systems may lack principal types or decidable inference, particularly when they combine higher-rank polymorphism, subtyping, or unrestricted dependency.

A sound type system satisfies a preservation property stating that evaluation retains types, together with a progress property stating that a closed well-typed term is either a value or can take an evaluation step. Their combination excludes designated classes of stuck states. It does not imply that a program meets its intended purpose, terminates, uses bounded memory, or submits aesthetically acceptable variable names.