[Haskell-cafe] Propositional logic question
Derek Elkins
derek.a.elkins at gmail.com
Mon Jun 25 20:02:58 EDT 2007
On Mon, 2007-06-25 at 20:41 +0100, Dave Tapley wrote:
> Hopefully this is just about on topic enough..
> (Oh and it's not home work, I just can't bring myself to let it go!)
>
> Taken from "Simon Thompson: Type Theory and Functional Programming"
>
> Section 1.1
> Exercise 1.3
>
> Question: Give a proof of (A => (B => C)) => ((A /\ B) => C).
Via the Curry-Howard correspondence, this corresponds to the type of
uncurry ( :: (a -> b -> c) -> (a,b) -> c ) and thus uncurry corresponds
to the proof. The @src lambdabot gives for uncurry is
uncurry f p = f (fst p) (snd p)
which most (careful) Haskell programmers would write as
uncurry f ~(x,y) = f x y
Try to see how the implementation of uncurry matches up to your proof of
the proposition.
More information about the Haskell-Cafe
mailing list