[Haskell-cafe] Origins of '$'

[Derek Elkins]

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.