Type theory is a branch of mathematical logic and the foundations of mathematics in which every expression is assigned a “type” - a classification that determines how it may be used in further reasoning. Originally developed to block the logical paradoxes that threatened early set-theoretic foundations, type theory has grown into a broad field with applications in logic, programming language design, and proof verification. The central idea is that restricting which objects may be predicated of which others prevents self-referential contradictions while preserving the expressive power needed for mathematics and computation.
The immediate motivation for type theory was Bertrand Russell's discovery in 1901 of a contradiction in Gottlob Frege's Grundgesetze der Arithmetik: the set of all sets that do not contain themselves neither can nor cannot contain itself. Russell's response, developed with Alfred North Whitehead in Principia Mathematica (1910-1913), was a ramified theory of types in which objects are stratified into a hierarchy - individuals, properties of individuals, properties of properties, and so on - with the rule that a predicate may only apply to objects of a lower type. This blocks the paradox by making the offending self-application grammatically ill-formed rather than false.
Earlier work by Gottlob Frege had distinguished between objects and concepts, and Henri Poincare had argued that impredicative definitions - those that quantify over a totality that includes the thing being defined - were the root of the paradoxes. Russell's ramified types incorporated a predicativity requirement; a simplified version, the simple theory of types, was later articulated principally by Frank Ramsey in 1926, with Rudolf Carnap subsequently developing related ideas, dropping the ramification while retaining the basic stratification.
Alonzo Church introduced simply typed lambda calculus in 1940, combining type theory with the lambda calculus he had developed in the early 1930s. This formalism became foundational for both mathematical logic and theoretical computer science. Per Martin-Lof developed intuitionistic type theory beginning in the 1970s, a constructive framework in which a proof of a proposition is identified with a term of the corresponding type - the propositions-as-types correspondence, also called the Curry-Howard correspondence after Haskell Curry and William Howard, who identified related connections between proof systems and type systems. Martin-Lof's system includes dependent types, in which the type of a term may depend on the value of another term, substantially increasing expressive power.
Homotopy type theory (HoTT), developed in the 2000s and 2010s and presented collectively in the Homotopy Type Theory book (2013), extends Martin-Lof type theory with an interpretation of types as topological spaces (up to homotopy equivalence) and adds the univalence axiom, which identifies equivalent types. HoTT has attracted attention as a potential new foundation for mathematics with direct computational content.
Type systems in programming languages are applied instances of type-theoretic ideas. Static type checking - verifying type correctness before a program runs - catches a class of errors at compile time. Dependent type systems, implemented in proof assistants such as Coq, Agda, Lean, and Idris, allow programs and their correctness proofs to be written in a single unified language. The Curry-Howard correspondence underlies these systems: writing a program and proving a theorem become the same activity. Industrial programming languages have moved toward richer type systems over time, with generics, algebraic data types, and gradual typing becoming common.
Type theory and set theory offer competing approaches to the foundations of mathematics. Set theory, particularly Zermelo-Fraenkel set theory with the axiom of choice (ZFC), is the dominant working foundation used by most mathematicians. Type theory's proponents argue that it has computational content that set theory lacks and that dependent and homotopy type theories provide a more natural account of mathematical practice. The debate over which framework better serves as a foundation for mathematics is ongoing. See the debate page for competing foundational viewpoints.
There is broad consensus in mathematical logic and theoretical computer science that type theory, in its various forms, is a consistent and useful framework for both foundations and programming language design. The mathematics consensus page and computer science consensus page address areas of agreement in their respective fields. Foundational questions - which type theory, and whether type theory should displace set theory - remain open and contested.