Intuitionistic type theory

Martin-Löf designed the type theory on the principles of mathematical constructivism. Constructivism requires any existence proof to contain a "witness". So, any proof of "there exists a prime greater than 1000" must identify a specific number that is both prime and greater than 1000. Intuitionistic type theory accomplished this design goal by internalizing the BHK interpretation. An interesting consequence is that proofs become mathematical objects that can be examined, compared, and manipulated.

Intuitionistic type theory's type constructors were built to follow a one-to-one correspondence with logical connectives. For example, the logical connective called implication (${\displaystyle A\implies B}$) corresponds to the type of a function (${\displaystyle A\to B}$). This correspondence is called the Curry–Howard isomorphism. Previous type theories had also followed this isomorphism, but Martin-Löf's was the first to extend it to predicate logic by introducing dependent types.

Intuitionistic type theory has 3 finite types, which are then composed using 5 different type constructors. Unlike set theories, type theories are not built on top of a logic like Frege's. So, each feature of the type theory does double duty as a feature of both math and logic.

If you are unfamiliar with type theory and know set theory, a quick summary is: Types contain terms just like sets contain elements. Terms belong to one and only one type. Terms like ${\displaystyle 2+2}$ and ${\displaystyle 2\cdot 2}$ compute ("reduce") down to canonical terms like 4. For more, see the article on Type theory.

The formal definition of intuitionistic type theory is written using judgements. For example, in the statement "if ${\displaystyle A}$ is a type and ${\displaystyle B}$ is a type then ${\displaystyle \textstyle \sum _{a:A}B}$ is a type" there are judgements of "is a type", "and", and "if ... then ...". The expression ${\displaystyle \textstyle \sum _{a:A}B}$ is not a judgement; it is the type being defined.

This second level of the type theory can be confusing, particularly where it comes to equality. There is a judgement of term equality, which might say ${\displaystyle 4=2+2}$. It is a statement that two terms reduce to the same canonical term. There is also a judgement of type equality, say that ${\displaystyle A=B}$, which means every element of ${\displaystyle A}$ is an element of the type ${\displaystyle B}$ and vice versa. At the type level, there is a type ${\displaystyle 4=2+2}$ and it contains terms if there is a proof that ${\displaystyle 4}$ and ${\displaystyle 2+2}$ reduce to the same value. (Obviously, terms of this type are generated using the term-equality judgement.) Lastly, there is an English-language level of equality, because we use the word "four" and symbol "${\displaystyle 4}$" to refer to the canonical term ${\displaystyle SSSS0}$. Synonyms like these are called "definitionally equal" by Martin-Löf.

The description of judgements below is based on the discussion in Nordström, Petersson, and Smith.

The formal theory works with types and objects.

A type is declared by:

• ${\displaystyle A\ {\mathsf {Type}}}$

An object exists and is in a type if:

• ${\displaystyle a{\mathbin {:}}A}$

Objects can be equal

• ${\displaystyle a=b}$

and types can be equal

• ${\displaystyle A=B}$

A type that depends on an object from another type is declared

• ${\displaystyle (x{\mathbin {:}}A)B}$

and removed by substitution

• ${\displaystyle B[x/a]}$, replacing the variable ${\displaystyle x}$ with the object ${\displaystyle a}$ in ${\displaystyle B}$.

An object that depends on an object from another type can be done two ways. If the object is "abstracted", then it is written

• ${\displaystyle [x]b}$

and removed by substitution

• ${\displaystyle b[x/a]}$, replacing the variable ${\displaystyle x}$ with the object ${\displaystyle a}$ in ${\displaystyle b}$.

The object-depending-on-object can also be declared as a constant as part of a recursive type. An example of a recursive type is:

• ${\displaystyle 0{\mathbin {:}}\mathbb {N} }$
• ${\displaystyle S{\mathbin {:}}\mathbb {N} \to \mathbb {N} }$

Here, ${\displaystyle S}$ is a constant object-depending-on-object. It is not associated with an abstraction. Constants like ${\displaystyle S}$ can be removed by defining equality. Here the relationship with addition is defined using equality and using pattern matching to handle the recursive aspect of ${\displaystyle S}$:

${\displaystyle {\begin{aligned}\operatorname {add} &{\mathbin {:}}\ (\mathbb {N} \times \mathbb {N} )\to \mathbb {N} \\\operatorname {add} (0,b)&=b\\\operatorname {add} (S(a),b)&=S(\operatorname {add} (a,b)))\end{aligned}}}$

${\displaystyle S}$ is manipulated as an opaque constant - it has no internal structure for substitution.

So, objects and types and these relations are used to express formulae in the theory. The following styles of judgements are used to create new objects, types and relations from existing ones:

${\displaystyle \Gamma \vdash \sigma \ {\mathsf {Type}}}$	σ is a well-formed type in the context Γ.
${\displaystyle \Gamma \vdash t{\mathbin {:}}\sigma }$	t is a well-formed term of type σ in context Γ.
${\displaystyle \Gamma \vdash \sigma \equiv \tau }$	σ and τ are equal types in context Γ.
${\displaystyle \Gamma \vdash t\equiv u{\mathbin {:}}\sigma }$	t and u are judgmentally equal terms of type σ in context Γ.
${\displaystyle \vdash \Gamma \ {\mathsf {Context}}}$	Γ is a well-formed context of typing assumptions.

By convention, there is a type that represents all other types. It is called ${\displaystyle {\mathcal {U}}}$ (or ${\displaystyle \operatorname {Set} }$). Since ${\displaystyle {\mathcal {U}}}$ is a type, the members of it are objects. There is a dependent type ${\displaystyle \operatorname {El} }$ that maps each object to its corresponding type. In most texts ${\displaystyle \operatorname {El} }$ is never written. From the context of the statement, a reader can almost always tell whether ${\displaystyle A}$ refers to a type, or whether it refers to the object in ${\displaystyle {\mathcal {U}}}$ that corresponds to the type.

This is the complete foundation of the theory. Everything else is derived.

To implement logic, each proposition is given its own type. The objects in those types represent the different possible ways to prove the proposition. Obviously, if there is no proof for the proposition, then the type has no objects in it. Operators like "and" and "or" that work on propositions introduce new types and new objects. So ${\displaystyle A\times B}$ is a type that depends on the type ${\displaystyle A}$ and the type ${\displaystyle B}$. The objects in that dependent type are defined to exist for every pair of objects in ${\displaystyle A}$ and ${\displaystyle B}$. Obviously, if ${\displaystyle A}$ or ${\displaystyle B}$ has no proof and is an empty type, then the new type representing ${\displaystyle A\times B}$ is also empty.

This can be done for other types (booleans, natural numbers, etc.) and their operators.

Using the language of category theory, R. A. G. Seely introduced the notion of a locally cartesian closed category (LCCC) as the basic model of type theory. This has been refined by Hofmann and Dybjer to Categories with Families or Categories with Attributes based on earlier work by Cartmell.[1]

A category with families is a category C of contexts (in which the objects are contexts, and the context morphisms are substitutions), together with a functor T : C^op → Fam(Set).

Fam(Set) is the category of families of Sets, in which objects are pairs ${\displaystyle (A,B)}$ of an "index set" A and a function B: X → A, and morphisms are pairs of functions f : A → A' and g : X → X' , such that B' _° g = f _° B — in other words, f maps B_a to B_g(a).

The functor T assigns to a context G a set ${\displaystyle Ty(G)}$ of types, and for each ${\displaystyle A:Ty(G)}$, a set ${\displaystyle Tm(G,A)}$ of terms. The axioms for a functor require that these play harmoniously with substitution. Substitution is usually written in the form Af or af, where A is a type in ${\displaystyle Ty(G)}$ and a is a term in ${\displaystyle Tm(G,A)}$, and f is a substitution from D to G. Here ${\displaystyle Af:Ty(D)}$ and ${\displaystyle af:Tm(D,Af)}$.

The category C must contain a terminal object (the empty context), and a final object for a form of product called comprehension, or context extension, in which the right element is a type in the context of the left element. If G is a context, and ${\displaystyle A:Ty(G)}$, then there should be an object ${\displaystyle (G,A)}$ final among contexts D with mappings p : D → G, q : Tm(D,Ap).

A logical framework, such as Martin-Löf's takes the form of closure conditions on the context dependent sets of types and terms: that there should be a type called Set, and for each set a type, that the types should be closed under forms of dependent sum and product, and so forth.

A theory such as that of predicative set theory expresses closure conditions on the types of sets and their elements: that they should be closed under operations that reflect dependent sum and product, and under various forms of inductive definition.

A fundamental distinction is extensional vs intensional type theory. In extensional type theory definitional (i.e., computational) equality is not distinguished from propositional equality, which requires proof. As a consequence type checking becomes undecidable in extensional type theory because programs in the theory might not terminate. For example, such a theory allows one to give a type to the Y-combinator, a detailed example of this can be found in Nordstöm and Petersson Programming in Martin-Löf's Type Theory.[2] However, this doesn't prevent extensional type theory from being a basis for a practical tool, for example, NuPRL is based on extensional type theory.

In contrast in intensional type theory type checking is decidable, but the representation of standard mathematical concepts is somewhat more cumbersome, since intensional reasoning requires using setoids or similar constructions. There are many common mathematical objects, which are hard to work with or can't be represented without this, for example, integer numbers, rational numbers, and real numbers. Integers and rational numbers can be represented without setoids, but this representation isn't easy to work with. Cauchy real numbers can't be represented without this.[3]

Homotopy type theory works on resolving this problem. It allows one to define higher inductive types, which not only define first order constructors (values or points), but higher order constructors, i.e. equalities between elements (paths), equalities between equalities (homotopies), ad infinitum.

Different forms of type theory have been implemented as the formal systems underlying of a number of proof assistants. While many are based on Per Martin-Löf's ideas, many have added features, more axioms, or different philosophical background. For instance, the NuPRL system is based on computational type theory[4] and Coq is based on the calculus of (co)inductive constructions. Dependent types also feature in the design of programming languages such as ATS, Cayenne, Epigram, Agda,[5] and Idris.[6]

Per Martin-Löf constructed several type theories that were published at various times, some of them much later than the preprints with their description became accessible to the specialists (among others Jean-Yves Girard and Giovanni Sambin). The list below attempts to list all the theories that have been described in a printed form and to sketch the key features that distinguished them from each other. All of these theories had dependent products, dependent sums, disjoint unions, finite types and natural numbers. All the theories had the same reduction rules that did not include η-reduction either for dependent products or for dependent sums, except for MLTT79 where the η-reduction for dependent products is added.

MLTT71 was the first of type theories created by Per Martin-Löf. It appeared in a preprint in 1971. It had one universe but this universe had a name in itself, i.e. it was a type theory with, as it is called today, "Type in Type". Jean-Yves Girard has shown that this system was inconsistent and the preprint was never published.

MLTT72 was presented in a 1972 preprint that has now been published.[7] That theory had one universe V and no identity types . The universe was "predicative" in the sense that the dependent product of a family of objects from V over an object that was not in V such as, for example, V itself, was not assumed to be in V. The universe was à la Russell, i.e., one would write directly "T∈V" and "t∈T" (Martin-Löf uses the sign "∈" instead of modern ":") without the additional constructor such as "El".

MLTT73 was the first definition of a type theory that Per Martin-Löf published (it was presented at the Logic Colloquium 73 and published in 1975[8]). There are identity types which he calls "propositions" but since no real distinction between propositions and the rest of the types is introduced the meaning of this is unclear. There is what later acquires the name of J-eliminator but yet without a name (see pp. 94–95). There is in this theory an infinite sequence of universes V₀, ..., V_n, ... . The universes are predicative, a-la Russell and non-cumulative! In fact, Corollary 3.10 on p. 115 says that if A∈V_m and B∈V_n are such that A and B are convertible then m = n. This means, for example, that it would be difficult to formulate univalence in this theory—there are contractible types in each of the V_i but it is unclear how to declare them to be equal since there are no identity types connecting V_i and V_j for i ≠ j.

MLTT79 was presented in 1979 and published in 1982.[9] In this paper, Martin-Löf introduced the four basic types of judgement for the dependent type theory that has since become fundamental in the study of the meta-theory of such systems. He also introduced contexts as a separate concept in it (see p. 161). There are identity types with the J-eliminator (which already appeared in MLTT73 but did not have this name there) but also with the rule that makes the theory "extensional" (p. 169). There are W-types. There is an infinite sequence of predicative universes that are cumulative.

Bibliopolis: there is a discussion of a type theory in the Bibliopolis book from 1984[10] but it is somewhat open-ended and does not seem to represent a particular set of choices and so there is no specific type theory associated with it.

• Intuitionistic logic
• Typed lambda calculus

• Martin-Löf, Per (1984). Intuitionistic type theory (PDF). Sambin, Giovanni. Napoli: Bibliopolis. ISBN 978-8870881059. OCLC 12731401.

• Per Martin-Löf's Notes, as recorded by Giovanni Sambin (1980)
• Nordström, Bengt; Petersson, Kent; Smith, Jan M. (1990). Programming in Martin-Löf's Type Theory. Oxford University Press. ISBN 9780198538141.
• Thompson, Simon (1991). Type Theory and Functional Programming. Addison-Wesley. ISBN 0-201-41667-0.
• Granström, Johan G. (2011). Treatise on Intuitionistic Type Theory. Springer. ISBN 978-94-007-1735-0.

• EU Types Project: Tutorials – lecture notes and slides from the Types Summer School 2005
• n-Categories - Sketch of a Definition – letter from John Baez and James Dolan to Ross Street, November 29, 1995