Editing Type theory (section)

==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" />