[Haskell-cafe] Propositional logic question

[Derek Elkins]

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.