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