Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence

_|_ 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/

On Wed, Oct 17, 2007 at 06:45:04PM -0700, Dan Weston wrote:
_|_ 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.
This is fine, but function types complicate the issue dramatically. In the CPO interpretation (from whence ⊥ originates), a function type is to be regarded as a product with one value of the co-domain for each value of the domain. If you force function types to be strict, you require the function to never produce ⊥, which gets you right back where you started - functions must be total. Stefan
participants (2)
-
Dan Weston
-
Stefan O'Rear