[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Stefan O'Rear]

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