Also, I was wondering if the constructor and/or function arguments should be marked strict. Otherwise, types can be inhabited by defined arguments. Since Prop is not strict in its argument, we could have the (false) theorem andAlwaysTrue :: forall p q . p :/\ q andAlwaysTrue p q = And (Prop undefined) (Prop undefined) This halts for all p and q since Prop and And are not strict. Dan Weston wrote:
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