<p>$N$, as a proposition, is isomorphic to an inductive type indexed by its size, existentially quantified over the index : you do not know statically the size of the argument, and as a result</p>

<p>So, as a logical proposition, it is quite a loose statement which is indeed inhabited by many proofs : we don't know much from the input as its information has been quantified away (that's more precise, fewer proofs as we have to work for every input)... but not much is expected either (that's not precise at all) </p>

<p>This reflect the looseness of the plain english statement :</p>

<blockquote>
  <p>For every pair of natural numbers, there is another natural number.</p>
</blockquote>

<p>or more precisely (?) :</p>

<blockquote>
  <p>Give me a number of any size, give me another number of any size, and I can give you a number of some size</p>
</blockquote>

CC BY-SA 3.0
2017-06-27T16:02:35.347Z
2017-06-27T16:02:35.347Z
nicolas
<p>Actually, the motivation for introducing dependent types goes in the opposite direction! Curry had noticed that there was a direct correspondence between typed terms in the $SK$ calculus and proofs in (minimal implicational) <em>propositional</em> logic, but there was no programing language known to correspond in such a way to <em>predicate</em> logic.</p>

<p>Indeed, introducing $\Pi$ types are necessary to model propositions of the form $\forall x.P$, which clearly do not admit representation as a simple type $A\rightarrow B$. (Actually, one can imagine a "forgetful" translation, where $A$ is the domain of $x$, and $B$ is the domain of "proofs of $P$", and in this way one can construct something very similar to certain forms of realizability, but this is clearly not an <em>isomorphism</em>.)</p>

<p>In summary, there <em>is</em> an isomorphism between functions $\mathbb{N}\rightarrow\mathbb{N}\rightarrow\mathbb{N}$ <strong>in the simply typed $\lambda$-calculus</strong> and proofs of $N\Rightarrow N\Rightarrow N$ in minimal logic, <strong>in the context $N,N\Rightarrow N$</strong>.</p>

<p>It is clear, however, that most programing languages have more than the STLC to define functions, and that there is more reason to care about the operational behavior of programs than that of (most) proofs.</p>

<p>It makes sense to use dependent types to explore these distinctions, as well as more subtle notions of types to distinguish between "computationally relevant" things and "computationally irrelevant" ones (e.g. in Coq, the $\mathrm{Prop}$ vs $\mathrm{Set}$ distinction).</p>

<p>But these were not the <em>original motivation</em> for dependent types.</p>

<hr>

<p>As a direct answer to your question, the "statement" $\mathbb{N}\Rightarrow\mathbb{N}\Rightarrow\mathbb{N}$ should be read in English as something like</p>

<blockquote>
  <p>For every pair of natural numbers, there is a natural number.</p>
</blockquote>

<p>And that's it! The fact that $\lambda x y. x+y$ and $\lambda x y. x\cdot y$ are two very computationally meaningful proofs of that statement does not factor at all into the statement as it stands.</p>

CC BY-SA 3.0
2017-06-19T06:23:19.293Z
I guess the thing that kills me is the phrasing "noticed..a direct correspondence"
Krpcannon
CC BY-SA 3.0
2017-06-19T15:05:46.400Z
@Krpcannon how so? I do need to hedge a little bit, since in the original paper the correspondence was not quite as direct as for the systems as they are usually presented today. The wikipedia page has the original citations: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#References
cody
CC BY-SA 3.0
2017-06-27T16:37:50.727Z
I don't think the "English translation" should read *another* natural number. It may well be the same number. That is, the type is also inhabited by the two projections.
Emil Jeřábek
CC BY-SA 3.0
2017-06-27T17:35:00.840Z
@EmilJeřábek I agree that the statement lends to that interpretation, I'll amend it.
cody
CC BY-SA 3.0
2017-06-18T23:32:06.957Z
2017-06-27T17:37:13.313Z
2017-06-27T17:37:13.313Z
cody
<p>By the Curry-Howard Isomorphism we view propositions (or theorems if true/inhabited) as types.</p>

<p>But take the type $\mathbb{N} \implies \mathbb{N} \implies \mathbb{N} $.</p>

<p>We have as witnesses to this type (i.e., proofs of this theorem) both</p>

<pre><code>f x y = x + y
f x y = x * y
</code></pre>

<p>Yet they "attest to the validity" of two very different programs. Is this the motivation for increasing the expressivity of a type system, as we see with dependent types? How would the type signature above be spoken in English - "for all naturals, x and y, it is true for all naturals"...? </p>

<dependent-type><curry-howard>
Motivation for Dependent Type
Krpcannon
# Motivation for Dependent Type

(Asked by: username_0 on 2017-06-18)

By the Curry-Howard Isomorphism we view propositions (or theorems if true/inhabited) as types.
But take the type $\mathbb{N} \implies \mathbb{N} \implies \mathbb{N} $.
We have as witnesses to this type (i.e., proofs of this theorem) both
f x y = x + y
f x y = x * y

Yet they "attest to the validity" of two very different programs. Is this the motivation for increasing the expressivity of a type system, as we see with dependent types? How would the type signature above be spoken in English - "for all naturals, x and y, it is true for all naturals"...?

**Tags:** dependent-type, curry-howard

---

## 2 answers

### Answer by username_2 on 2017-06-18. Score: 9 | Accepted answer

Actually, the motivation for introducing dependent types goes in the opposite direction! Curry had noticed that there was a direct correspondence between typed terms in the $SK$ calculus and proofs in (minimal implicational) *propositional* logic, but there was no programing language known to correspond in such a way to *predicate* logic.

Indeed, introducing $\Pi$ types are necessary to model propositions of the form $\forall x.P$, which clearly do not admit representation as a simple type $A\rightarrow B$. (Actually, one can imagine a "forgetful" translation, where $A$ is the domain of $x$, and $B$ is the domain of "proofs of $P$", and in this way one can construct something very similar to certain forms of realizability, but this is clearly not an *isomorphism*.)

In summary, there *is* an isomorphism between functions $\mathbb{N}\rightarrow\mathbb{N}\rightarrow\mathbb{N}$ **in the simply typed $\lambda$-calculus** and proofs of $N\Rightarrow N\Rightarrow N$ in minimal logic, **in the context $N,N\Rightarrow N$**.

It is clear, however, that most programing languages have more than the STLC to define functions, and that there is more reason to care about the operational behavior of programs than that of (most) proofs.

It makes sense to use dependent types to explore these distinctions, as well as more subtle notions of types to distinguish between "computationally relevant" things and "computationally irrelevant" ones (e.g. in Coq, the $\mathrm{Prop}$ vs $\mathrm{Set}$ distinction).

But these were not the *original motivation* for dependent types.

---

As a direct answer to your question, the "statement" $\mathbb{N}\Rightarrow\mathbb{N}\Rightarrow\mathbb{N}$ should be read in English as something like

> For every pair of natural numbers, there is a natural number.

And that's it! The fact that $\lambda x y. x+y$ and $\lambda x y. x\cdot y$ are two very computationally meaningful proofs of that statement does not factor at all into the statement as it stands.

> **Comments:**
> **username_0**: I guess the thing that kills me is the phrasing "noticed..a direct correspondence"  
> **username_2**: @Krpcannon how so? I do need to hedge a little bit, since in the original paper the correspondence was not quite as direct as for the systems as they are usually presented today. The wikipedia page has the original citations: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#References  
> **username_3**: I don't think the "English translation" should read *another* natural number. It may well be the same number. That is, the type is also inhabited by the two projections.  
> **username_2**: @EmilJeřábek I agree that the statement lends to that interpretation, I'll amend it.  

---

### Answer by username_1 on 2017-06-27. Score: 0

$N$, as a proposition, is isomorphic to an inductive type indexed by its size, existentially quantified over the index : you do not know statically the size of the argument, and as a result

So, as a logical proposition, it is quite a loose statement which is indeed inhabited by many proofs : we don't know much from the input as its information has been quantified away (that's more precise, fewer proofs as we have to work for every input)... but not much is expected either (that's not precise at all)

This reflect the looseness of the plain english statement :

> For every pair of natural numbers, there is another natural number.

or more precisely (?) :

> Give me a number of any size, give me another number of any size, and I can give you a number of some size


---

