Editing Type theory (section)

=== 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.