[Haskell-cafe] adjunction of product and exponentiation

[Jonathan Cast]

On Wed, 2008-08-06 at 13:56 -0700, Jason Dusek wrote:
> The problem as stated is to find the unit for the adjunction:
> 
>     ((- x A), (-)^A x A)
> 
>   The latter functor takes an arrow f to (f . -) x id_A and does
>   the obvious thing for objects. The co-unit diagram is given
>   as:
> 
>             B^A x A ---- eval_AB ----> B
>                ^                       ^
>                |                       |
>                |                       |
>          curry(g) x id_A               g : C x A -> B
>                |                       |
>                |                       |
>                |                       |
>              C x A --------------------+
> 
>   This diagram is somewhat puzzling, because it seems the second
>   functor has turned into (-)^A ! Continuing in with that, we
>   get a unit diagram like this:
> 
>                C ---- magic ----> (C x A)^A
>                |                     |
>                |                     |
>                |                     |
>             curry(g)              (g . -)
>                |                     |
>                |                     |
>                |                     v
>                +------------------> B^A
> 
>   So what is the magic? It is an arrow that takes a C to an
>   arrow that takes an A and makes the product C x A. I want to
>   write curry(C x A) but that is ridiculous looking. What's the
>   right notation for this thing?

It's a curried pairing operator.  Haskell calls it (,); it might also be
called pair.  It is also, of course, equal to curry(id), so if you write
identity arrows as the corresponding objects then curry(C x A) is
perfectly reasonable.

(This function is rather fundamental, meaning its main purpose is to
justify a move that, 99% of the time it's made, is made without any
comment at all.  Spelling it out /is/ ridiculous, in the same sense that
explicitly invoking modus ponens in your proofs is ridiculous.  Unless
you're doing low-level formal proof theory, of course.)

jcc