In mathematical logic, and theoretical computer science, type theory is the study of formal systems that classify expressions or mathematical objects by their types. Roughly speaking, a type plays a similar role to that played by a data type in programming: it specifies what kind of thing an expression is and how it may be used. Type theories are used in the study of programming languages (type systems), formal logic, and the formalization of mathematics.
Some type theories have been proposed as alternatives to set theory as a foundation of mathematics. Examples include Alonzo Church's simple theory of types and Per Martin-Löf's intuitionistic type theory.
Many proof assistants are based on type theory. For example, the underlying formal language of Rocq (formerly Coq) is the calculus of inductive constructions, while Lean is based on dependent type theory.
History
Type theory was created to avoid paradoxes in naive set theory and formal logic, such as Russell's paradox which demonstrates that, without proper axioms, it is possible to define the set of all sets that are not members of themselves; this set both contains itself and does not contain itself. Between 1902 and 1908, Bertrand Russell proposed various solutions to this problem.
By 1908, Russell arrived at a ramified theory of types together with an axiom of reducibility, both of which appeared in Whitehead and Russell's Principia Mathematica published in 1910, 1912, and 1913. This system avoided contradictions suggested in Russell's paradox by creating a hierarchy of types and then assigning each concrete mathematical entity to a specific type. Entities of a given type were built exclusively of subtypes of that type, thus preventing an entity from being defined using itself. This resolution of Russell's paradox is similar to approaches taken in other formal systems, such as Zermelo-Fraenkel set theory.Stanford Encyclopedia of Philosophy (rev. Mon Oct 12, 2020) Russell’s Paradox 3. Early Responses to the Paradox
Type theory is particularly popular in conjunction with Alonzo Church's lambda calculus. One notable early example of type theory is Church's simply typed lambda calculus. Church's theory of types helped the formal system avoid the Kleene–Rosser paradox that afflicted the original untyped lambda calculus. Church demonstrated that it could serve as a foundation of mathematics and it was referred to as a higher-order logic.
In the modern literature, "type theory" refers to a typed system based around lambda calculus. One influential system is Per Martin-Löf's intuitionistic type theory, which was proposed as a foundation for constructive mathematics. Another is Thierry Coquand's calculus of constructions, which is used as the foundation by Rocq (previously known as Coq), Lean, and other computer proof assistants. Type theory is an active area of research, one direction being the development of homotopy type theory.
Applications Mathematical foundations The first computer proof assistant, called Automath, used type theory to encode mathematics on a computer. Martin-Löf specifically developed intuitionistic type theory to encode all mathematics to serve as a new foundation for mathematics. There is ongoing research into mathematical foundations using homotopy type theory.
Mathematicians working in category theory already had difficulty working with the widely accepted foundation of Zermelo–Fraenkel set theory. This led to proposals such as Lawvere's Elementary Theory of the Category of Sets (ETCS). Homotopy type theory continues in this line using type theory. Researchers are exploring connections between dependent types (especially the identity type) and algebraic topology (specifically homotopy).
Proof assistants
Much of the current research into type theory is driven by proof checkers, interactive proof assistants, and automated theorem provers. Most of these systems use a type theory as the mathematical foundation for encoding proofs, which is not surprising, given the close connection between type theory and programming languages: LF is used by Twelf, often to define other type theories; many type theories which fall under higher-order logic are used by the HOL family of provers and PVS; computational type theory is used by NuPRL; calculus of constructions and its derivatives are used by Rocq (previously known as Coq), Matita, and Lean; UTT (Luo's Unified Theory of dependent Types) is used by Agda which is both a programming language and proof assistant
Many type theories are supported by LEGO and Isabelle. Isabelle also supports foundations besides type theories, such as ZFC. Mizar is an example of a proof system that only supports set theory.
Programming languages Any static program analysis, such as the type checking algorithms in the semantic analysis phase of compiler, has a connection to type theory. A prime example is Agda, a programming language which uses UTT (Luo's Unified Theory of dependent Types) for its type system.
The programming language ML was developed for manipulating type theories (see Logic for Computable Functions) and its own type system was heavily influenced by them.
Linguistics Type theory is also widely used in formal theories of semantics of natural languages, especially Montague grammarCooper, Robin. "Type theory and semantics in flux" . Handbook of the Philosophy of Science 14 (2012): 271-323. and its descendants. In particular, categorial grammars and pregroup grammars extensively use type constructors to define the types (noun, verb, etc.) of words.
The most common construction takes the basic types and for individuals and truth-values, respectively, and defines the set of types recursively as follows: if and are types, then so is ; nothing except the basic types, and what can be constructed from them by means of the previous clause are types.
A complex type is the type of functions from entities of type to entities of type . Thus one has types like that are interpreted as elements of the set of functions from entities to truth-values, i.e. indicator functions of sets of entities. An expression of type is a function from sets of entities to truth-values, i.e. a (indicator function of a) set of sets. This latter type is standardly taken to be the type of natural language quantifiers, like everybody or nobody (Montague 1973, Barwise and Cooper 1981).Barwise, Jon; Cooper, Robin (1981) Generalized quantifiers and natural language Linguistics and Philosophy 4 (2):159--219 (1981)
Type theory with records is a formal semantics representation framework, using records to express type theory types. It has been used in natural language processing, principally computational semantics and dialogue systems.Cooper, Robin (2010). Type theory and semantics in flux. Handbook of the Philosophy of Science. Volume 14: Philosophy of Linguistics. Elsevier.
Social sciences Gregory Bateson introduced a theory of logical types into the social sciences; his notions of double bind and logical levels are based on Russell's theory of types.
Logic A type theory is a mathematical logic, which is to say it is a collection of rules of inference that result in judgments. Most logics have judgments asserting "The proposition is true", or "The formula is a well-formed formula". A type theory has judgments that define types and assign them to a collection of formal objects, known as terms. A term and its type are often written together as .
Terms A term in logic is recursively defined as a constant symbol, variable, or a function application, where a term is applied to another term. Constant symbols could include the natural number , the Boolean value , and functions such as the successor function and conditional operator . Thus some terms could be , , , and .
Judgments Most type theories have 4 judgments: " is a type" " is a term of type " "Type is equal to type " "Terms and both of type are equal"
Judgments may follow from assumptions. For example, one might say "assuming is a term of type and is a term of type , it follows that is a term of type ". Such judgments are formally written with the turnstile symbol .
If there are no assumptions, there will be nothing to the left of the turnstile.
The list of assumptions on the left is the context of the judgment. Capital greek letters, such as and , are common choices to represent some or all of the assumptions. The 4 different judgments are thus usually written as follows.
Formal notation for judgments Description Type is a type (under assumptions ). is a term of type (under assumptions ).Type is equal to type (under assumptions ).Terms and are both of type and are equal (under assumptions ).
Some textbooks use a triple equal sign to stress that this is judgmental equality and thus an extrinsic notion of equality. The judgments enforce that every term has a type. The type will restrict which rules can be applied to a term.
Rules of inference A type theory's inference rules say what judgments can be made, based on the existence of other judgments. Rules are expressed as a Gentzen-style deduction using a horizontal line, with the required input judgments above the line and the resulting judgment below the line. For example, the following inference rule states a substitution rule for judgmental equality.The rules are syntactic and work by rewriting. The metavariables , , , , and may actually consist of complex terms and types that contain many function applications, not just single symbols.
To generate a particular judgment in type theory, there must be a rule to generate it, as well as rules to generate all of that rule's required inputs, and so on. The applied rules form a proof tree, where the top-most rules need no assumptions. One example of a rule that does not require any inputs is one that states the type of a constant term. For example, to assert that there is a term of type , one would write the following.
Type inhabitation
Generally, the desired conclusion of a proof in type theory is one of type inhabitation. The decision problem of type inhabitation (abbreviated by ) is: Given a context and a type , decide whether there exists a term that can be assigned the type in the type environment . Girard's paradox shows that type inhabitation is strongly related to the consistency of a type system with Curry–Howard correspondence. To be sound, such a system must have uninhabited types.
A type theory usually has several rules, including ones to: create a judgment (known as a context in this case) add an assumption to the context (context weakening) rearrange the assumptions use an assumption to create a variable define reflexivity, symmetry and transitivity for judgmental equality define substitution for application of lambda terms list all the interactions of equality, such as substitution define a hierarchy of type universes assert the existence of new types
Also, for each "by rule" type, there are 4 different kinds of rules: "type formation" rules say how to create the type "term introduction" rules define the canonical terms and constructor functions, like "pair" and "S". "term elimination" rules define the other functions like "first", "second", and "R". "computation" rules specify how computation is performed with the type-specific functions.
For examples of rules, an interested reader may follow Appendix A.2 of the Homotopy Type Theory book, or read Martin-Löf's Intuitionistic Type Theory.
Connections to foundations The logical framework of a type theory bears a resemblance to intuitionistic, or constructive, logic. Formally, type theory is often cited as an implementation of the Brouwer–Heyting–Kolmogorov interpretation of intuitionistic logic. Additionally, connections can be made to category theory and computer programs.
Intuitionistic logic