14
$\begingroup$

I've been reading up on Intuitionistic Type Theory (ITT) and it does make sense. But what I'm struggling to understand is "why" was it created in the first place?

Intuitionistic Logic (IL) and Simply-typed $\lambda$-calculus (STLC) and type theory in general predates the very existence of Martin-Löf himself! It seems that one can do everything in STLC that is doable in ITT (I may be wrong, but at least it feels that way).

So what was "novel" about ITT and how exactly did (or does) it advance the theory of computation? From what I understand, he introduced the notion of "dependent types", but it seems they were already there in STLC, in a way. Was his ITT an attempt at abstraction to understand the underlying principles of STLC and IL together? But didn't STLC already held do that? So, just why was ITT created in the first place? What is/was the point?

Here's an excerpt from Wikipedia: But I still don't get the reason behind its creation that didn't already exist before.

Martin-Löf's first draft article on type theory dates back to 1971. This impredicative theory generalized Girard's System F. However, this system turned out to be inconsistent due to Girard's paradox which was discovered by Girard when studying System U, an inconsistent extension of System F. This experience led Per Martin-Löf to develop the philosophical foundations of type theory, his meaning explanation, a form of proof-theoretic semantics, which justifies predicative type theory as presented in his 1984 Bibliopolis book...

It seems from the excerpt that the reason was to develop the "philosophical foundations of type theory" - I thought this foundation already existed (or maybe I assumed it did). Was this the main reason then?

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ If I remember correctly the reason he did so was a bit philosophical (a constructive foundation of mathematics) and not just technical, but it has been sometime since I have attended his lectures and I don't have my notes from them with me to look up. A good place to look up to grasp a better understanding of Martin-Lof's work and its comparison to other theories is Beeson's "Foundations of Constructive Mathematics". It has a chapter devoted to that. $\endgroup$
    – Kaveh
    Commented Mar 2, 2015 at 5:55
  • 1
    $\begingroup$ ps: you might want to edit the title to match what you are asking in the body, right now the title seems to ask what was the novelty in Martin-Lof's theory, while the body seems to be asking why he did it. $\endgroup$
    – Kaveh
    Commented Mar 2, 2015 at 6:02

1 Answer 1

Reset to default
24
$\begingroup$

Very briefly: the simply-typed $\lambda$-calculus does not have dependent types. Dependent types were proposed by de Bruijn and Howard who wanted to extend the Curry-Howard correspondence from propositional to first-order logic. The key contribution of Martin-Löf's is a novel analysis of equality. There are two main ways of giving Curry-Howard style account of equality.

  • Using Leibniz's rule of the identity of indiscernibles to encode propositional equality . This approach is used in the calculus of constructions, but it requires impredicative universes which were rejected by Martin-Löf for philosophical reasons.

  • A direct constructive characterisation of equality. Giving such a characterisation using identity types might be the main novelty of Martin-Löf's intuitionistic type theory.

Identity types appear deceptively simple today, but they refocussed the understanding of type-theory partly because they gave rise to intriguing semantical questions such as: are identity proofs unique? In some sense this question lead to homotopy type theory and the univalence axiom (which is incompatible with the uniqueness of identities). That the uniqueness of identity proofs is not derivable in Martin-Löf's intuitionistic type theory was shown by Hofmann and Streicher in: "The groupoid interpretation of type theory". Incidentally, this result also shows that pattern matching is not a conservative extension of traditional type theory.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.