[Haskell-cafe] adjunction of product and exponentiation
Jonathan Cast
jonathanccast at fastmail.fm
Wed Aug 6 17:32:32 EDT 2008
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
More information about the Haskell-Cafe
mailing list