[Haskell-cafe] Higher order types via the Curry-Howard correspondence

[Gaal Yahas]

What do higher-order types like lists mean when viewed through the
Curry-Howard correspondence? I've been wondering about this for a
while. The tutorials ask me to consider

id :: forall a. a -> a
(.) :: forall a b c. (b -> c) -> (a -> b) -> (a -> c)

These represent theorems in a logical calculus, with the variables a,
b, c denoting propositions. In the case of the composition function,
the proposition (a -> c) may be deduced if (b -> c) and (a -> b)
obtain, and so on. (I've obviously skimmed some details.) We know the
function

e :: a -> b

diverges because there is no way to deduce b from a with no other
premises; the only value that satisfies this is bottom -- and so on.
But what does the following mean?

map :: (a -> b) -> [a] -> [b]

Since the empty list inhabits the type [b], this theorem is trivially
a tautology, so let's work around and demand a non-trivial proof by
using streams instead:

data Stream a = SHead a (Stream a)
sMap :: (a -> b) -> Stream a -> Stream b

What is the object "Stream a" in logic? What inference rules may be
applied to it? How is "data Stream" introduced, and what about variant
constructors?

-- 
Gaal Yahas <gaal at forum2.org>
http://gaal.livejournal.com/