Martin-Lf dependent type theory
Context
Type theory
Foundations
foundations
The basis of it all
Foundational axioms
Removing axioms
Martin-Löf dependent type theory
Idea
Per Martin-Löf‘s dependent type theory, also known as intuitionistic type theory, or constructive type theory is a specific form of type theory developed to support constructive mathematics. (Note that both “dependent type theory” and “intuitionistic type theory” may refer more generally to type theories that contain dependent types or are intuitionistic, respectively.)
Martin-Löf’s dependent type theory is notable for several reasons:
-
One can construct an interpretation of first-order intuitionistic logic by interpreting propositions as types (this is true of most any dependent type theory).
-
It has a version of a variant of the axiom of choice as a theorem (because of the properties of the above interpretation), see the discussion below.
-
In its intensional form, it has sufficient computational content to function as a programming language. At the same time, it then has identity types whose presence shows that one is really dealing with a form of homotopy type theory.
Syntax
If is a term, and a type, then is a typing declaration asserting that is a term of type . We will define the forms of valid terms and types below; to begin with, we assume we have a stock of variables, atomic types, and parametrised types.
A context is a finite ordered list of typing declarations, defined inductively as follows:
- The empty list is a valid context.
- If is a valid context, is a variable not appearing in , and is a valid type in the context , then the context obtained by appending to is also valid.
Note that this must be considered a mutual inductive definition along with the definition of when a type is valid in a given context, which is to be given below in terms of type constructors.
We write to assert that is a valid typing declaration in the context of , and by abuse of notation we may write to assert that is a valid type in the context of .
For any context , if is an atomic type, .
If is a typing declaration in , then we have .
Binary product types
If and , then .
If and then .
If , then and .
Unit type
There is an atomic type called .
For any context we have .
Dependent product types
If , then .
If , then .
If and , then .
Function types
Function types may be regarded as a special case of dependent product types, where does not depend on at all. When we write out the rules for dependent products in this case, they become the following.
Firstly, if and , then .
If , then .
If and , then .
Binary sum types
If and , then .
If and , then ; and if and , then .
If , and , then .
Empty type
There is an atomic type called .
If , then .
Dependent sum types
If , then .
If , and , then .
If and , then .
Note that just as function types can be defined to be dependent products where does not depend on , binary product types (above) can be defined to be dependent sums where does not depend on .
Finite types
Martin-Löf also includes in his type theory a type with exactly elements, for every external natural number . The types and can then be defined as and , respectively. On the other hand, with and given as above, one may define , , and so on (by recursion on the external natural number ).
Note that we have not included any axiom of infinity, however.
Propositions as types
Under the Curry-Howard isomorphism, we may identify propositions with certain atomic types and predicates with certain parametrised types.
An inhabitant of such a proposition-as-a-type is interpreted as a ‘proof’ of that proposition.
We write for the judgement that is inhabited: that is, if , then . The type-formation rules above are then seen to be the rules of inference for (a fragment of) intuitionistic first-order logic. Indeed, we have:
- Conjunction introduction:
- Conjunction elimination:
- Truth introduction
- Universal generalisation:
- Universal instantiation:
- Conditional proof (implication introduction):
- Modus ponens (implication elimination):
- Disjunction introduction:
- Disjunction elimination:
- False elimination:
- Existential generalisation:
- Existential instantiation:
The only traditional rule of inference we are missing is the rule of excluded middle, so this logic is intuitionistic.
The above interpretation justifies the use of the symbols , , , instead of , , , , when we are using types to represent propositions.
Equality types
We may introduce a family of equality types for each type and each pair of terms of that type: if and , then .
These are not the intensional identity types which Martin-Löf later introduced as a particular sort of inductive family of types, but instead an extensional notion of equality defined by induction over the class of all types (regarded as inductively defined by the above type-formation clauses). Note that it is essential, for a purpose such as this, that the type-formation clauses be regarded as an inductive definition, rather than as “operations” defined on some pre-existing collection of types: in order to define equality in the way we are about to do, we have to be able to inspect a given type and decide uniquely which rule was used to construct it.
The equality type is reflexive, symmetric, and transitive. That means, for example, if , , , and then .
Mike Shulman: Is that (reflexivity, symmetry, and transitivity) a rule we are giving, or an assertion we are making about derivability? I’m a little unsure because the presentation here is slightly different from that in the reference: there Martin-Löf uses both a propositional equality and a judgmental one.
Finite product types
If , and , then and .
If , then .
Unit type
If , then .
Dependent product types
If and , then .
If , then .
Function types
If and , then .
If , then .
Binary sum types
If and , and , then and
Dependent sum types
If , and , then .
The other equality rule for dependent sum types is derivable from the above.
Properties
Models and categorical semantics
The models of ML type theory depend crucially on whether one considers the variant of extensional type theory or that of intensional type theory.
The models of the extensional version are (just) locally cartesian closed categories.
The faithful models of the intensional version with identity types are however certain (∞,1)-categories, notably (∞,1)-toposes, presented by simplicial model categories (Warren). For this reason one speaks of homotopy type theory.
For a more detailed discussion of these matters see at relation between type theory and category theory.
Axiom of choice
In dependent type theory we can verify the following “logical form of the axiom of choice” (Bell, Tait), see also (Rijke, section 2.5.1).
Theorem
(ACL)
One should note carefully that this “is” only “the axiom of choice” under the above propositions-as-types interpretation of the quantifiers and .
References
See also the references at type theory.
The original reference is
-
Per Martin-Löf, Intuitionistic type theory (1984)
-
Per Martin-Löf, An intuitionistic theory of types: predicative part, In Logic Colloquium (1973), ed. H. E. Rose and J. C. Shepherdson (North-Holland, 1974), 73-118. (web)
A philosophical examination is
An introduction and survey (with an eye towards homotopy type theory) is in chapter 1 of
- Michael Warren, Homotopy theoretic aspects of constructive type theory, PhD thesis (2008) (pdf)
as well as
- Egbert Rijke, Homotopy type theory (2012) (pdf)
A discussion of ML dependent type theory as the internal language of locally cartesian closed categories is in
- R. A. G. Seely, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. (1984) 95 (pdf)
Discussion of the logical axiom of choice in dependent type theory is in
- John Bell, The Axiom of choice in type theory, Stanford Encyclopedia of philosophy, 2008 (web)