[Haskell-cafe] (no subject)
Brent Yorgey
byorgey at seas.upenn.edu
Wed May 19 11:30:31 EDT 2010
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
More information about the Haskell-Cafe
mailing list