Intuitionistic Type Theory: Encyclopedia II - Intuitionistic Type Theory - Connectives of Type Theory

Intuitionistic Type Theory - 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:

Intuitionistic Type Theory - Π-types

Π-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 for n-tuples 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.

Intuitionistic Type Theory - Σ-types

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

Intuitionistic Type Theory - Finite types

Of special importance are 0 (the empty type), 1 (the unit type) and 2 (the type of Booleans or truth values). Invoking the Curry Howard isomorphism again, 0 stands for False and 1 for True.

Using finite types we can define negation as and disjoint union, which following the Curry Howard isomorphism also represents disjunction, can be defined as .

Intuitionistic Type Theory - 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 = b and this is the proof of reflexivity refl:Πa:A.a = a.

Intuitionistic Type Theory - 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 W-types, the type of well-founded 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.

Intuitionistic Type Theory - Universes

An example of a universe is U₀, the universe of all small types, which contains names for all the types introduced so far. To every name a:U₀ 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.

Adapted from the Wikipedia article "Connectives of Type Theory", under the G.N U Free Docmentation License. Please also see http://en.wikipedia.org/wiki