<p>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&ouml;f's is a novel analysis of equality.
There are two main ways of giving Curry-Howard style account of equality. </p>

<ul>
<li><p>Using Leibniz's rule of the <a href="https://en.wikipedia.org/wiki/Identity_of_indiscernibles">identity of indiscernibles</a> to encode propositional equality . This approach is used in the calculus of constructions, but it requires impredicative universes which were rejected by Martin-L&ouml;f for philosophical reasons.</p></li>
<li><p>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.</p></li>
</ul>

<p>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.</p>

CC BY-SA 3.0
2015-03-01T21:41:20.770Z
2015-03-02T10:41:02.103Z
2015-03-02T10:41:02.103Z
Martin Berger
<p>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?</p>

<p>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).  </p>

<p>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?</p>

<p>Here's an excerpt from <a href="http://en.wikipedia.org/wiki/Per_Martin-L%C3%B6f#Logic">Wikipedia</a>: But I still don't get the reason behind its creation that didn't already exist before.</p>

<blockquote>
  <p>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...</p>
</blockquote>

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

CC BY-SA 3.0
2015-03-02T05:55:38.373Z
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.
Kaveh
CC BY-SA 3.0
2015-03-02T06:02:29.783Z
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.
Kaveh
<lo.logic><soft-question><type-theory><big-picture><ho.history-overview>
Why was there a need for Martin-Löf to create intuitionistic type theory?
PhD
# Why was there a need for Martin-Löf to create intuitionistic type theory?

(Asked by: username_0 on 2015-03-01)

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](http://en.wikipedia.org/wiki/Per_Martin-L%C3%B6f#Logic): 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?

**Tags:** lo.logic, soft-question, type-theory, big-picture, ho.history-overview

> **Comments:**
> **username_1**: 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.  
> **username_1**: 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.  

---

## 1 answers

### Answer by username_2 on 2015-03-01. Score: 24 | Accepted answer

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](https://en.wikipedia.org/wiki/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.


---

