"Correctness" of type theory

Question

How to "proof" that type theory is correct? Or at least explain that it's meaningful in some sense. In what extent is this a mathematical question and in what is a philosophical one?

When type theories are introduced for example in Luo's book, the following properties are proved:

• Subject reduction
• Reduction termination
• Church-Rosser property

As far as I understand, what these properties describe is that we have a decidable type checking, and that the language of type theory is meaningful in some sense, but nothing more than this.

I asked a question on violation of strict positivity for inductive types (Example of where violation of strict positivity condition in inductive types leads to inconsistency) and in the answer I was told that non strictly positive types might lead to non existence of set theoretic model. Why we need type theoretic model here? And what it gives to us?

Answer 1

Type theories have multiple uses, and with each kind of usage comes a different notion of correctness. They two key uses are

• As a foundation of mathematics. In this context correctness means primarily that we can't deduce falisity.

• As a tool in programming. Here correctness means primarily that that well-typed programs "don't go wrong" in Milner's famous words, i.e. that they do not exhibit a certain forms of error, such as trying to execute 3 + "hello".

Both notions of correctness are related, but not the same.

Gödel's second incompleteness theorem puts serious restrictions in the way of showing the 'correctness' of type theories as a foundation of mathematics. The best you can hope for is to show 'correctness' (understood as consistency) relative to some other foundation, e.g. by giving a set-theoretic model.

The key thing we worry about with type theories is that a given type-theory is inconsistent because we can define a non-terminating term. Modern type-theories are fairly complicated beasts, and it's quite easy to make them too powerful so that a fix-point combinator becomes definable. Such fixpoint combinators inhabit every type, making the type-theory inconsistent as a foundation of mathematics. Since fixpoint combinators can be subtle, it is quite easy to overlook how one's typing system allows them to be defined. Indeed, famous foundationalists have a habit of proposing foundations of mathematics that are unsound for this reason. For example Martin-Löf's original proposal for type-theory made the kind of types itself a type (that approach to typing is now referred to as Type:Type). This is extremely convenient, and gives you the most general form of impredicative polymorphism. Alas, Girard discovered that this was unsound, when he managed to express the Burali-Forti paradox in Type:Type, see this discussion for more details. Every since, Martin-Löf's type theories have been predicative, but with added inductive definitions to recover (much of) the expressive power of impredicativity.

Encoding a type theory in another foundation such as set theory gives us a fuzzy feeling of security: it says there are unlikely to be an obvious unsoundness bugs in our type-theory. The justification behind this intuition is strictly empirical (!): in the century of since Cantor invented and Zermelo formalised it, nobody has found a soundness bug in conventional set theory. (As an aside, this situation is similar to cryptography where we trust RSA, Diffie-Hellman, AES or 3DES for little other reason than that they have withstood sustained attempts at breaking.)

Note that while a system with Type:Type is wrong as a foundation of mathematics, it is perfectly acceptable as a typing system for programming languages, because we can still show that no typeable program goes "wrong".

Regarding proof techniques for correctness, the different properties you mention relate to different notions of correctness. Termination is the key step to showing correctness of a type-theory as a foundation of mathematics, while subject reduction is usually the key step to showing that a type-theory is usable as a tool in programming. Note that since a termination proof is the high-road to consistency as a foundation, by Gödel's second incompleteness theorem, we can prove termination of a type-theory only by using a stronger system.

Answer 2

Regarding decidable type checking: this depends on whether you consider your λ-calculus with or without type annotations. System F (a.k.a second-order λ-calculus) has the three properties you cited, but it is proved that there is no algorithm that, given a System F term without type annotations, says whether this term can have a System F type.

In λ-calculi where types depend on terms (e.g. the Calculus of Constructions), it is necessary to decide when two terms are convertible (the same modulo β-reduction) during typing. This is done by checking that their normal forms are equal. The existence of normal forms and the possibility of computing them are ensured by the three properties cited.

The existence of nonterminating computations is a problem if you use type theory as a foundation of mathematics (this is what the first answer alludes to). A nonterminating term in a language that does not enforce termination, such as OCaml, may have type ∀X.X, also known as "False".

On the other hand, as pointed out before, nonterminating computations are not necessarily a problem if you use your type system for a programming language. First, certain computations are nonterminating (e.g. an operating system, the control loop of a user interface, of an airplane fly-by-wire system...); but it may be argued that such computations typically consist of a big loop whose body waits for an event and then executes a terminating computation. Furthermore, in a language such as Coq where you must prove termination, termination proofs are often very very tedious, to the extent that people often prefer to add an artificial extra argument initialized to a very high value, with some error condition if reaching zero, rather than proving termination,.