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