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