On Wed, May 19, 2010 at 01:37:49PM +0000, R J wrote:

This is another proof-layout question, this time from Bird 1.4.7. We're asked to define the functions curry2 and uncurry2 for currying and uncurrying functions with two arguments. Simple enough: curry2 :: ((a, b) -> c) -> (a -> (b -> c))curry2 f x y = f (x, y) uncurry2 :: (a -> (b -> c)) -> ((a, b) -> c)uncurry2 f (x, y) = f x y The following two assertions are obviously true theorems, but how are the formal proofs laid out?

There are lots of variations, I wouldn't say there's one "right" way to organize/lay out the proofs. But here's how I might do it: curry2 (uncurry2 f) x y = { def. of curry2 } uncurry2 f (x,y) = { def. of uncurry2 } f x y I'll let you do the other one. By the way, are you working through these problems just for self-study, or is it homework for a class? -Brent