[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Dan Weston]

That is a great tutorial. Thanks! But in the last two sentences of the 
introduction you say:

 > We just need to find any program with the given type.
 > The existence of a program for the type will be a proof
 > of the corresponding proposition!

Maybe you should make explicit that

1) the type is inhabited

undefined :: forall p . p

does not prove that all propositions are true

2) the function must halt for all defined arguments

fix :: forall p . (p -> p) -> p
fix f = let x = f x in x

does not prove the (false) theorem

(p => p) => p

even though (fix id) is well-typed and id is certainly not undefined 
(though fix id is).

Tim Newsham wrote:
> A tutorial on the Curry-Howard Correspondence in Haskell:
>   http://www.thenewsh.com/%7Enewsham/formal/curryhoward/
> 
> Feedback appreciated.
> 
> Tim Newsham
> http://www.thenewsh.com/~newsham/
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
>