Dan Weston writes:
... now I am totally flummoxed:
thm1 :: (a -> a) -> a
thm1 f = let x = f x in x
> thm1 (const 1)
1
I *thought* that the theorem ((a => a) => a) is not derivable (after all,
0^(0^0) = 0^1 = 0), but it appears somehow that thm1 is a proof of its
type.
Help, I just unlearned everything I ever thought I new about the C-H
correspondence!
No, the world is not so cruel. This is not a theorem, you cannot really
derive it by constructing a polymorphic function, I cheated, because
your statement was negligent.
(const 1) is not a function of type (a->a), the only function *really* of
that type is id.
People, use Djinn!
The slave of the Lamp of Alladenartson will send you to Walhalla if
you ask: what ? (a->a)->a
Jerzy Karczmarczuk
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
