[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Dan Weston]

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.

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
>>
>>
> 
>