Inmathematics andtheoretical computer science, atype theory is theformal presentation of a specifictype system.[a] Type theory is the academic study of type systems.
Some type theories serve as alternatives toset theory as afoundation of mathematics. Two influential type theories that have been proposed as foundations are:
Mostcomputerized proof-writing systems use a type theory fortheir foundation. A common one isThierry Coquand'sCalculus of Inductive Constructions.
Type theory was created to avoidparadoxes innaive set theory andformal logic[b], such asRussell'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 aramified theory of types together with anaxiom of reducibility, both of which appeared inWhitehead andRussell'sPrincipia 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 ofsubtypes of that type,[c] 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 asZermelo-Fraenkel set theory.[4]
Type theory is particularly popular in conjunction withAlonzo Church'slambda calculus. One notable early example of type theory is Church'ssimply typed lambda calculus. Church's theory of types[5] helped the formal system avoid theKleene–Rosser paradox that afflicted the original untyped lambda calculus. Church demonstrated[d] that it could serve as afoundation of mathematics and it was referred to as ahigher-order logic.
In the modern literature, "type theory" refers to a typed system based around lambda calculus. One influential system isPer Martin-Löf'sintuitionistic type theory, which was proposed as a foundation forconstructive mathematics. Another isThierry Coquand'scalculus of constructions, which is used as the foundation byRocq (previously known asCoq),Lean, and other computerproof assistants. Type theory is an active area of research, one direction being the development ofhomotopy type theory.
The first computer proof assistant, calledAutomath, used type theory to encode mathematics on a computer. Martin-Löf specifically developedintuitionistic type theory to encodeall mathematics to serve as a new foundation for mathematics. There is ongoing research into mathematical foundations usinghomotopy type theory.
Mathematicians working incategory theory already had difficulty working with the widely accepted foundation ofZermelo–Fraenkel set theory. This led to proposals such as Lawvere'sElementary Theory of the Category of Sets (ETCS).[7] Homotopy type theory continues in this line using type theory. Researchers are exploring connections between dependent types (especially the identity type) andalgebraic topology (specificallyhomotopy).
Much of the current research into type theory is driven byproof checkers, interactiveproof assistants, andautomated 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:
Many type theories are supported byLEGO andIsabelle. Isabelle also supports foundations besides type theories, such asZFC.Mizar is an example of a proof system that only supports set theory.
Anystatic program analysis, such as the type checking algorithms in thesemantic analysis phase ofcompiler, has a connection to type theory. A prime example isAgda, a programming language which uses UTT (Luo's Unified Theory of dependent Types) for its type system.
The programming languageML was developed for manipulating type theories (seeLCF) and its own type system was heavily influenced by them.
Type theory is also widely used informal theories of semantics ofnatural languages,[8][9] especiallyMontague grammar[10] and its descendants. In particular,categorial grammars andpregroup 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 andtruth-values, respectively, and defines the set of types recursively as follows:
A complex type is the type offunctions from entities of type to entities of type. Thus one has types like which 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 ofnatural language quantifiers, like everybody ornobody (Montague 1973,Barwise and Cooper 1981).[11]
Type theory with records is aformal semantics representation framework, usingrecords to expresstype theory types. It has been used innatural language processing, principallycomputational semantics anddialogue systems.[12][13]
Gregory Bateson introduced a theory of logical types into the social sciences; his notions ofdouble bind and logical levels are based on Russell's theory of types.
A type theory is amathematical logic, which is to say it is a collection ofrules of inference that result injudgments. Most logics have judgments asserting "Theproposition is true", or "Theformula is awell-formed formula".[14] 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.
Aterm in logic isrecursively defined as aconstant symbol,variable, or afunction application, where a term is applied to another term. Constant symbols could include the natural number, the Boolean value, and functions such as thesuccessor function andconditional operator. Thus some terms could be,,, and.
Most type theories have 4 judgments:
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 theturnstile symbol.
If there are no assumptions, there will be nothing to the left of the turnstile.
The list of assumptions on the left is thecontext 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 isjudgmental equality and thus anextrinsic notion of equality.[15] The judgments enforce that every term has a type. The type will restrict which rules can be applied to a term.
A type theory'sinference rules say what judgments can be made, based on the existence of other judgments. Rules are expressed as aGentzen-stylededuction using a horizontal line, with the required input judgments above the line and the resulting judgment below the line.[16] For example, the following inference rule states asubstitution rule for judgmental equality.The rules are syntactic and work byrewriting. Themetavariables,,,, 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 aproof 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.
Generally, the desired conclusion of a proof in type theory is one oftype inhabitation.[17] The decision problem of type inhabitation (abbreviated by) is:
Girard's paradox shows that type inhabitation is strongly related to theconsistency 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:
Also, for each "by rule" type, there are 4 different kinds of rules
For examples of rules, an interested reader may follow Appendix A.2 of theHomotopy Type Theory book,[15] or read Martin-Löf's Intuitionistic Type Theory.[18]
The logical framework of a type theory bears a resemblance tointuitionistic, or constructive, logic. Formally, type theory is often cited as an implementation of theBrouwer–Heyting–Kolmogorov interpretation of intuitionistic logic.[18] Additionally, connections can be made tocategory theory andcomputer programs.
When used as a foundation, certain types are interpreted to bepropositions (statements that can be proven), and terms inhabiting the type are interpreted to be proofs of that proposition. When some types are interpreted as propositions, there is a set of common types that can be used to connect them to make aBoolean algebra out of types. However, the logic is notclassical logic butintuitionistic logic, which is to say it does not have thelaw of excluded middle nordouble negation.
Under this intuitionistic interpretation, there are common types that act as the logical operators:
| Logic Name | Logic Notation | Type Notation | Type Name |
|---|---|---|---|
| True | Unit Type | ||
| False | Empty Type | ||
| Implication | Function | ||
| Not | Function to Empty Type | ||
| And | Product Type | ||
| Or | Sum Type | ||
| For All | Dependent Product | ||
| Exists | Dependent Sum |
Because the law of excluded middle does not hold, there is no term of type. Likewise, double negation does not hold, so there is no term of type.
It is possible to include the law of excluded middle and double negation into a type theory, by rule or assumption. However, terms may not compute down to canonical terms and it will interfere with the ability to determine if two terms are judgementally equal to each other.[citation needed]
Per Martin-Löf proposed his intuitionistic type theory as a foundation forconstructive mathematics.[14] Constructive mathematics requires when proving "there exists an with property", one must construct a particular and a proof that it has property. In type theory, existence is accomplished using the dependent product type, and its proof requires a term of that type.
An example of a non-constructive proof isproof by contradiction. The first step is assuming that does not exist and refuting it by contradiction. The conclusion from that step is "it is not the case that does not exist". The last step is, by double negation, concluding that exists. Constructive mathematics does not allow the last step of removing the double negation to conclude that exists.[19]
Most of the type theories proposed as foundations are constructive, and this includes most of the ones used by proof assistants.[citation needed] It is possible to add non-constructive features to a type theory, by rule or assumption. These include operators on continuations such ascall with current continuation. However, these operators tend to break desirable properties such ascanonicity andparametricity.
TheCurry–Howard correspondence is the observed similarity between logics and programming languages. The implication in logic, "A B" resembles a function from type "A" to type "B". For a variety of logics, the rules are similar to expressions in a programming language's types. The similarity goes farther, as applications of the rules resemble programs in the programming languages. Thus, the correspondence is often summarized as "proofs as programs".
The opposition of terms and types can also be viewed as one ofimplementation andspecification. Byprogram synthesis, (the computational counterpart of) type inhabitation can be used to construct (all or parts of) programs from the specification given in the form of type information.[20]
Many programs that work with type theory (e.g., interactive theorem provers) also do type inferencing. It lets them select the rules that the user intends, with fewer actions by the user.
Although the initial motivation forcategory theory was far removed from foundationalism, the two fields turned out to have deep connections. AsJohn Lane Bell writes: "In fact categories canthemselves be viewed as type theories of a certain kind; this fact alone indicates that type theory is much more closely related to category theory than it is to set theory." In brief, a category can be viewed as a type theory by regarding its objects as types (orsorts[21]), i.e. "Roughly speaking, a category may be thought of as a type theory shorn of its syntax." A number of significant results follow in this way:[22]
The interplay, known ascategorical logic, has been a subject of active research since then; see the monograph of Jacobs (1999) for instance.
Homotopy type theory attempts to combine type theory and category theory. It focuses on equalities, especially equalities between types.Homotopy type theory differs fromintuitionistic type theory mostly by its handling of the equality type. In 2016,cubical type theory was proposed, which is a homotopy type theory with normalization.[23][24]
The most basic types are called atoms, and a term whose type is an atom is known as an atomic term. Common atomic terms included in type theories arenatural numbers, often notated with the type,Boolean logic values (/), notated with the type, andformal variables, whose type may vary.[17] For example, the following may be atomic terms.
In addition to atomic terms, most modern type theories also allow forfunctions. Function types introduce an arrow symbol, and aredefined inductively: If and are types, then the notation is the type of a function which takes aparameter of type and returns a term of type. Types of this form are known assimple types.[17]
Some terms may be declared directly as having a simple type, such as the following term,, which takes in two natural numbers in sequence and returns one natural number.
Strictly speaking, a simple type only allows for one input and one output, so a more faithful reading of the above type is that is a function which takes in a natural number and returns a function of the form. The parentheses clarify that does not have the type, which would be a function which takes in a function of natural numbers and returns a natural number. The convention is that the arrow isright associative, so the parentheses may be dropped from's type.[17]
New function terms may be constructed usinglambda expressions, and are called lambda terms. These terms are also defined inductively: a lambda term has the form, where is a formal variable and is a term, and its type is notated, where is the type of, and is the type of.[17] The following lambda term represents a function which doubles an input natural number.
The variable is and (implicit from the lambda term's type) must have type. The term has type, which is seen by applying the function application inference rule twice. Thus, the lambda term has type, which means it is a function taking a natural number as anargument and returning a natural number.
A lambda term is often referred to[e] as ananonymous function because it lacks a name. The concept of anonymous functions appears in many programming languages.
The power of type theories is in specifying how terms may be combined by way ofinference rules.[5] Type theories which have functions also have the inference rule offunction application: if is a term of type, and is a term of type, then the application of to, often written, has type. For example, if one knows the type notations,, and, then the following type notations can bededuced from function application.[17]
Parentheses indicate theorder of operations; however, by convention, function application isleft associative, so parentheses can be dropped where appropriate.[17] In the case of the three examples above, all parentheses could be omitted from the first two, and the third may simplified to.
Type theories that allow for lambda terms also include inference rules known as-reduction and-reduction. They generalize the notion of function application to lambda terms. Symbolically, they are written
The first reduction describes how to evaluate a lambda term: if a lambda expression is applied to a term, one replaces every occurrence of in with. The second reduction makes explicit the relationship between lambda expressions and function types: if is a lambda term, then it must be that is a function term because it is being applied to. Therefore, the lambda expression is equivalent to just, as both take in one argument and apply to it.[5]
For example, the following term may be-reduced.
In type theories that also establish notions ofequality for types and terms, there are corresponding inference rules of-equality and-equality.[17]
Theempty type has no terms. The type is usually written or. One use for the empty type is proofs oftype inhabitation. If for a type, it is consistent to derive a function of type, then isuninhabited, which is to say it has no terms.
Theunit type has exactly 1 canonical term. The type is written or and the single canonical term is written. The unit type is also used in proofs of type inhabitation. If for a type, it is consistent to derive a function of type, then isinhabited, which is to say it must have one or more terms.
The Boolean type has exactly 2 canonical terms. The type is usually written or or. The canonical terms are usually and.
Natural numbers are usually implemented in the style ofPeano Arithmetic. There is a canonical term for zero. Canonical values larger than zero use iterated applications of asuccessor function.
Some type theories allow for types of complex terms, such as functions or lists, to depend on the types of its arguments; these are calledtype constructors. For example, a type theory could have the dependent type, which should correspond tolists of terms, where each term must have type. In this case, has the kind, where denotes theuniverse of all types in the theory.
The product type,, depends on two types, and its terms are commonly written asordered pairs. The pair has the product type, where is the type of and is the type of. Each product type is then usually defined with eliminator functions and.
Besides ordered pairs, this type is used for the concepts oflogical conjunction andintersection.
The sum type is written as either or. In programming languages, sum types may be referred to astagged unions. Each type is usually defined withconstructors and, which areinjective, and an eliminator function such that
The sum type is used for the concepts oflogical disjunction andunion.
Some theories also allow terms to have their definitions depend on types. For instance, an identity function of any type could be written as. The function is said to be polymorphic in, or generic in.
As another example, consider a function, which takes in a and a term of type, and returns the list with the element at the end. The type annotation of such a function would be, which can be read as "for any type, pass in a and an, and return a". Here is polymorphic in.
With polymorphism, the eliminator functions can be defined generically forall product types as and.
Likewise, the sum type constructors can be defined for all valid types of sum members as and, which areinjective, and the eliminator function can be given as such that
Some theories also permit types to be dependent on terms instead of types. For example, a theory could have the type, where is a term of type encoding the length of thevector. This allows for greater specificity andtype safety: functions with vector length restrictions or length matching requirements, such as thedot product, can encode this requirement as part of the type.[26]
There are foundational issues that can arise from dependent types if a theory is not careful about what dependencies are allowed, such asGirard's Paradox. The logicianHenk Barendegt introduced thelambda cube as a framework for studying various restrictions and levels of dependent typing.[27]
Two commontype dependencies, dependent product and dependent sum types, allow for the theory to encodeBHK intuitionistic logic by acting as equivalents touniversal and existential quantification; this is formalized byCurry–Howard Correspondence.[26] As they also connect toproducts andsums inset theory, they are often written with the symbols and, respectively.
Sum types are seen independent pairs, where the second type depends on the value of the first term. This arises naturally in computer science where functions may return different types of outputs based on the input. For example, the Boolean type is usually defined with an eliminator function, which takes three arguments and behaves as follows.
Ordinary definitions of require and to have the same type. If the type theory allows for dependent types, then it is possible to define a dependent type such that
The type of may then be written as.
Following the notion of Curry-Howard Correspondence, theidentity type is a type introduced to mirrorpropositional equivalence, as opposed to thejudgmental (syntactic) equivalence that type theory already provides.
An identity type requires two terms of the same type and is written with the symbol. For example, if and are terms, then is a possible type. Canonical terms are created with a reflexivity function,. For a term, the call returns the canonical term inhabiting the type.
The complexities of equality in type theory make it an active research topic;homotopy type theory is a notable area of research that mainly deals with equality in type theory.
Inductive types are a general template for creating a large variety of types. In fact, all the types described above and more can be defined using the rules of inductive types. Two methods of generating inductive types areinduction-recursion andinduction-induction. A method that only uses lambda terms isScott encoding.
Someproof assistants, such asRocq (previously known asCoq) andLean, are based on the calculus for inductive constructions, which is acalculus of constructions with inductive types.
The most commonly acceptedfoundation for mathematics isfirst-order logic with thelanguage andaxioms ofZermelo–Fraenkel set theory with theaxiom of choice, abbreviated ZFC. Type theories having sufficientexpressibility may also act as a foundation of mathematics. There are a number of differences between these two approaches.
Proponents of type theory will also point out its connection to constructive mathematics through theBHK interpretation, its connection to logic by theCurry–Howard isomorphism, and its connections toCategory theory.
Terms usually belong to a single type. However, there are set theories that define "subtyping".
Computation takes place by repeated application of rules. Many types of theories arestrongly normalizing, which means that any order of applying the rules will always end in the same result. However, some are not. In a normalizing type theory, the one-directional computation rules are called "reduction rules", and applying the rules "reduces" the term. If a rule is not one-directional, it is called a "conversion rule".
Some combinations of types are equivalent to other combinations of types. When functions are considered "exponentiation", the combinations of types can be written similarly to algebraic identities.[28] Thus,,,,,.
Most type theories do not haveaxioms. This is because a type theory is defined by its rules of inference. This is a source of confusion for people familiar with Set Theory, where a theory is defined by both the rules of inference for a logic (such asfirst-order logic) and axioms about sets.
Sometimes, a type theory will add a few axioms. An axiom is a judgment that is accepted without a derivation using the rules of inference. They are often added to ensure properties that cannot be added cleanly through the rules.
Axioms can cause problems if they introduce terms without a way to compute on those terms. That is, axioms can interfere with thenormalizing property of the type theory.[29]
Some commonly encountered axioms are:
TheAxiom of Choice does not need to be added to type theory, because in most type theories it can be derived from the rules of inference. This is because of theconstructive nature of type theory, where proving that a value exists requires a method to compute the value. The Axiom of Choice is less powerful in type theory than most set theories, because type theory's functions must be computable and, being syntax-driven, the number of terms in a type must be countable. (SeeAxiom of choice § In constructive mathematics.)
(x,y) -> x^5+y, as an anonymous function.[25]{{cite journal}}: CS1 maint: DOI inactive as of July 2025 (link)| General | |||||||||
|---|---|---|---|---|---|---|---|---|---|
| Theorems (list) and paradoxes | |||||||||
| Logics |
| ||||||||
| Set theory |
| ||||||||
| Formal systems (list), language and syntax |
| ||||||||
| Proof theory | |||||||||
| Model theory | |||||||||
| Computability theory | |||||||||
| Related | |||||||||
