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

[Josef Svenningsson]

I think both Benja's and David's answers are terrific. Let me just add
a reference.
The person who's given these issues most thought is probably Per
Martin-Löf. If you want to know more about the meaning of local
connectives you should read his "On the Meanings of the Logical
Constants and the Justifications of the Logical Laws" [1]. It consists
of three lectures which I think are quite readable although I can
recommend skipping the first lecture, at least on a first read-through
since it's pretty heavy going.
In the beginning of the third lecture you will find the classic quote:
"the meaning of a proposition is determined by what it is to verify
it, or what counts as a verification of it"
This is essentially what both Benja and David said.

hth,

Josef

[1] http://www.hf.uio.no/ifikk/filosofi/njpl/vol1no1/meaning/meaning.html

On 5/11/07, Benja Fallenstein <benja.fallenstein at gmail.com> wrote:
> 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>