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

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 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 :

...

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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe