Intuitionistic type theory (also known as constructive type theory, or MartinLöf type theory) is a type theory and an alternative foundation of mathematics based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per MartinLöf, a Swedish mathematician and philosopher, in 1972. MartinLöf has modified his proposal a few times; his 1971 impredicative formulation was inconsistent as demonstrated by Girard's paradox. Later formulations were predicative. He proposed both intensional and extensional variants of the theory. For more detail see the section on MartinLöf type theories below.
Intuitionistic type theory is based on a certain analogy or isomorphism between propositions and types: a proposition is identified with the type of its proofs. This identification is usually called the Curry–Howard isomorphism, which was originally formulated for intuitionistic logic and simply typed lambda calculus. Type theory extends this identification to predicate logic by introducing dependent types, that is types which contain values.
Type theory internalizes the interpretation of intuitionistic logic proposed by Brouwer, Heyting and Kolmogorov, the socalled BHK interpretation. The types in type theory play a similar role to sets in set theory but functions definable in type theory are always computable.
Contents

Connectives of type theory 1

Πtypes 1.1

Σtypes 1.2

Finite types 1.3

Equality type 1.4

Inductive types 1.5

Universes 1.6

Formalisation of type theory 2

Categorical models of type theory 3

Extensional versus intensional 4

Implementations of type theory 5

MartinLöf Type Theories 6

See also 7

References 8

Further reading 9

External links 10

References 11
Connectives of type theory
In the context of type theory a connective is a way of constructing types, possibly using already given types. The basic connectives of type theory are:
Πtypes
Πtypes, also called dependent product types, are analogous to the indexed products of sets. As such, they generalize the normal function space to model functions whose result type may vary on their input. E.g. writing \operatorname{Vec}({\mathbb R}, n) for the type of ntuples of real numbers and \mathbb N for the type of natural numbers,

\prod_{n \mathbin{:} {\mathbb N}} \operatorname{Vec}({\mathbb R}, n)
stands for the type of a function that, given a natural number n, returns an ntuple of real numbers. The usual function space arises as a special case when the range type does not actually depend on the input, e.g., \prod_{n \mathbin{:} {\mathbb N}} {\mathbb R} is the type of functions from natural numbers to the real numbers, which is also written as {\mathbb N} \to {\mathbb R}.
Using the Curry–Howard isomorphism Πtypes also serve to model implication and universal quantification: e.g., a term inhabiting

\prod_{m, n \mathbin{:} {\mathbb N}} (m + n = n + m)
is a function which assigns to any pair of natural numbers a proof that addition is commutative for that pair and hence can be considered as a proof that addition is commutative for all natural numbers. (Here we have used the equality type (x = y) as explained below.)
Σtypes
Σtypes, also called dependent sum types, are analogous to the indexed disjoint unions of sets. As such, they generalize the usual Cartesian product to model pairs where the type of the second component depends on the first. For example, the type \sum_{n \mathbin{:} {\mathbb N}} \operatorname{Vec}({\mathbb R}, n) stands for the type of pairs of a natural number n and an ntuple of real numbers, i.e., this type can be used to model sequences of arbitrary but finite length (usually called lists). The conventional Cartesian product type arises as a special case when the type of the second component doesn't actually depend on the first, e.g., \sum_{n \mathbin{:} {\mathbb N}} {\mathbb R} is the type of pairs of a natural number and a real number, which is also written as {\mathbb N} \times {\mathbb R}.
Again, using the Curry–Howard isomorphism, Σtypes also serve to model conjunction and existential quantification.
Finite types
Of special importance are 0 or ⊥ (the empty type), 1 or ⊤ (the unit type) and 2 (the type of Booleans or classical truth values). Invoking the Curry–Howard isomorphism again, ⊥ stands for false and ⊤ for true.
Using finite types we can define negation as

\neg A \equiv A \to \bot.
Equality type
Given a, b \mathbin{:} A, the expression a = b denotes the type of equality proofs for a is equal to b. That is, if a = b is inhabited, then a is said to be equal to b. There is only one (canonical) inhabitant of a = a and this is the proof of reflexivity

\operatorname{refl} \mathbin{:} \prod_{a \mathbin{:} A} (a = a).
Examination of the properties of the equality type, or rather, extending it to a notion of equivalence, lead to homotopy type theory.
Inductive types
A prime example of an inductive type is the type of natural numbers \mathbb{N} which is generated by 0 \mathbin{:} {\mathbb N} and \operatorname{succ} \mathbin{:} {\mathbb N} \to {\mathbb N}. An important application of the propositions as types principle is the identification of (dependent) primitive recursion and induction by one elimination constant:

{\operatorname\, \mathbin{:} P(0)\, \to \left(\prod_{n \mathbin{:} {\mathbb N}} P(n) \to P(\operatorname{succ}(n))\right) \to \prod_{n \mathbin{:} {\mathbb N}} P(n)
for any given type P(n) indexed by n \mathbin{:} {\mathbb N}. In general inductive types can be defined in terms of Wtypes, the type of wellfounded trees.
An important class of inductive types are inductive families like the type of vectors \operatorname{Vec}(A, n) mentioned above, which is inductively generated by the constructors \operatorname{vnil} \mathbin{:} \operatorname{Vec}(A, 0) and

\operatorname{vcons}\, \mathbin{:}\, A \to \prod_{n \mathbin{:} {\mathbb N}} \operatorname{Vec}(A, n) \to \operatorname{Vec}(A, \operatorname{succ}(n)).
Applying the Curry–Howard isomorphism once more, inductive families correspond to inductively defined relations.
Universes
An example of a universe is \mathcal{U}_0, the universe of all small types, which contains names for all the types introduced so far. To every name a \mathbin{:} \mathcal{U}_0 we associate a type \operatorname{El}(a), its extension or meaning. It is standard to assume a predicative hierarchy of universes: \mathcal{U}_n for every natural number n \mathbin{:} {\mathbb N}, where the universe \mathcal{U}_{n+1} contains a code for the previous universe, i.e., we have u_n \mathbin{:} \mathcal{U}_{n+1} with \operatorname{El}(u_n) \equiv \mathcal{U}_n. (A hierarchy with this property is called "cumulative".)
Stronger universe principles have been investigated, i.e., super universes and the Mahlo universe. In 1992 Huet and Coquand introduced the calculus of constructions, a type theory with an impredicative universe, thus combining type theory with Girard's System F. This extension is not universally accepted by Intuitionists since it allows impredicative, i.e., circular, constructions, which are often identified with classical reasoning.
Formalisation of type theory
This formalization is based on the discussion in Nordström, Petersson, and Smith.
The formal theory works with types and objects.
A type is declared by:
An object exists and is in a type if:
Objects can be equal
and types can be equal
A type that depends on an object from another type is declared
and removed by substitution

B[x / a] , replacing the variable x with the object a in 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
and removed by substitution

b[x / a] , replacing the variable x with the object a in b.
The objectdependingonobject can also be declared as a constant as part of a recursive type. An example of a recursive type is:

0 \mathbin{:} \mathbb{N}

\operatorname{succ} \mathbin{:} \mathbb{N} \to \mathbb{N}
Here, \operatorname{succ} is a constant objectdependingonobject. It is not associated with an abstraction. Constants like \operatorname{succ} 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 \operatorname{succ}:

\begin{align} \operatorname{add} &\mathbin{:}\ (\mathbb{N} \times \mathbb{N}) \to \mathbb{N} \\ \operatorname{add}(0, b) &= b \\ \operatorname{add}(\operatorname{succ}(a), b) &= \operatorname{succ}(\operatorname{add}(a, b))) \end{align}
\operatorname{succ} 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:
\Gamma\vdash \sigma\ \mathsf{Type}

σ is a wellformed type in the context Γ.

\Gamma\vdash t \mathbin{:} \sigma

t is a wellformed term of type σ in context Γ.

\Gamma\vdash \sigma \equiv \tau

σ and τ are equal types in context Γ.

\Gamma\vdash t \equiv u \mathbin{:} \sigma

t and u are judgmentally equal terms of type σ in context Γ.

\vdash \Gamma\ \mathsf{Context}

Γ is a wellformed context of typing assumptions.

By convention, there is a type that represents all other types. It is called \mathcal{U} (or \operatorname{Set}). Since \mathcal{U} is a type, the member of it are objects. There is a dependent type \operatorname{El} that maps each object to its corresponding type. In most texts \operatorname{El} is never written. From the context of the statement, a reader can almost always tell whether A refers to a type, or whether it refers to the object in \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 A \times B is a type that depends on the type A and the type B. The objects in that dependent type are defined to exist for every pair of objects in A and B. Obviously, if A or B has no proof and is an empty type, then the new type representing A \times B is also empty.
This can be done for other types (booleans, natural numbers, etc.) and their operators.
Categorical models of type theory
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.
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 (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 Ty(G) of types, and for each A : Ty(G), a set 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 Ty(G) and a is a term in Tm(G,A), and f is a substitution from D to G. Here Af : Ty(D) and 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 A : Ty(G), then there should be an object (G,A) final among contexts D with mappings p : D → G, q : Tm(D,Ap).
A logical framework, such as MartinLö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.
Extensional versus intensional
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 Ycombinator, a detailed example of this can be found in.^{[1]} 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. From a practical standpoint there's no difference between a program which doesn't terminate and a program which takes a million years to terminate.
In contrast in intensional type theory type checking is decidable, but the representation of standard mathematical concepts is somewhat more cumbersome, since extensional 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. Real numbers can't be represented without this see.^{[2]}
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.
Implementations of type theory
Type theory has been the base of a number of proof assistants, such as NuPRL, LEGO and Coq. Recently, dependent types also featured in the design of programming languages such as ATS, Cayenne, Epigram, Agda, and Idris.
MartinLöf Type Theories
Per MartinLof 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. 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 MartinLö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.^{[3]} 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 ala Russell, i.e., one would write directly "T∈V" and "t∈T" (MartinLöf uses the sign "∈" instead of modern ":") without the additional constructor such as "El".
MLTT73 It was the first definition of a type theory that Per MartinLöf published (it was presented at the Logic Colloquium 73 and published in 1975^{[4]}). 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 Jeliminator but yet without a name (see pp. 94–95). There is in this theory an infinite sequence of universes V_{0},...,V_{n},... . The universes are predicative, ala Russell and noncumulative! 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 It was presented in 1979 and published in 1982.^{[5]} This is a very important and interesting paper. In it MartinLöf introduced the four basic types of judgement for the dependent type theory that has since became fundamental in the study of the metatheory of such systems. He also introduced contexts as a separate concept in it (see p. 161). There are identity types types with the Jeliminator (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 Wtypes. 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^{[6]} but it is somewhat openended and does not seem to represent a particular set of choices and so there is no specific type theory associated with it.
See also
References

Per MartinLöf (1984). Intuitionistic Type Theory Bibliopolis. ISBN 8870881059.
Further reading

Bengt Nordström; Kent Petersson; Jan M. Smith (1990). Programming in MartinLöf's Type Theory. Oxford University Press. The book is out of print, but a free version can be picked up from here.

Thompson, Simon (1991). Type Theory and Functional Programming AddisonWesley. ISBN 0201416670.

Granström, Johan G. (2011). Treatise on Intuitionistic Type Theory Springer. ISBN 9789400717350.
External links

EU Types Project: Tutorials  lecture notes and slides from the Types Summer School 2005

nCategories  Sketch of a Definition  letter from John Baez and James Dolan to Ross Street, November 29, 1995
References

^ Bengt Nordström; Kent Petersson; Jan M. Smith (1990). Programming in MartinLöf's Type Theory. Oxford University Press p.90

^ Altenkirch, Thorsten, Thomas Anberrée, and Nuo Li. "Definable Quotients in Type Theory."

^ Per MartinLöf, An intuitionistic theory of types, Twentyfive years of constructive type theory (Venice,1995), Oxford Logic Guides, v. 36, pp. 127172, Oxford Univ. Press, New York, 1998

^ Per MartinLöf, An intuitionistic theory of types: predicative part, Logic Colloquium '73 (Bristol, 1973), 73118. Studies in Logic and the Foundations of Mathematics, Vol. 80, NorthHolland, Amsterdam,1975

^ Per MartinLöf, Constructive mathematics and computer programming, Logic, methodology and philosophy of science, VI (Hannover, 1979), Stud. Logic Found. Math., v. 104, pp. 153175, NorthHolland, Amsterdam, 1982

^ Per MartinLöf, Intuitionistic type theory, Studies in Proof Theory. Lecture Notes, v. 1, Notes by Giovanni Sambin, pp. iv+91, 1984
This article was sourced from Creative Commons AttributionShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, EGovernment Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a nonprofit organization.