[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[jerzy.karczmarczuk at info.unicaen.fr]

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