[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Dan Weston]

_|_ 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 at haskell.org
>>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>>
>>>>
>>>
>>>
>>
>>
> 
> Tim Newsham
> http://www.thenewsh.com/~newsham/
> 
>