====== Type Theory ====== 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. ===== Background and Origins ===== 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|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. ===== Developments in the Twentieth Century ===== 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. ===== Applications in Computer Science ===== 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. ===== Relationship to Set Theory ===== 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. [[type-theory-foundations-debate|See the debate page for competing foundational viewpoints.]] ===== Consensus Status ===== 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 [[type-theory-mathematics-consensus|mathematics consensus page]] and [[type-theory-computer-science-consensus|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. ===== Viewpoints ===== * **[[type-theory-foundationalist-viewpoint|Foundationalist]]** - Type theory provides a superior foundation for mathematics because it is constructive, proof-relevant, and has direct computational content that ZFC-style set theory lacks. * **[[type-theory-pluralist-viewpoint|Foundational Pluralist]]** - Multiple foundations, including set theory and various type theories, are legitimate tools; no single system need be chosen as the unique basis for mathematics. * **[[type-theory-set-theory-primacy-viewpoint|Set-Theory Primacy]]** - ZFC and its extensions remain the appropriate foundation; type theory is a useful tool but not a replacement for classical set-theoretic foundations. * **[[type-theory-computational-viewpoint|Computational / Curry-Howard]]** - The identification of proofs with programs is the central insight, and type theory's value lies primarily in its applications to verified computation and programming language design. * **[[type-theory-predicativist-viewpoint|Predicativist]]** - Only predicative type theories (those avoiding impredicative definitions) are fully justified; impredicative systems such as the Calculus of Constructions outrun constructive justification. ===== Related Pages ===== * [[type-theory-history|Type Theory - History]] * [[type-theory-debate|Type Theory - Debate]] * [[type-theory-foundations-debate|Type Theory - Foundations Debate]] * [[type-theory-mathematics-consensus|Type Theory - Mathematics Consensus]] * [[type-theory-computer-science-consensus|Type Theory - Computer Science Consensus]] * [[principia-mathematica|Principia Mathematica]] * [[set-theory|Set Theory]] * [[lambda-calculus|Lambda Calculus]] * [[homotopy-type-theory|Homotopy Type Theory]] * [[curry-howard-correspondence|Curry-Howard Correspondence]] * [[proof-assistants|Proof Assistants]] ===== Footnotes ===== - Russell, Bertrand, and Alfred North Whitehead. //Principia Mathematica//. 3 vols. Cambridge: Cambridge University Press, 1910-1913. - Church, Alonzo. "A Formulation of the Simple Theory of Types." //Journal of Symbolic Logic// 5, no. 2 (1940): 56-68. - Martin-Lof, Per. "An Intuitionistic Theory of Types: Predicative Part." In //Logic Colloquium '73//, edited by H. E. Rose and J. C. Shepherdson, 73-118. Amsterdam: North-Holland, 1975. - The Univalent Foundations Program. //Homotopy Type Theory: Univalent Foundations of Mathematics//. Institute for Advanced Study, 2013. https://homotopytypetheory.org/book/ - Howard, William A. "The Formulae-as-Types Notion of Construction." In //To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism//, edited by J. P. Seldin and J. R. Hindley, 479-490. Academic Press, 1980. (Circulated as a manuscript from 1969.) - Ramsey, Frank P. "The Foundations of Mathematics." //Proceedings of the London Mathematical Society// s2-25, no. 1 (1926): 338-384.