This blog is moving home...

 ... and can now be found here.

Discussing "Intuitionistic Type Theory"

(Link)

Author: Per Martin-Löf (University of Stockholm)

Reference: Per Martin-Löf, Intuitionistic Type Theory, Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980 (1984)

Why this paper? Cited by A conservativity result for homotopy elementary types in dependent type theory, Topological Quantum Gates in Homotopy Type Theory, and A parametricity-based formalization of semi-simplicial and semi-cubical sets

5 years on from Martin-Löf’s seminal paper on type theory (on which I have written before; I will try to avoid repeating myself), he presented his approach to a mixed audience of computer scientists, mathematicians, and philosophers. As such, these notes are quite accessible to a range of audiences, with time spent on questions like “What is it we must know in order to have the right to judge something to be a set?”, plenty of examples, and a fairly light touch on metatheorems about his system. However this is not merely a teaching course on his 1975 material, and we see two major new ideas enter his type theory here (and also in his almost simultaneously published paper Constructive mathematics and computer programming, which covers similar ground but is much briefer).

The first is the reflection rule, which allows ‘propositional’ equalities proved within the system to be used freely to replace equals by equals anywhere (as a fully fledged ‘definitional’ equality). This captures the strong extensional view of equality, as opposed to the intensional view of the older work in which objects enjoy first class equality only if they are described the same way, up to some automatic conversions. This is an old concept from philosophy of language, where Superman and Clark Kent are extensionally but not intensionally equal, because there are places in language for which they are not interchangeable: “Clark Kent is a civilian identity” does not imply “Superman is a civilian identity”. Martin-Löf notably does not discuss the reasons for this change or its ramifications. In fact it is known to have unfortunate consequences computationally, violating one of the keystone theorems of his earlier paper – the decidability of type checking – among other troublesome aspects. This does not make extensional type theory useless; it is the right tool for much ‘pen and paper’ type theory in which we want to work synthetically in a particular mathematical setting but use the strong form of equality usually preferred by mathematicians.

The second new idea is the introduction of W-types (at least, I believe this is their first appearance), which gives a general tree-like syntax for inductive types such as natural numbers and lists.

Finally, I would note the interesting fact that, linguistically at least, Martin- Löf repeatedly conflates the terms ‘type’ and ‘set’. This does not reflect most modern practice, in which category theory is usually the language of choice for defining denotational semantics, opening the way for the interpretation of type theory in mathematical settings others than sets. Indeed, in homotopy type theory (invented in part to find an interesting middle way between extensional and intensional equality) the notion of type is strictly more general than that of set: a set is a type without interesting equalities.