[Haskell-cafe] Tutorial: Curry-Howard Correspondence
Stefan O'Rear
stefanor at cox.net
Wed Oct 17 21:55:21 EDT 2007
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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20071017/191cad34/attachment.bin
More information about the Haskell-Cafe
mailing list