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. _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
