[Haskell-cafe] Higher order types via the Curry-Howard
josef.svenningsson at gmail.com
Sun May 13 14:24:49 EDT 2007
I think both Benja's and David's answers are terrific. Let me just add
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" . 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.
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 -> 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
More information about the Haskell-Cafe