# Motivation for Dependent Type

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"...?

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.

• I guess the thing that kills me is the phrasing "noticed..a direct correspondence" – Krpcannon Jun 19 '17 at 6:23
• @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: en.wikipedia.org/wiki/… – cody Jun 19 '17 at 15:05
• 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 Jun 27 '17 at 16:37
• @EmilJeřábek I agree that the statement lends to that interpretation, I'll amend it. – cody Jun 27 '17 at 17:35

$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