[Haskell-cafe] Tutorial: Curry-Howard Correspondence
westondan at imageworks.com
Wed Oct 17 18:06:33 EDT 2007
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:
> Feedback appreciated.
> Tim Newsham
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe