[Haskell-cafe] Tutorial: Curry-Howard Correspondence
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:
>> Feedback appreciated.
>> Tim Newsham
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe