 Intuitionistic type theory

Intuitionistic type theory, or constructive type theory, or MartinLöf type theory or just Type Theory is a logical system and a set theory 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.
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 so called BHK interpretation. The types of 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
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 for ntuples of real numbers, stands for the type of functions which given a natural number returns a tuple of real numbers of this size. The usual function space arises as a special case when the range type does not actually depend on the input, e.g. is the type of functions from natural numbers to the real numbers, which is also written as . Using the Curry–Howard isomorphism Πtypes also serve to model implication and universal quantification: e.g. a term inhabiting 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.
Σ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 2nd component depends on the first. E.g. the type stands for the type of pairs of a natural number and a tuple of real numbers of that size, i.e. this type can be used to model sequences of arbitrary length (usually called lists). The conventional Cartesian product type arises as a special case when the type of the 2nd component doesn't actually depend on the first, e.g. is the type of pairs of a natural number and a real number, which is also written as . 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 .
Equality type
Given a,b:A then a = b is the type of equality proofs that a is equal to b. There is only one (canonical) inhabitant of a = a and this is the proof of reflexivity refl:Πa:A.a = a.
Inductive types
A prime example of an inductive type is the type of natural numbers which is generated by and . An important application of the propositions as types principle is the identification of (dependent) primitive recursion and induction by one elimination constant: for any given type P(n) indexed by . 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 Vec(A,n) mentioned above, which is inductively generated by the constructors vnil:Vec(A,0) and . Applying the Curry–Howard isomorphism once more, inductive families correspond to inductively defined relations.
Universes
An example of a universe is U_{0}, the universe of all small types, which contains names for all the types introduced so far. To every name a:U_{0} we associate a type El(a), its extension or meaning. It is standard to assume a predicative hierarchy of universes: U_{n} for every natural number , where the universe U_{n + 1} contains a code for the previous universe, i.e. we have u_{n}:U_{n + 1} with El(u_{n}) = U_{n}. This hierarchy is often assumed to be cumulative, that is the codes from U_{n} are embedded in U_{n + 1}.
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
Type Theory is usually presented as a dependently typed lambda calculus, using the judgements:
 , Γ is a wellformed context of typing assumptions.
 , σ is a wellformed type in context Γ.
 , t is a wellformed term of type σ in context Γ.
 , σ and τ are equal types in context Γ.
 , t and u are equal terms of type σ in context Γ.
Of special importance is the conversion rule, which says that given and then .
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. This is because relying on computational equality means that the equality depends on computations that could be Turing complete in general and thus the equality itself is undecidable due to the halting problem. Some type theories enforce the restriction that all computations be decidable so that definitional equality may be used.
In contrast in intensional Type Theory type checking is decidable, but the representation of standard mathematical concepts is somewhat complex, since extensional reasoning requires using setoids or similar constructions. It is a subject of current discussion whether this tradeoff is unavoidable and whether the lack of extensional principles in intensional Type Theory is a feature or a bug.
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 and Agda.
See also
 Calculus of constructions
 Curry–Howard isomorphism
 Intuitionistic logic
 MartinLöf, Per
 Type theory
 Typed lambda calculus
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, Nov. 29, 1995
Categories: Dependently typed programming
 Mathematical constructivism
 Type theory
 Logic in computer science
 Intuitionism
Wikimedia Foundation. 2010.
Look at other dictionaries:
Type theory — In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general. In programming language theory, a branch of computer science … Wikipedia
Intuitionistic logic — Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well formed statements are assumed to be either true or… … Wikipedia
Type — may refer to:In philosophy: *A type is a category of being *Type token distinction *Type theory, basis for the study of type systemsIn mathematics: *Type (model theory) *Type or Arity, the number of operands a function takes *Type, any… … Wikipedia
Theory (mathematical logic) — This article is about theories in a formal language, as studied in mathematical logic. For other uses, see Theory (disambiguation). In mathematical logic, a theory (also called a formal theory) is a set of sentences in a formal language. Usually… … Wikipedia
Dependent type — Type systems Type safety Inferred vs. Manifest Dynamic vs. Static Strong vs. Weak Nominal vs. Structural Dependent typing Duck typing Latent typing Linear typing Uniqueness typing … Wikipedia
Constructive set theory — is an approach to mathematical constructivism following the program of axiomatic set theory. That is, it uses the usual first order language of classical set theory, and although of course the logic is constructive, there is no explicit use of… … Wikipedia
Background and genesis of topos theory — This page gives some very general background to the mathematical idea of topos. This is an aspect of category theory, and has a reputation for being abstruse. The level of abstraction involved cannot be reduced beyond a certain point; but on the… … Wikipedia
Set theory — This article is about the branch of mathematics. For musical set theory, see Set theory (music). A Venn diagram illustrating the intersection of two sets. Set theory is the branch of mathematics that studies sets, which are collections of objects … Wikipedia
Model theory — This article is about the mathematical discipline. For the informal notion in other parts of mathematics and science, see Mathematical model. In mathematics, model theory is the study of (classes of) mathematical structures (e.g. groups, fields,… … Wikipedia
Proof theory — is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively defined data structures such as plain lists, boxed… … Wikipedia