View source for Type theory

{{short description|Concept in mathematical logic}}
{{redirect|Theory of types|an architectural term|Form (architecture)#Theories}}
In [[mathematics]] and [[computer science|theoretical computer science]], a '''type theory''' is the [[formal system|formal presentation]] of a specific [[type system]].{{efn|name=basics|1= See {{section link||Terms and types}}   }} Type theory is the academic study of type systems. 

Some type theories serve as alternatives to [[set theory]] as a [[Foundations of mathematics|foundation of mathematics]]. Two influential type theories that have been proposed as foundations are: 

* [[typed lambda calculus|Typed λ-calculus]] of [[Alonzo Church]]
* [[Intuitionistic type theory]] of [[Per Martin-Löf]]

Most [[proof assistant|computerized proof-writing systems]] use a type theory for [[Curry–Howard correspondence|their foundation]]. A common one is [[Thierry Coquand]]'s [[Calculus of constructions|Calculus of Inductive Constructions]].

==History==
{{Main|History of type theory}}
Type theory was created to avoid a [[paradox]] in a mathematical equation{{efn|name= kleeneRosser |1= The [[Kleene–Rosser paradox]] "The Inconsistency of Certain Formal Logics" on page 636 ''Annals of Mathematics'' '''36''' number 3  (July 1935), showed that <math> 1=2 </math>.<ref name= KleeneRosser> {{Cite journal |first1=S. C. |last1=Kleene |name-list-style=amp |first2=J. B. |last2=Rosser |title=The inconsistency of certain formal logics |journal=[[Annals of Mathematics]] |volume=36 |issue=3 |pages=630–636 |year=1935 |doi=10.2307/1968646 |jstor=1968646 }}</ref>}} based on [[naive set theory]] and [[formal logic]]. [[Russell's paradox]] (first described in [[Gottlob Frege]]'s [[The Foundations of Arithmetic]]) is 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 [[History_of_type_theory#The_1908_"ramified"_theory_of_types|ramified theory of types]] together with an [[axiom of reducibility]], both of which appeared in [[Alfred North Whitehead|Whitehead]] and [[Bertrand Russell|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 [[subtyping|subtype]]s of that type,{{efn|name=JuliaSample|1= In [[Julia (programming language)|Julia]]'s type system, for example, abstract types have no instances, but can have subtype,<ref name=juliaSample >Balbaert, Ivo (2015) ''Getting Started With Julia Programming'' ISBN 978-1-78328-479-5</ref>{{rp|110}} whereas concrete types do not have subtypes but can have instances, for "[[Julia (programming language)#Language features|documentation, optimization, and dispatch]]".<ref name=juliaTypes >docs.julialang.org [https://docs.julialang.org/en/v1/manual/types/ v.1 Types] {{Webarchive|url=https://web.archive.org/web/20220324054245/https://docs.julialang.org/en/v1/manual/types/|date=2022-03-24}}</ref>}} 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|Zermelo-Fraenkel set theory]].<ref name="sepErp">''Stanford Encyclopedia of Philosophy'' [https://plato.stanford.edu/entries/russell-paradox/#ERP (rev. Mon Oct 12, 2020) Russell’s Paradox] {{Webarchive|url=https://web.archive.org/web/20211218023900/https://plato.stanford.edu/entries/russell-paradox/#ERP|date=December 18, 2021}} 3. Early Responses to the Paradox</ref>

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<ref name="church">{{cite journal|author-link=Alonzo Church|first=Alonzo|last=Church|title=A formulation of the simple theory of types|journal=The Journal of Symbolic Logic|volume=5|issue=2|pages=56–68|year=1940|doi=10.2307/2266170|jstor=2266170|s2cid=15889861}}</ref> helped the formal system avoid the [[Kleene–Rosser paradox]] that afflicted the original untyped lambda calculus. Church demonstrated{{efn|name=logisticMethod|1= Church demonstrated his ''logistic method'' with his simple theory of types,<ref name=church/> and explained his method in 1956,<ref name=intro>Alonzo Church (1956) [https://archive.org/details/dli.ernet.449121/page/85/mode/2up?q=logistic Introduction To Mathematical Logic Vol 1]</ref> pages 47-68.}} that it could serve as a [[Foundations of mathematics|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 [[Constructivism (mathematics)|constructive mathematics]]. Another is [[Thierry Coquand]]'s [[calculus of constructions]], which is used as the foundation by [[Coq (software)|Coq]], [[Lean (proof assistant)|Lean]], and other computer [[Proof assistant|proof assistants]]. Type theory is an active area of research, one direction being the development of [[homotopy type theory]].

==Applications==
{{Expand section|date=May 2008}}
===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).<ref>{{nlab|id=ETCS}}</ref> 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===
{{main|Proof assistant}}
Much of the current research into type theory is driven by [[Automated proof checking|proof checkers]], interactive [[proof assistant]]s, and [[Automated theorem proving|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:
* [[Logical framework|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 (proof assistant)|HOL family of provers]] and [[Prototype Verification System|PVS]];
* computational type theory is used by [[NuPRL]];
* [[calculus of constructions]] and its derivatives are used by [[Coq (software)|Coq]], [[Matita]], and [[Lean (proof assistant)|Lean]];
* UTT (Luo's Unified Theory of dependent Types) is used by [[Agda (programming language)|Agda]] which is both a programming language and proof assistant

Many type theories are supported by [[LEGO (proof assistant)|LEGO]] and [[Isabelle (proof assistant)|Isabelle]]. Isabelle also supports foundations besides type theories, such as [[Zermelo–Fraenkel set theory|ZFC]]. [[Mizar system|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 (compilers)|semantic analysis]] phase of [[compiler]], has a connection to type theory. A prime example is [[Agda (programming language)|Agda]], a programming language which uses UTT (Luo's Unified Theory of dependent Types) for its type system.

The programming language [[ML (programming language)|ML]] was developed for manipulating type theories (see [[Logic for Computable Functions|LCF]]) and its own type system was heavily influenced by them.

===Linguistics===
Type theory is also widely used in [[formal semantics (linguistics)|formal theories of semantics]] of [[natural language]]s,<ref>{{Cite book|last1=Chatzikyriakidis|first1=Stergios|url=https://books.google.com/books?id=iEEUDgAAQBAJ|title=Modern Perspectives in Type-Theoretical Semantics|last2=Luo|first2=Zhaohui|date=2017-02-07|publisher=Springer|isbn=978-3-319-50422-3|language=en|access-date=2022-07-29|archive-date=2023-08-10|archive-url=https://web.archive.org/web/20230810074711/https://books.google.com/books?id=iEEUDgAAQBAJ|url-status=live}}</ref><ref>{{Cite book|last=Winter|first=Yoad|url=https://books.google.com/books?id=aDRWDwAAQBAJ&q=%22formal+semantics%22+%22type+theory%22|title=Elements of Formal Semantics: An Introduction to the Mathematical Theory of Meaning in Natural Language|date=2016-04-08|publisher=Edinburgh University Press|isbn=978-0-7486-7777-1|language=en|access-date=2022-07-29|archive-date=2023-08-10|archive-url=https://web.archive.org/web/20230810074717/https://books.google.com/books?id=aDRWDwAAQBAJ&q=%22formal+semantics%22+%22type+theory%22|url-status=live}}</ref> especially [[Montague grammar]]<ref>Cooper, Robin. "[http://lecomte.al.free.fr/ressources/PARIS8_LSL/ddl-final.pdf Type theory and semantics in flux] {{Webarchive|url=https://web.archive.org/web/20220510190635/http://lecomte.al.free.fr/ressources/PARIS8_LSL/ddl-final.pdf|date=2022-05-10}}." Handbook of the Philosophy of Science 14 (2012): 271-323.</ref> and its descendants. In particular, [[categorial grammar]]s and [[pregroup grammar]]s extensively use type constructors to define the types (''noun'', ''verb'', etc.) of words.

The most common construction takes the basic types <math>e</math> and <math>t</math> for individuals and [[truth-value]]s, respectively, and defines the set of types recursively as follows:
* if <math>a</math> and <math>b</math> are types, then so is <math>\langle a,b\rangle</math>;
* nothing except the basic types, and what can be constructed from them by means of the previous clause are types.

A complex type <math>\langle a,b\rangle</math> is the type of [[Function (mathematics)|functions]] from entities of type <math>a</math> to entities of type <math>b</math>. Thus one has types like <math>\langle e,t\rangle</math> which are interpreted as elements of the set of functions from entities to truth-values, i.e. [[indicator function]]s of sets of entities. An expression of type <math>\langle\langle e,t\rangle,t\rangle</math> 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 [[Generalized quantifier|natural language quantifiers]], like '' everybody'' or ''nobody'' ([[Richard Montague|Montague]] 1973, [[Jon Barwise|Barwise]] and Cooper 1981).<ref>Barwise, Jon; Cooper, Robin (1981) [https://philpapers.org/rec/BARGQA Generalized quantifiers and natural language] ''Linguistics and Philosophy'' '''4''' (2):159--219 (1981)</ref>

[[Type theory with records]] is a [[formal semantics (linguistics)|formal semantics]] representation framework, using ''[[Record_(computer_science)|records]]'' to express ''type theory types''. It has been used in [[natural language processing]], principally [[computational semantics]] and [[dialogue systems]].<ref>{{cite journal|last = Cooper| first = Robin| year = 2005| title = Records and Record Types in Semantic Theory| journal = Journal of Logic and Computation| volume = 15| issue = 2| pages = 99–112| doi = 10.1093/logcom/exi004}}</ref><ref>Cooper, Robin (2010). ''Type theory and semantics in flux''. ''Handbook of the Philosophy of Science. Volume 14: Philosophy of Linguistics''. Elsevier.</ref>

===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 [[Rule of inference|rules of inference]] that result in [[Judgment (mathematical logic)|judgment]]s. Most logics have judgments asserting "The [[proposition]] <math>\varphi</math> is true", or "The [[Propositional formula|formula]] <math>\varphi</math> is a [[well-formed formula]]".<ref name=":6">{{Cite journal |last=Martin-Löf |first=Per |date=1987-12-01 |title=Truth of a proposition, evidence of a judgement, validity of a proof |url=https://doi.org/10.1007/BF00484985 |journal=Synthese |language=en |volume=73 |issue=3 |pages=407–420 |doi=10.1007/BF00484985 |issn=1573-0964}}</ref> 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 <math>\mathrm{term}:\mathsf{type}</math>.

===Terms===
A [[Term (logic)|term in logic]] is [[Recursive definition|recursively defined]] as a [[Logical constant|constant symbol]], [[Variable (mathematics)|variable]], or a [[function application]], where a term is applied to another term. Constant symbols could include the natural number <math>0</math>, the Boolean value <math>\mathrm{true}</math>, and functions such as the [[successor function]] <math>\mathrm{S}</math> and [[conditional operator]] <math>\mathrm{if}</math>. Thus some terms could be <math>0</math>, <math>(\mathrm{S}\,0)</math>, <math>(\mathrm{S}\,(\mathrm{S}\,0))</math>, and <math>(\mathrm{if}\,\mathrm{true}\,0\,(\mathrm{S}\,0))</math>.

===Judgments===
Most type theories have 4 judgments:

* "<math>T</math> [[#Gamma,IsaType|is a type]]"
* "<math>t</math> [[#Gamma,IsaTerm|is a term]] of type <math>T</math>"
* "Type <math>T_1</math> [[#Gamma,IsEq|is equal to]] type <math>T_2</math>"
* "Terms <math>t_1</math> and <math>t_2</math> both of type <math>T</math> [[#Gamma,BothTsAreEq|are equal]]"

Judgments may follow from assumptions. For example, one might say "assuming <math>x</math> is a term of type <math>\mathsf{bool}</math> and <math>y</math> is a term of type <math>\mathsf{nat}</math>, it follows that <math>(\mathrm{if}\,x\,y\,y)</math> is a term of type <math>\mathsf{nat}</math>". Such judgments are formally written with the [[Turnstile (symbol)|turnstile symbol]] <math>\vdash</math>.

<math>x:\mathsf{bool},y:\mathsf{nat}\vdash(\textrm{if}\,x\,y\,y): \mathsf{nat}</math>

If there are no assumptions, there will be nothing to the left of the turnstile.

<math>\vdash \mathrm{S}:\mathsf{nat}\to\mathsf{nat}</math>

The list of assumptions on the left is the ''context'' of the judgment. Capital greek letters, such as [[Gamma|<math>\Gamma</math>]] and <math>\Delta</math>, are common choices to represent some or all of the assumptions. The 4 different judgments are thus usually written as follows.

{| class="wikitable"
! Formal notation for judgments !! Description
|- {{anchor|Gamma,IsaType}}
|<math>\Gamma \vdash T</math> Type||<math>T</math> is a type (under assumptions <math>\Gamma</math>).
|- {{anchor|Gamma,IsaTerm}}
|<math>\Gamma \vdash t : T</math>||<math>t</math> is a term of type <math>T</math> (under assumptions <math>\Gamma</math>).
|- {{anchor|Gamma,IsEq}}
|<math>\Gamma \vdash T_1 = T_2 </math>||Type <math>T_1</math> is equal to type <math>T_2</math> (under assumptions <math>\Gamma</math>).
|- {{anchor|Gamma,BothTsAreEq}}
|<math>\Gamma \vdash t_1 = t_2 : T </math>||Terms <math>t_1</math> and <math>t_2</math> are both of type <math>T</math> and are equal (under assumptions <math>\Gamma</math>).
|}

Some textbooks use a triple equal sign <math>\equiv</math> to stress that this is [[Judgment (mathematical logic)|judgmental equality]] and thus an [[Intrinsic and extrinsic properties|extrinsic]] notion of equality.<ref name=":5">{{Cite book |last=The Univalent Foundations Program |url=https://homotopytypetheory.org/book/ |title=Homotopy Type Theory: Univalent Foundations of Mathematics |publisher=Homotopy Type Theory |year=2013}}</ref> 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 [[Rule of inference|inference rules]] say what judgments can be made, based on the existence of other judgments. Rules are expressed as a [[Sequent calculus|Gentzen]]-style [[Formal system|deduction]] using a horizontal line, with the required input judgments above the line and the resulting judgment below the line.<ref>{{cite web |last1=Smith |first1=Peter |title=Types of proof system |url=https://www.logicmatters.net/resources/pdfs/ProofSystems.pdf |url-status=live |archive-url=https://ghostarchive.org/archive/20221009/https://www.logicmatters.net/resources/pdfs/ProofSystems.pdf |archive-date=2022-10-09 |access-date=29 December 2021 |website=logicmatters.net}}</ref> For example, the following inference rule states a [[Substitution (logic)|substitution]] rule for judgmental equality.<math display="block">
\begin{array}{c}
\Gamma\vdash t:T_1 \qquad \Delta\vdash T_1 = T_2 \\
\hline
\Gamma,\Delta\vdash t:T_2
\end{array}
</math>The rules are syntactic and work by [[rewriting]]. The [[Metavariable|metavariables]] <math>\Gamma</math>, <math>\Delta</math>, <math>t</math>, <math>T_1</math>, and <math>T_2</math> 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 [[Natural deduction#Proofs and type theory|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 <math>0</math> of type <math>\mathsf{nat}</math>, one would write the following.<math display="block">
\begin{array}{c}
\hline
\vdash 0 : nat \\
\end{array}
</math>

==== Type inhabitation ====
{{Main|Type inhabitation}}
Generally, the desired conclusion of a proof in type theory is one of [[type inhabitation]].<ref name=":1">{{cite book |author1=Henk Barendregt |url=https://books.google.com/books?id=2UVasvrhXl8C |title=Lambda Calculus with Types |author2=Wil Dekkers |author3=Richard Statman |date=20 June 2013 |publisher=Cambridge University Press |isbn=978-0-521-76614-2 |pages=1–66}}</ref> The decision problem of type inhabitation (abbreviated by <math>\exists t.\Gamma \vdash t : \tau?</math>) is: 
:Given a context <math>\Gamma</math> and a type <math>\tau</math>, decide whether there exists a term <math>t</math> that can be assigned the type <math>\tau</math> in the type environment <math>\Gamma</math>.
[[System U#Girard's paradox|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'')
* [[structural rule|rearrange the assumptions]]
* use an assumption to create a variable
* define [[Reflexive relation|reflexivity]], [[Symmetric relation|symmetry]] and [[Transitive relation|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,<ref name=":5" />  or read Martin-Löf's Intuitionistic Type Theory.<ref name=":3">{{Cite web|url=https://hott.github.io/HoTT-2019/images/mltt-rules.pdf|title=Rules to Martin-Löf's Intuitionistic Type Theory|access-date=2022-01-22|archive-date=2021-10-21|archive-url=https://web.archive.org/web/20211021231427/https://hott.github.io/HoTT-2019/images/mltt-rules.pdf|url-status=live}}</ref>

==Connections to foundations==
The logical framework of a type theory bears a resemblance to [[Intuitionistic logic|intuitionistic]], or constructive, logic. Formally, type theory is often cited as an implementation of the [[Brouwer–Heyting–Kolmogorov interpretation]] of intuitionistic logic.<ref name=":3" /> Additionally, connections can be made to [[category theory]] and [[Computer programming|computer programs]].

===Intuitionistic logic===
When used as a foundation, certain types are interpreted to be [[propositions]] (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 a [[Boolean algebra (structure)|Boolean algebra]] out of types. However, the logic is not [[classical logic]] but [[intuitionistic logic]], which is to say it does not have the [[law of excluded middle]] nor [[double negation]].

Under this intuitionistic interpretation, there are common types that act as the logical operators:
{|class="wikitable"
! Logic Name !! Logic Notation !! Type Notation !! Type Name
|-
|True||<math>\top</math>||<math>\top</math>||Unit Type
|-
|False||<math>\bot</math>||<math>\bot</math>||Empty Type
|-
|[[Material conditional|Implication]]||<math>A \to B</math>||<math>A \to B</math>||Function
|-
|[[Not (logic)|Not]]||<math>\neg A</math>||<math>A \to \bot</math>||Function to Empty Type
|-
|[[And (logic)|And]]||<math>A \land B</math>||<math>A \times B</math>||Product Type
|-
|[[Or (logic)|Or]]||<math>A \lor B</math>||<math>A + B</math>||Sum Type
|-
|[[Universal quantification|For All]]||<math>\forall a \in A, P(a)</math>||<math>\Pi a:A.P(a)</math>||Dependent Product
|-
|[[Existential quantification|Exists]]||<math>\exists a \in A, P(a)</math>||<math>\Sigma a: A.P(a)</math>||Dependent Sum
|}

Because the law of excluded middle does not hold, there is no term of type <math>\Pi a.A+ (A\to\bot)</math>. Likewise, double negation does not hold, so there is no term of type <math>\Pi A.((A\to\bot)\to\bot)\to A</math>.

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.{{Cn|date=January 2024}}

==== Constructive mathematics ====
Per Martin-Löf proposed his intuitionistic type theory as a foundation for [[constructive mathematics]].<ref name=":6" /> Constructive mathematics requires when proving "there exists an <math>x</math> with property <math>P(x)</math>", one must construct a particular <math>x</math> and a proof that it has property <math>P</math>. 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 is [[proof by contradiction]]. The first step is assuming that <math>x</math> does not exist and refuting it by contradiction. The conclusion from that step is "it is not the case that <math>x</math> does not exist". The last step is, by double negation, concluding that <math>x</math> exists. Constructive mathematics does not allow the last step of removing the double negation to conclude that <math>x</math> exists.<ref>{{cite web|title=proof by contradiction|url=https://ncatlab.org/nlab/show/proof+by+contradiction|website=nlab|access-date=29 December 2021|archive-date=13 August 2023|archive-url=https://web.archive.org/web/20230813170132/https://ncatlab.org/nlab/show/proof+by+contradiction|url-status=live}}</ref>

Most of the type theories proposed as foundations are constructive, and this includes most of the ones used by proof assistants.{{Cn|date=January 2024}} It is possible to add non-constructive features to a type theory, by rule or assumption. These include operators on continuations such as [[Call/cc#Relation to non-constructive logic|call with current continuation]]. However, these operators tend to break desirable properties such as [[canonicity (type theory)|canonicity]] and [[parametricity]].

===Curry-Howard correspondence===
The [[Curry–Howard correspondence]] is the observed similarity between logics and programming languages. The implication in logic, "A <math>\to</math> 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 of ''implementation'' and ''specification''. By [[program 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.<ref>
{{cite conference |last1=Heineman |first1=George T. |last2=Bessai |first2=Jan |last3=Düdder |first3=Boris |last4=Rehof |first4=Jakob |year=2016 |title=A long and winding road towards modular synthesis |conference=ISoLA 2016 |series=Lecture Notes in Computer Science |publisher=Springer |volume=9952 |pages=303–317 |doi=10.1007/978-3-319-47166-2_21 |isbn=978-3-319-47165-5 |book-title=Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques}}</ref>

====Type inference====
{{Main|Type inference}}

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.

===Research areas===

==== Category theory ====

Although the initial motivation for [[category theory]] was far removed from foundationalism, the two fields turned out to have deep connections. As [[John Lane Bell]] writes: "In fact categories can ''themselves'' 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 (or ''sorts'' <ref>{{Cite journal|last=Barendregt|first=Henk|date=1991|title=Introduction to generalized type systems|journal=[[Journal of Functional Programming]]|volume=1|issue=2|pages=125–154|doi=10.1017/s0956796800020025|issn=0956-7968|hdl=2066/17240|s2cid=44757552 |hdl-access=free}}</ref>), 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:<ref name="Sets and Extensions in the Twentieth Century">{{cite book|series=Handbook of the History of Logic|volume=6|title=Sets and Extensions in the Twentieth Century|year=2012|publisher=Elsevier|isbn=978-0-08-093066-4|first=John L.|last=Bell|chapter=Types, Sets and Categories|chapter-url=http://publish.uwo.ca/~jbell/types.pdf|editor-first=Akihiro|editor-last=Kanamory|access-date=2012-11-03|archive-date=2018-04-17|archive-url=https://web.archive.org/web/20180417105624/http://publish.uwo.ca/~jbell/types.pdf|url-status=live}}</ref>
* [[Cartesian closed category|cartesian closed categories]] correspond to the typed λ-calculus ([[Lambek]], 1970);
* [[C-monoid]]s (categories with products and exponentials and one non-terminal object) correspond to the untyped λ-calculus (observed independently by Lambek and [[Dana Scott]] around 1980);
* [[Locally cartesian closed category|locally cartesian closed categories]] correspond to [[Martin-Löf type theory|Martin-Löf type theories]] (Seely, 1984).

The interplay, known as [[categorical logic]], has been a subject of active research since then; see the monograph of Jacobs (1999) for instance.

==== Homotopy type theory ====
[[Homotopy type theory]] attempts to combine type theory and category theory. It focuses on equalities, especially equalities between types. [[Homotopy type theory]] differs from [[intuitionistic 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.<ref>{{Cite book |last1=Sterling |first1=Jonathan |title=2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |last2=Angiuli |first2=Carlo |date=2021-06-29 |publisher=IEEE |isbn=978-1-6654-4895-6 |location=Rome, Italy |pages=1–15 |chapter=Normalization for Cubical Type Theory |doi=10.1109/LICS52264.2021.9470719 |access-date=2022-06-21 |chapter-url=https://ieeexplore.ieee.org/document/9470719 |archive-url=https://web.archive.org/web/20230813170127/https://ieeexplore.ieee.org/document/9470719 |archive-date=2023-08-13 |url-status=live |arxiv=2101.11479 |s2cid=231719089}}</ref><ref name=":0" />

==Definitions==
=== Terms and types ===

==== Atomic terms ====
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 are [[natural number]]s, often notated with the type <math>\mathsf{nat}</math>, [[Boolean Logic|Boolean logic]] values (<math>\mathrm{true}</math>/<math>\mathrm{false}</math>), notated with the type <math>\mathsf{bool}</math>, and [[Variable (mathematics)|formal variables]], whose type may vary.<ref name=":1" /> For example, the following may be atomic terms.

* <math>42:\mathsf{nat}</math>
* <math>\mathrm{true}:\mathsf{bool}</math>
* <math>x:\mathsf{nat}</math>
* <math>y:\mathsf{bool}</math>

====Function terms====
In addition to atomic terms, most modern type theories also allow for [[Function (mathematics)|functions]]. Function types introduce an arrow symbol, and are [[Recursive definition|defined inductively]]: If <math>\sigma</math> and <math>\tau</math> are types, then the notation <math>\sigma\to\tau</math> is the type of a function which takes a [[parameter]] of type <math>\sigma</math> and returns a term of type <math>\tau</math>. Types of this form are known as [[Simply typed lambda calculus|''simple'' types]].<ref name=":1" />

Some terms may be declared directly as having a simple type, such as the following term, <math>\mathrm{add}</math>, which takes in two natural numbers in sequence and returns one natural number.

<math>\mathrm{add}:\mathsf{nat}\to (\mathsf{nat}\to\mathsf{nat})</math>

Strictly speaking, a simple type only allows for one input and one output, so a more faithful reading of the above type is that <math>\mathrm{add}</math> is a function which takes in a natural number and returns a function of the form <math>\mathsf{nat}\to\mathsf{nat}</math>. The parentheses clarify that <math>\mathrm{add}</math> does not have the type <math>(\mathsf{nat}\to \mathsf{nat})\to\mathsf{nat}</math>, which would be a function which takes in a function of natural numbers and returns a natural number. The convention is that the arrow is [[Operator associativity|right associative]], so the parentheses may be dropped from <math>\mathrm{add}</math>'s type.<ref name=":1" />

==== Lambda terms ====
New function terms may be constructed using [[Lambda calculus#Definition|lambda expression]]s, and are called lambda terms. These terms are also defined inductively: a lambda term has the form <math>(\lambda v .t)</math>, where <math>v</math> is a formal variable and <math>t</math> is a term, and its type is notated <math>\sigma\to\tau</math>, where <math>\sigma</math> is the type of <math>v</math>, and <math>\tau</math> is the type of <math>t</math>.<ref name=":1" /> The following lambda term represents a function which doubles an input natural number.

<math>(\lambda x.\mathrm{add}\,x\,x): \mathsf{nat}\to\mathsf{nat}</math>

The variable is <math>   x</math> and (implicit from the lambda term's type) must have type <math>    \mathsf{nat} </math>. The term <math>   \mathrm{add}\,x\,x</math> has type <math>    \mathsf{nat} </math>, which is seen by applying the function application inference rule twice. Thus, the lambda term has type <math>\mathsf{nat}\to\mathsf{nat}</math>, which means it is a function taking a natural number as an [[Argument of a function|argument]] and returning a natural number.

A lambda term is often referred to{{efn|name= anon|1= In [[Julia (programming language)|Julia]], for example, a function with no name, but with two parameters in some tuple (x,y) can be denoted by say, <code>(x,y) -> x^5+y</code>, as an anonymous function.<ref name=balbaert > Balbaert,Ivo [https://www.oreilly.com/library/view/getting-started-with/9781783284795/ch03s03.html (2015) Getting Started with Julia]</ref>}} as an [[anonymous function]] because it lacks a name. The concept of anonymous functions appears in many programming languages.

=== Inference Rules ===

==== Function application ====
The power of type theories is in specifying how terms may be combined by way of [[Rule of inference|inference rules]].<ref name="church" /> Type theories which have functions also have the inference rule of [[function application]]: if <math>t</math> is a term of type <math>\sigma\to\tau</math>, and <math>s</math> is a term of type <math>\sigma</math>, then the application of <math>t</math> to <math>s</math>, often written <math>(t\,s)</math>, has type <math>\tau</math>. For example, if one knows the type notations <math>0:\textsf{nat}</math>, <math>1:\textsf{nat}</math>, and <math>2:\textsf{nat}</math>, then the following type notations can be [[Deduction system|deduced]] from function application.<ref name=":1" />
* <math>  (\mathrm{add}\,1): \textsf{nat}\to\textsf{nat}</math>
* <math>   ((\mathrm{add}\,2)\,0): \textsf{nat}</math>
* <math>   ((\mathrm{add}\,1)((\mathrm{add}\,2)\,0)): \textsf{nat}</math>

Parentheses indicate the [[order of operations]]; however, by convention, function application is [[left associative]], so parentheses can be dropped where appropriate.<ref name=":1" /> In the case of the three examples above, all parentheses could be omitted from the first two, and the third may simplified to <math>   \mathrm{add}\,1\, (\mathrm{add}\,2\,0): \textsf{nat}</math>.

==== Reductions ====
Type theories that allow for lambda terms also include inference rules known as <math>\beta</math>-reduction and <math>\eta</math>-reduction. They generalize the notion of function application to lambda terms. Symbolically, they are written

* <math>(\lambda v. t)\,s\rightarrow t[v \colon= s]</math> (<math>\beta</math>-reduction).
* <math>(\lambda v. t\, v)\rightarrow t</math>, if <math>   v</math> is not a [[Free variables and bound variables|free variable]] in <math>t</math> (<math>\eta</math>-reduction).

The first reduction describes how to evaluate a lambda term: if a lambda expression <math>(\lambda v .t)</math> is applied to a term <math>s</math>, one replaces every occurrence of <math>v</math> in <math>t</math> with <math>s</math>. The second reduction makes explicit the relationship between lambda expressions and function types: if <math>(\lambda v. t\, v)</math> is a lambda term, then it must be that <math>t</math> is a function term because it is being applied to <math>v</math>. Therefore, the lambda expression is equivalent to just <math>t</math>, as both take in one argument and apply <math>t</math> to it.<ref name="church" />

For example, the following term may be <math>\beta</math>-reduced.

<math>(\lambda x.\mathrm{add}\,x\,x)\,2\rightarrow \mathrm{add}\,2\,2</math>

In type theories that also establish notions of [[Equality (mathematics)|equality]] for types and terms, there are corresponding inference rules of <math>\beta</math>-equality and <math>\eta</math>-equality.<ref name=":1" />

===Common terms and types===
====Empty type====
The [[empty type]] has no terms. The type is usually written <math>\bot</math> or <math>\mathbb 0</math>. One use for the empty type is proofs of [[type inhabitation]]. If for a type <math>a</math>, it is consistent to derive a function of type <math>a\to\bot</math>, then <math>a</math> is ''uninhabited'', which is to say it has no terms.

====Unit type====
The [[unit type]] has exactly 1 canonical term. The type is written <math>\top</math> or <math>\mathbb 1</math> and the single canonical term is written <math>\ast</math>. The unit type is also used in proofs of type inhabitation. If for a type <math>a</math>, it is consistent to derive a function of type <math>\top\to a</math>, then <math>a</math> is ''inhabited'', which is to say it must have one or more terms.

====Boolean type====
The Boolean type has exactly 2 canonical terms. The type is usually written <math>\textsf{bool}</math> or <math>\mathbb B</math> or <math>\mathbb 2</math>. The canonical terms are usually <math>\mathrm{true}</math> and <math>\mathrm{false}</math>.

====Natural numbers====
Natural numbers are usually implemented in the style of [[Peano arithmetic|Peano Arithmetic]]. There is a canonical term <math>0:\mathsf{nat}</math> for zero. Canonical values larger than zero use iterated applications of a [[successor function]] <math>\mathrm{S}:\mathsf{nat}\to\mathsf{nat}</math>.

=== Type constructors ===
Some type theories allow for types of complex terms, such as functions or lists, to depend on the types of its arguments; these are called [[Kind (type theory)|type constructors]]. For example, a type theory could have the dependent type <math>\mathsf{list}\,a</math>, which should correspond to [[List (abstract data type)|lists]] of terms, where each term must have type <math>a</math>. In this case, <math>\mathsf{list}</math> has the kind <math>U\to U</math>, where <math>U</math> denotes the [[Universe (mathematics)|universe]] of all types in the theory. 

====Product type====
The product type, <math>\times</math>, depends on two types, and its terms are commonly written as [[Ordered pair|ordered pairs]] <math>(s,t)</math>. The pair <math>(s,t)</math> has the product type <math>\sigma\times\tau</math>, where <math>\sigma</math> is the type of <math>s</math> and <math>\tau</math> is the type of <math>t</math>. Each product type is then usually defined with eliminator functions <math>\mathrm{first}:\sigma\times\tau\to\sigma</math> and <math>\mathrm{second}:\sigma\times\tau\to\tau</math>.

* <math>\mathrm{first}\,(s,t)</math> returns <math>s</math>, and
* <math>\mathrm{second}\,(s,t)</math> returns <math>t</math>.

Besides ordered pairs, this type is used for the concepts of [[logical conjunction]] and [[intersection]].

====Sum type====
The sum type is written as either <math>+</math> or <math>\sqcup</math>. In programming languages, sum types may be referred to as [[Tagged union|tagged unions]]. Each type <math>\sigma\sqcup\tau</math> is usually defined with [[Constructor (programming)|constructors]] <math>\mathrm{left}:\sigma\to(\sigma\sqcup\tau)</math> and <math>\mathrm{right}:\tau\to(\sigma\sqcup\tau)</math>, which are [[Injective function|injective]], and an eliminator function <math>\mathrm{match}:(\sigma\to\rho)\to(\tau\to\rho)\to(\sigma\sqcup\tau)\to\rho</math> such that

* <math>\mathrm{match}\,f\,g\,(\mathrm{left}\,x)</math> returns <math>f\,x</math>, and
* <math>\mathrm{match}\,f\,g\,(\mathrm{right}\,y)</math> returns <math>g\,y</math>.

The sum type is used for the concepts of [[logical or|logical disjunction]] and [[Union (set theory)|union]].

=== Polymorphic types ===
Some theories also allow terms to have their definitions depend on types. For instance, an identity function of any type could be written as <math>\lambda x.x:\forall\alpha. \alpha\to\alpha</math>. The function is said to be polymorphic in <math>\alpha</math>, or generic in <math>x</math>.

As another example, consider a function <math>\mathrm{append}</math>, which takes in a <math>\mathsf{list}\,a</math> and a term of type <math>a</math>, and returns the list with the element at the end. The type annotation of such a function would be <math>\mathrm{append}:\forall\,a.\mathsf{list}\,a\to a\to\mathsf{list}\,a</math>, which can be read as "for any type <math>a</math>, pass in a <math>\mathsf{list}\,a</math> and an <math>a</math>, and return a <math>\mathsf{list}\,a</math>". Here <math>\mathrm{append}</math> is polymorphic in <math>a</math>.

====Products and sums====
With polymorphism, the eliminator functions can be defined generically for ''all'' product types as <math>\mathrm{first}:\forall\,\sigma\,\tau.\sigma\times\tau\to\sigma</math> and <math>\mathrm{second}:\forall\,\sigma\,\tau.\sigma\times\tau\to\tau</math>.

* <math>\mathrm{first}\,(s,t)</math> returns <math>s</math>, and
* <math>\mathrm{second}\,(s,t)</math> returns <math>t</math>.

Likewise, the sum type constructors can be defined for all valid types of sum members as <math>\mathrm{left}:\forall\,\sigma\,\tau.\sigma\to(\sigma\sqcup\tau)</math> and <math>\mathrm{right}:\forall\,\sigma\,\tau.\tau\to(\sigma\sqcup\tau)</math>, which are [[Injective function|injective]], and the eliminator function can be given as <math>\mathrm{match}:\forall\,\sigma\,\tau\,\rho.(\sigma\to\rho)\to(\tau\to\rho)\to(\sigma\sqcup\tau)\to\rho</math> such that

* <math>\mathrm{match}\,f\,g\,(\mathrm{left}\,x)</math> returns <math>f\,x</math>, and
* <math>\mathrm{match}\,f\,g\,(\mathrm{right}\,y)</math> returns <math>g\,y</math>.

=== Dependent typing ===
Some theories also permit types to be dependent on terms instead of types. For example, a theory could have the type <math>\mathsf{vector}\,n</math>, where <math>n</math> is a term of type <math>\mathsf{nat}</math> encoding the length of the [[Vector space|vector]]. This allows for greater specificity and [[type safety]]: functions with vector length restrictions or length matching requirements, such as the [[dot product]], can encode this requirement as part of the type.<ref name=":2">{{Citation |last1=Bove |first1=Ana |title=Dependent Types at Work |date=2009 |url=https://doi.org/10.1007/978-3-642-03153-3_2 |work=Language Engineering and Rigorous Software Development: International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised Tutorial Lectures |pages=57–99 |editor-last=Bove |editor-first=Ana |access-date=2024-01-18 |series=Lecture Notes in Computer Science |place=Berlin, Heidelberg |publisher=Springer |language=en |doi=10.1007/978-3-642-03153-3_2 |isbn=978-3-642-03153-3 |last2=Dybjer |first2=Peter |editor2-last=Barbosa |editor2-first=Luís Soares |editor3-last=Pardo |editor3-first=Alberto |editor4-last=Pinto |editor4-first=Jorge Sousa}}</ref> 

There are foundational issues that can arise from dependent types if a theory is not careful about what dependencies are allowed, such as [[Girard's paradox|Girard's Paradox]]. The logician [[Henk Barendregt|Henk Barendegt]] introduced the [[lambda cube]] as a framework for studying various restrictions and levels of dependent typing.<ref>{{Cite journal |last=Barendegt |first=Henk |date=April 1991 |title=Introduction to generalized type systems |url=https://doi.org/10.1017/S0956796800020025 |journal=[[Journal of Functional Programming]] |volume=1 |issue=2 |pages=125–154 |doi=10.1017/S0956796800020025 |via=Cambridge Core|hdl=2066/17240 |hdl-access=free }}</ref>

==== Dependent products and sums ====
Two common [[Dependent type|type dependencies]], dependent product and dependent sum types, allow for the theory to encode [[BHK interpretation|BHK intuitionistic logic]] by acting as equivalents to [[Quantification (logic)|universal and existential quantification]]; this is formalized by [[Curry–Howard correspondence|Curry–Howard Correspondence]].<ref name=":2" /> As they also connect to [[Cartesian product|products]] and [[Disjoint union|sums]] in [[set theory]], they are often written with the symbols <math>\Pi</math> and <math>\Sigma</math>, respectively.

Sum types are seen in [[Dependent type|dependent 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 <math>\mathrm{if}</math>, which takes three arguments and behaves as follows.
* <math>\mathrm{if}\,\mathrm{true}\,x\,y</math> returns <math>x</math>, and
* <math>\mathrm{if}\,\mathrm{false}\,x\,y</math> returns <math>y</math>.
Ordinary definitions of <math>\mathrm{if}</math> require <math>x</math> and <math>y</math> to have the same type. If the type theory allows for dependent types, then it is possible to define a dependent type <math>x:\mathsf{bool}\,\vdash\,\mathrm{TF}\,x:U\to U\to U</math> such that

* <math>\mathrm{TF}\,\mathrm{true}\,\sigma\,\tau</math> returns <math>\sigma</math>, and
* <math>\mathrm{TF}\,\mathrm{false}\,\sigma\,\tau</math> returns <math>\tau</math>.

The type of <math>\mathrm{if}</math> may then be written as <math>\forall\,\sigma\,\tau.\Pi_{x:\mathsf{bool}}.\sigma\to\tau\to\mathrm{TF}\,x\,\sigma\,\tau</math>.

{{anchor|Equality types}}
====Identity type====
Following the notion of Curry-Howard Correspondence, the [[identity type]] is a type introduced to mirror [[Propositional logic|propositional equivalence]], as opposed to the [[Judgment (mathematical logic)|judgmental (syntactic) equivalence]] that type theory already provides.

An identity type requires two terms of the same type and is written with the symbol <math>=</math>. For example, if <math>x+1</math> and <math>1+x</math> are terms, then <math>x+1=1+x</math> is a possible type. Canonical terms are created with a reflexivity function, <math>\mathrm{refl}</math>. For a term <math>t</math>, the call <math>\mathrm{refl}\,t</math> returns the canonical term inhabiting the type <math>t=t</math>.

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====
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 are [[induction-recursion]] and [[induction-induction]]. A method that only uses lambda terms is [[Mogensen–Scott encoding|Scott encoding]].

Some [[Proof assistant|proof assistants]], such as [[Coq (software)|Coq]] and [[Lean (proof assistant)|Lean]], are based on the calculus for inductive constructions, which is a [[calculus of constructions]] with inductive types.

==Differences from set theory==
The most commonly accepted [[Foundations of mathematics|foundation for mathematics]] is [[first-order logic]] with the [[Formal language|language]] and [[Axiom|axioms]] of [[Zermelo–Fraenkel set theory]] with the [[axiom of choice]], abbreviated ZFC. Type theories having sufficient [[Expressive power (computer science)|expressibility]] may also act as a foundation of mathematics. There are a number of differences between these two approaches.

* Set theory has both [[Rule of inference|rules]] and [[axiom]]s, while type theories only have rules. Type theories, in general, do not have axioms and are defined by their rules of inference.<ref name=":5" />
* Classical set theory and logic have the [[law of excluded middle]]. When a type theory encodes the concepts of "and" and "or" as types, it leads to [[intuitionistic logic]], and does not necessarily have the law of excluded middle.<ref name=":3" />
* In set theory, an element is not restricted to one set. The element can appear in subsets and unions with other sets. In type theory, terms (generally) belong to only one type. Where a subset would be used, type theory can use a [[Predicate (mathematical logic)|predicate function]] or use a dependently-typed product type, where each element <math>x</math> is paired with a proof that the subset's property holds for <math>x</math>. Where a union would be used, type theory uses the sum type, which contains new canonical terms.
* Type theory has a built-in notion of computation. Thus, "1+1" and "2" are different terms in type theory, but they compute to the same value. Moreover, functions are defined computationally as lambda terms. In set theory, "1+1=2" means that "1+1" is just another way to refer the value "2". Type theory's computation does require a complicated concept of equality.
* Set theory [[Set-theoretic definition of natural numbers|encodes numbers as sets]]. Type theory can encode numbers as functions using [[Church encoding]], or more naturally as [[Intuitionistic type theory#Inductive types|inductive types]], and the construction closely resembles [[Peano axioms|Peano's axioms]].
* In type theory, proofs are types whereas in set theory, proofs are part of the underlying first-order logic.<ref name=":5" />

Proponents of type theory will also point out its connection to constructive mathematics through the [[BHK interpretation]], its connection to logic by the [[Curry–Howard isomorphism]], and its connections to [[Category theory]].

===Properties of type theories===
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 are [[strongly 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.<ref name=":4">{{cite web|last1=Milewski|first1=Bartosz|title=Programming with Math (Exploring Type Theory)|url=https://www.youtube.com/watch?v=8AGWTWVOJ74|website=YouTube|access-date=2022-01-22|archive-date=2022-01-22|archive-url=https://web.archive.org/web/20220122213434/https://www.youtube.com/watch?v=8AGWTWVOJ74|url-status=live}}</ref> Thus, <math>{\mathbb 0} + A \cong A</math>, <math>{\mathbb 1} \times A \cong A</math>, <math>{\mathbb 1} + {\mathbb 1} \cong {\mathbb 2}</math>, <math>A^{B+C} \cong A^B \times A^C</math>, <math>A^{B\times C} \cong (A^B)^C</math>.

===Axioms===
Most type theories do not have [[axiom]]s. 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 as [[first-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 the [[Normal form (abstract rewriting)|normalizing property]] of the type theory.<ref>{{cite web|title=Axioms and Computation|url=https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html|website=Theorem Proving in Lean|access-date=21 January 2022|archive-date=22 December 2021|archive-url=https://web.archive.org/web/20211222130219/https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html|url-status=live}}</ref>

Some commonly encountered axioms are:
* "Axiom K" ensures "uniqueness of identity proofs". That is, that every term of an identity type is equal to reflexivity.<ref>{{cite web|title=Axiom K|url=http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/axiom+K+(type+theory)|website=nLab|access-date=2022-01-21|archive-date=2022-01-19|archive-url=https://web.archive.org/web/20220119172036/http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/axiom+K+(type+theory)|url-status=live}}</ref>
* "Univalence Axiom" holds that equivalence of types is equality of types. The research into this property led to [[cubical type theory]], where the property holds without needing an axiom.<ref name=":0">{{cite journal|last1=Cohen|first1=Cyril|last2=Coquand|first2=Thierry|last3=Huber|first3=Simon|last4=Mörtberg|first4=Anders|title=Cubical Type Theory: A constructive interpretation of the univalence axiom|journal=21st International Conference on Types for Proofs and Programs (TYPES 2015)|date=2016|doi=10.4230/LIPIcs.CVIT.2016.23|doi-broken-date=1 November 2024|doi-access=free |arxiv=1611.02108|url=https://www.cse.chalmers.se/~simonhu/papers/cubicaltt.pdf|archive-url=https://ghostarchive.org/archive/20221009/https://www.cse.chalmers.se/~simonhu/papers/cubicaltt.pdf|archive-date=2022-10-09|url-status=live}}</ref>
* "Law of Excluded Middle" is often added to satisfy users who want [[classical logic]], instead of intuitionistic logic.

The [[Axiom of choice|Axiom 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 the [[Constructive mathematics|constructive]] 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. (See {{Section link|Axiom of choice#In constructive mathematics}}.)

==List of type theories==
===Major===
* [[Simply typed lambda calculus]] which is a [[higher-order logic]]
* [[Intuitionistic type theory]]
* [[System F]]
* [[Logical framework|LF]] is often used to define other type theories
* [[Calculus of constructions]] and its derivatives

===Minor===
* [[Automath]]
* [[ST type theory]]
* UTT (Luo's Unified Theory of dependent Types)
* some forms of [[combinatory logic]]
* others defined in the [[lambda cube]] (also known as [[pure type system]]s)
* others under the name [[typed lambda calculus]]

===Active research===
* [[Homotopy type theory]] explores equality of types
*[[nlab:cubical+type+theory|Cubical Type Theory]] is an implementation of homotopy type theory

==See also==
* [[Class (set theory)]]
* [[Type–token distinction]]

==Further reading==
{{refbegin}}
* {{cite web|first1=C.|last1=Aarts|first2=R.|last2=Backhouse|first3=P.|last3=Hoogendijk|first4=E.|last4=Voermans|first5=J.|last5=van der Woude|title=A Relational Theory of Datatypes|date=December 1992|publisher=Technische Universiteit Eindhoven|url=https://www.researchgate.net/publication/277287583}}
* {{cite book|first=Peter|last=Andrews B.|year=2002|isbn=978-1-4020-0763-7|title=An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof|edition=2nd|publisher=Kluwer}}
*{{cite book|first=Bart|last=Jacobs|title=Categorical Logic and Type Theory|year=1999|publisher=Elsevier|isbn=978-0-444-50170-7|series=Studies in Logic and the Foundations of Mathematics|volume=141|url=https://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html|access-date=2020-07-19|archive-date=2023-08-10|archive-url=https://web.archive.org/web/20230810075226/https://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html|url-status=live}} Covers type theory in depth, including polymorphic and dependent type extensions. Gives [[categorical semantics]].
* {{cite book|first=Luca|last=Cardelli|chapter=Type Systems|chapter-url=http://citeseer.ist.psu.edu/cardelli97type.html|editor-first=Allen B.|editor-last=Tucker|title=The Computer Science and Engineering Handbook|publisher=CRC Press|year=1996|isbn=9780849329098|pages=2208–36|access-date=2004-06-26|archive-date=2008-04-10|archive-url=https://web.archive.org/web/20080410185229/http://citeseer.ist.psu.edu/cardelli97type.html|url-status=live}}
* {{cite book|first=Jordan E.|last=Collins|year=2012|isbn=978-3-8473-2963-3|title=A History of the Theory of Types: Developments After the Second Edition of 'Principia Mathematica'|publisher=Lambert Academic Publishing|hdl=11375/12315}} Provides a historical survey of the developments of the theory of types with a focus on the decline of the theory as a foundation of mathematics over the four decades following the publication of the second edition of 'Principia Mathematica'.
* {{cite book|author-link=Robert Lee Constable|last=Constable|first=Robert L.|chapter=Naïve Computational Type Theory|chapter-url=http://www.nuprl.org/documents/Constable/naive.pdf|archive-url=https://ghostarchive.org/archive/20221009/http://www.nuprl.org/documents/Constable/naive.pdf|archive-date=2022-10-09|url-status=live|editor-first=H.|editor-last=Schwichtenberg|editor-first2=R.|editor-last2=Steinbruggen|title=Proof and System-Reliability|publisher=Springer|series=Nato Science Series II|volume=62|year=2012|orig-year=2002|isbn=9789401004138|pages=213–259}} Intended as a type theory counterpart of [[Paul Halmos]]'s (1960) ''[[Naive Set Theory (book)|Naïve Set Theory]]''
* {{cite encyclopedia|author-link=Thierry Coquand|first=Thierry|last=Coquand|title=Type Theory|date=2018|orig-year=2006|encyclopedia=[[Stanford Encyclopedia of Philosophy]]|url=http://plato.stanford.edu/entries/type-theory/}}
* {{cite book|first=Simon|last=Thompson|title=Type Theory and Functional Programming|publisher=Addison–Wesley|year=1991|isbn=0-201-41667-0|url=http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/|access-date=2006-04-03|archive-date=2021-03-23|archive-url=https://web.archive.org/web/20210323203228/http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/|url-status=live}}
* {{cite book|author-link=J. Roger Hindley|first=J. Roger|last=Hindley|title=Basic Simple Type Theory|publisher=Cambridge University Press|year=2008|orig-year=1995|isbn=978-0-521-05422-5}}<!--no idea why these get different ISBNs, they don't appear to be different editions--> A good introduction to simple type theory for computer scientists; the system described is not exactly Church's STT though. [http://www.iwu.edu/~htiede/papers/pdf/jolli-review.pdf Book review] {{Webarchive|url=https://web.archive.org/web/20110607234927/http://www.iwu.edu/~htiede/papers/pdf/jolli-review.pdf|date=2011-06-07}}
* {{cite book|first1=Fairouz D.|last1=Kamareddine|first2=Twan|last2=Laan|first3=Rob P.|last3=Nederpelt|title=A modern perspective on type theory: from its origins until today|publisher=Springer|year=2004|isbn=1-4020-2334-0}}
* {{cite book|first1=José|last1=Ferreirós|first2=José Ferreirós|last2=Domínguez|title=Labyrinth of thought: a history of set theory and its role in modern mathematics|publisher=Springer|year=2007|isbn=978-3-7643-8349-7|edition=2nd|chapter=X. Logic and Type Theory in the Interwar Period}}
* {{cite thesis|first=T.D.L.|last=Laan|title=The evolution of type theory in logic and mathematics|date=1997|type=PhD|publisher=Eindhoven University of Technology|url=https://pure.tue.nl/ws/files/1383309/498552.pdf|archive-url=https://ghostarchive.org/archive/20221009/https://pure.tue.nl/ws/files/1383309/498552.pdf|archive-date=2022-10-09|url-status=live|doi=10.6100/IR498552|isbn=90-386-0531-5}}
* Montague, R. (1973) "The proper treatment of quantification in ordinary English". In K. J. J. Hintikka, J. M. E. Moravcsik, and P. Suppes (eds.), ''Approaches to Natural Language'' (Synthese Library, 49), Dordrecht: Reidel, 221–242; reprinted in Portner and Partee (eds.) 2002, pp. 17–35. See: [https://plato.stanford.edu/entries/montague-semantics/#Bib Montague Semantics], Stanford Encyclopedia of Philosophy.''
{{refend}}

==Notes==
{{Notelist}}

==References==
{{Reflist|30em}}

==External links==

===Introductory material===
*[https://ncatlab.org/nlab/show/type+theory Type Theory at nLab], which has articles on many topics.
*[https://plato.stanford.edu/entries/type-theory-intuitionistic/ Intuitionistic Type Theory] article at the Stanford Encyclopedia of Philosophy
*[https://home.ttic.edu/~dreyer/course/papers/barendregt.pdf Lambda Calculi with Types] book by Henk Barendregt
*[https://hbr.github.io/Lambda-Calculus/cc-tex Calculus of Constructions / Typed Lambda Calculus] textbook style paper by Helmut Brandl
*[https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf Intuitionistic Type Theory] notes by Per Martin-Löf
*[https://www.cse.chalmers.se/research/group/logic/book/book.pdf Programming in Martin-Löf's Type Theory] book
*[https://homotopytypetheory.org/book/ Homotopy Type Theory] book, which proposed homotopy type theory as a mathematical foundation.

===Advanced material===
* {{scholarpedia|title=Computational type theory|urlname=Computational_type_theory|curator=Robert L. Constable}}
* [http://lists.seas.upenn.edu/mailman/listinfo/types-list The TYPES Forum] &mdash; moderated e-mail forum focusing on type theory in computer science, operating since 1987.
* [ftp://ftp.cs.cornell.edu/pub/nuprl/doc/book.ps.gz The Nuprl Book]: "Introduction to Type Theory."
* [http://www.cs.chalmers.se/Cs/Research/Logic/Types/tutorials.html Types Project lecture notes] of summer schools 2005–2008
** The [http://www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/program.html 2005 summer school] has introductory lectures
*[https://www.cs.uoregon.edu/research/summerschool/archives.html Oregon Programming Languages Summer School], many lectures and some notes.
**[https://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html Summer 2013 lectures] including [https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_YncjXRzdGq2SjKv5F2J8HUFeqN Robert Harper's talks on YouTube]
**[https://www.cs.uoregon.edu/research/summerschool/summer15/curriculum.html Summer 2015 Types, Logic, Semantics, and Verification]
* [http://math.andrej.com/category/type-theory/ Andrej Bauer's blog]

{{Computer science}}
{{Mathematical logic}}
{{Formal semantics}}

{{DEFAULTSORT:Type Theory}}
[[Category:Type theory| ]]
[[Category:Systems of formal logic]]
[[Category:Hierarchy]]