Editing Type theory (section)

==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 [[Rocq (software)|Rocq]] (previously known as ''Coq'') and [[Lean (proof assistant)|Lean]], are based on the calculus for inductive constructions, which is a [[calculus of constructions]] with inductive types.