[Haskell-cafe] (no subject)

[Brent Yorgey]

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