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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe