[Haskell-cafe] Tutorial: Curry-Howard Correspondence
Dan Weston
westondan at imageworks.com
Wed Oct 17 18:22:26 EDT 2007
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
>>
>>
>
>
More information about the Haskell-Cafe
mailing list