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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe