Re: [Haskell-cafe] Propositional logic question

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.