_|_ does not provide a witness to a theorem in any consistent logic (otherwise everything could be proved from it), yet it inhabits every type in Haskell. If the only invalid type instance is _|_, then a necessary and sufficient test for the C-H correspondence be the existence of a type instance that halts. Non-strict constructors would seem to mess that up. From http://en.wikipedia.org/wiki/Curry%E2%80%93Howard#Types "The problem of finding a ?-expression with a particular type is called the type inhabitation problem. The answer turns out to be remarkable: There is a closed ?-expression with a particular type only if the type corresponds to a theorem of logic, when the ? symbols are re-interpreted as meaning logical implication." By inhabit, they clearly mean no occurrence (recursively) in the type instance of _|_. I think the extra wrinkle you are introducing with constructors like Prop to wrap types is justified only insofar as the boxed and unboxed types are isomorphic, but they are not unless the constructor is strict in all its arguments. Just as _|_ :: a does not qualify as justifying theorem a, so in isomorphism Prop _|_ :: Prop a should also not qualify. If all constructors were strict, Prop _|_ = _|_ and all is fine. I am posting this to the haskell-cafe list because I am not at all sure that my understanding is right, and I don't want you to change your tutorial if it's not. Dan Weston Tim Newsham wrote:
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.
Hmm.. I'm wondering to what degree this would make a difference. I'm not actually running any of these programs. I'm just compiling them and relying on the type checker to validate the types (and check the proofs). If I understand this correctly, adding "!" wont affect the behavior of the type checking phase.
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
Tim Newsham http://www.thenewsh.com/~newsham/