Intuitionistic Type Theory
|
|
Intuitionistic Type Theory, or Constructive Type Theory, or Martin-Löf Type Theory or just Type Theory (with capital letters) is at the same time a functional programming language, a logic and a set theory based on the principles of mathematical constructivism. Type Theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher, in 1972. Martin-Löf has modified his proposal a few times; proposing first impredicative and then predicative, and first extensional and then intensional variants of Type Theory.
Type Theory is based on the identification of 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 propositional 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 as sets in set theory but functions 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:
<math>\Pi<math>-types
<math>\Pi<math>-types, also called dependent function types, generalize the normal function space to model functions whose result type may vary on their input. E.g. writing <math>\mbox{Vec}({\mathbb R},n)<math> for <math>n<math>-tuples of real numbers, <math>\Pi n:{\mathbb N}.\mbox{Vec}({\mathbb R},n)<math> 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. <math>\Pi n:{\mathbb N}.{\mathbb R}<math> is the type of functions from natural numbers to the real numbers, which is also written as <math>{\mathbb N}\to{\mathbb R}<math>. Using the Curry Howard isomorphism <math>\Pi<math>-types also serve to model implication and universal quantification: e.g. a term inhabiting <math>\Pi m,n:{\mathbb N}.m+n = n+m<math> 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.
<math>\Sigma<math>-types
<math>\Sigma<math>-types, also called dependent product types, generalize the usual Cartesian product to model pairs where the type of the 2nd component depends on the first. E.g. the type <math>\Sigma n:{\mathbb N}.\mbox{Vec}({\mathbb R},n)<math> 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. <math>\Sigma n:{\mathbb N}.{\mathbb R}<math> is the type of pairs of a natural number and a real number, which is also written as <math>{\mathbb N}\times{\mathbb R}<math>. Again, using the Curry Howard isomorphism, <math>\Sigma<math>-types also serve to model conjunction and existential quantification.
Finite types
Of special importance are <math>0<math> (the empty type), <math>1<math> (the unit type) and <math>2<math> (the type of Booleans or truth values). Invoking the Curry Howard isomorphism again, <math>0<math> stands for False and <math>1<math> for True.
Using finite types we can define negation as <math>\neg A = A \to 0<math> and disjoint union, which following the Curry Howard isomorphism also represents disjunction, can be defined as <math>A+B = \Sigma b:2.\mbox{if}\,b\,\mbox{then}\,A\,\mbox{else}\, B<math>.
Equality type
Given <math>a,b : A<math> then <math>a = b<math> is the type of equality proofs that <math>a<math> is equal to <math>b<math>. There is only one (canonical) inhabitant of <math>a = b<math> and this is the proof of reflexivity <math>\mbox{refl} : \Pi a:A.a = a<math>.
Inductive types
A prime example of an inductive type is the type of natural numbers <math>\mathbb N<math> which is generated by <math>0 : {\mathbb N}<math> and <math>\mbox{succ} :{\mathbb N} \to {\mathbb N}<math>. An important application of the propositions as types principle is the identification of (dependent) primitive recursion and induction by one elimination constant: <math>{\mathbb N}-\mbox{elim} : P(0) \to (\Pi n:{\mathbb N}.P(n)\to P(\mbox{succ}(n)))\to\Pi n:{\mathbb N}.P(n)<math> for any given type <math>P(n)<math> indexed by <math>n:{\mathbb N}<math>. In general inductive types can be defined in terms of W-types, the type of well-founded trees.
An important class of inductive types are inductive families like the type of vectors <math>\mbox{Vec}(A,n)<math> mentioned above, which is inductively generated by the constructors <math>\mbox{vnil}:\mbox{Vec}(A,0)<math> and <math>\mbox{vcons}:A\to\Pi n:{\mathbb N}.\mbox{Vec}(A,n)\to\mbox{Vec}(A,\mbox{succ}(n))<math>. Applying the Curry Howard isomorphism once more, inductive families correspond to inductively defined relations.
Universes
An example of a universe is <math>U_0<math>, the universe of all small types, which contains names for all the types introduced so far. To every name <math>a:U_0<math> we associate a type <math>El(a)<math>, it's extension or meaning. It is standard to assume a predicative hierarchy of universes: <math>U_n<math> for every natural number <math>n:{\mathbb N}<math>, where the universe <math>U_{n+1}<math> contains a code for the previous universe, i.e. we have <math>u_n:U_{n+1}<math> with <math>El(u_n)=U_n<math>. This hierarchy is often assumed to be cumulative, that is the codes from <math>U_n<math> are embedded in <math>U_{n+1}<math>.
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:
- <math>\vdash \Gamma\, \mbox{Context}<math>, <math>\Gamma<math> is a well-formed context of typing assumptions.
- <math>\Gamma\vdash \sigma\, \mbox{Type}<math>, <math>\sigma<math> is a well-formed type in context <math>\Gamma<math>.
- <math>\Gamma\vdash t : \sigma<math>, <math>t<math> is a well-formed term of type <math>\sigma<math> in context <math>\Gamma<math>.
- <math>\Gamma\vdash \sigma\equiv\tau<math>, <math>\sigma<math> and <math>\tau<math> are equal types in context <math>\Gamma<math>.
- <math>\Gamma\vdash t \equiv u: \sigma<math>, <math>t<math> and <math>u<math> are equal terms of type <math>\sigma<math> in context <math>\Gamma<math>.
Of special importance is the conversion rule, which says that given <math>\Gamma\vdash t : \sigma<math> and <math>\Gamma\vdash \sigma\equiv\tau<math> then <math>\Gamma\vdash t : \tau<math>.
Categorical models of Type Theory
Using the language of Category Theory, 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.
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 contrast in intensional Type Theory type checking is decidable, but the representation of many mathematical concepts is non-standard due to a lack of extensional reasoning. 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 Dependent ML and Epigram.
See also
- Typed lambda calculus
- Curry-Howard isomorphism
- Intuitionistic logic
- Calculus of constructions
- Per Martin-Löf
External links
- Bengt Nordström; Kent Petersson; Jan M. Smith (1990). Programming in Martin-Löf's Type Theory. Oxford University Press. The book is out of print, but a free version can be picked up from here (http://www.cs.chalmers.se/Cs/Research/Logic/book/).
- Thompson, Simon (1991). Type Theory and Functional Programming (http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/) Addison-Wesley. ISBN 0-201-41667-0.