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