On Mon, 2008-12-08 at 23:15 +0100, Joachim Breitner wrote:
Hi,
Am Montag, den 08.12.2008, 15:59 -0600 schrieb Nathan Bloomfield:
Slightly off topic, but the A^B notation for hom-sets also makes the natural isomorphism we call currying expressable as A^(BxC) = (A^B)^C.
So A^(B+C) = A^B × A^C ?
Oh, right, I guess that’s actually true:
uncurry either :: (a -> c, b -> c) -> (Either a b -> c) (\f -> (f . Left, f . Right)) :: (Either a b -> c) -> (a -> c, b -> c)
It’s always nice to see that I havn’t learned the elementary power calculation rules for nothing :-)
I want to point out a quick categorical way of proving this (and almost all the other "arithmetic" laws follow similarly.) This is just continuity of right adjoints. The interesting thing is the adjunction, one that is commonly neglected in discussions of Cartesian closed categories. A^- is a function C^{op} -> C and it is adjoint to itself on the right, i.e. (A^-)^{op} -| A^-. As an isomorphism of hom functors that is, Hom(=,A^-) ~ Hom(-,A^=) or in Haskell notation there is an isomorphism flip :: (a -> b -> c) -> (b -> a -> c) (it is it's own inverse.) This is induced by the swap operation on pairs and is why for enriched categories usually they talk about -symmetric- monoidally closed categories. Symmetric monoidally closed categories validate all the arithmetic laws as well. So B+C is BxC in the opposite category and so A^- takes (BxC)^op to A^B x A^C. And that's not all, every adjunction gives rise to a monad namely, A^(A^-) or in Haskell notation (b -> a) -> a and indeed if you work out the details this is the continuation monad.