I read that the Curry-Howard correspondence introduces an isomorphism between typed functions and logical statements. For example, supposedly the function
$$\begin{array}{l}
I : \forall a. a \to a\\
I = \lambda x. x
\end{array}$$
can be interpreted as:
$$p \implies p \text{ for any proposition } p$$
Is that correct? How might I interpret a function $K : \forall ab. a \to (b \to a)$? What about $\text{succ} : \mathbb{N} \to \mathbb{N}$, where $\text{succ} = \lambda x. x + 1$?
If the scope of this question is too large, can someone recommend an introductory book that would cover this? A proof of the isomorphism would probably be enlightening, too: can someone point me to one?
Best Answer
Have a look at Girard, Lafont and Taylor, Proofs and Types. It's available online in its entirety.
We can state the Curry–Howard correspondence in general terms as a correspondence between proof systems and type theories. Two ways of stating it as that proofs are programs and propositions are types. Your question looks like it's focused on the connection which Howard drew between natural deduction and the simply-typed $\lambda$-calculus.
You ask how to interpret a function $K : \forall{a, b} . a \rightarrow (b \rightarrow a)$, which is not precisely the right question to ask, because it misses the intensional aspect of the correspondence. Let $t$ be a term of type $\forall{a, b} . a \rightarrow (b \rightarrow a)$ whose extension is the function $K$. (In general there will be many such $t$ for any given $K$.) What does $t$ correspond to, then? A proof of the proposition which its type corresponds to: the proposition that for arbitrary propositions $a$ and $b$, $a \rightarrow (b \rightarrow a)$.
What might $t$ look like? We can figure this out to some extent because of its type. Start with $r : b \rightarrow a$. Let $v : a$ and $x : b$. Then let $r := \lambda x. v$. Then $t := \lambda y. (\lambda x. v)$.
Of course this isn't terribly informative: to figure out anything substantial we'd need to know what $v$ is. There are lots of things it might be: here's one which fits. Let $v := y$. Then $t := \lambda y. (\lambda x. y)$. In other words, provide terms $u : a$ and $s: b$ (which, remember, are proofs of $a$ and $b$ respectively), so then $(t[u / y])[s / x]$ reduces to just $u$, which is a proof of $b$.