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

[Benja Fallenstein]

Adding some thoughts to what David said (although I don't understand
the issues deeply enough to be sure that these ideas don't lead to
ugly things like paradoxes)--

2007/5/10, Gaal Yahas <gaal at forum2.org>:
> 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?

It's not that much more interesting than "list." The 'data'
declaration can be read as,

"To prove the proposition (Stream a), you must prove the proposition
'a' and the proposition 'Stream a.'"

In ordinary logic this would mean that you couldn't prove (Stream a),
of course, but that just corresponds to strict languages in which you
couldn't construct an object of type Stream a (because it would have
to be infinite). To make sense of this, we need to assume a logic in
which we can have similar 'infinite proofs.' (This is the part where
I'm not sure it's really possible to do. I haven't read the Pierce
chapter David refers to.)

With that reading, (Stream a) is basically the same proposition as (a)
-- as evidenced by

f x = SHead x (f x)  -- f :: a -> Stream a
g (SHead x) = x  -- g :: Stream a -> a

We can find more interesting propositions, though. Here's an example
(perhaps not useful, but I find it interesting :-)):

data Foo a b = A a | Fn (Foo a b -> b)

We can prove this proposition if we can prove one of these propositions:

a
a -> b
(a -> b) -> b
((a -> b) -> b) -> b
...

Each of these is weaker than the previous one; if x is a proof of
proposition n, then (\f -> f x) is a proof of proposition n+1. The
fourth one is a tautology in classical logic, but not in
intuitionistic logic.

- Benja