Puzzle 168: For a programmer the most important adjunction is the one between product and function type. We call it currying. It's an adjunction between two endofunctors: \$$F\$$ takes takes the set \$$a\$$ and "multiplies" it by some fixed set \$$c\$$ (takes cartesian product). The hom-set \$$C(F a, b)\$$ is a set of functions from a product \$$(a \times c)\$$ to \$$b\$$. These functions are in one-to-one correspondence with functions that take \$$a\$$ as an argument and return a function from \$$c\$$ to \$$b\$$. Therefore, the second functor \$$G\$$ takes a set \$$b\$$ and produces a function type \$$c \to b\$$, a.k.a, the exponential \$$b^c\$$

The adjunction \$$\alpha_{a b}\$$ is called curry:

curry :: ((a, c) -> b) -> (a ->(c -> b))

Naturality condition involves two functions, f :: a' -> a and g :: b -> b'. We have to figure out how \$$F\$$ acts of \$$f\$$ and how \$$G\$$ acts of \$$g\$$.

The product is a bifunctor, meaning it can lift a pair of functions at once. In Haskell this is done by a function called bimap:

bimap :: (a -> a') -> (b -> b') -> (a, b) -> (a', b')

Here, we want to lift one function, so we'll apply bimap to f and the identity function id (this is \$$id_c\$$). The left hand side of the naturality condition becomes:

p1 :: (a' -> a) -> (b -> b') -> ((a, c) -> b) -> (a' -> (c -> b'))

p1 f g h = curry (g . h . bimap f id)

The lifting of \$$g\$$ by functor \$$G\$$ acts on functions from the fixed \$$c\$$ to some \$$b\$$ simply by postcomposing \$$g\$$. This postcomposition is expressed as (g . ). The right hand side of the naturality condition becomes:

p2 :: (a' -> a) -> (b -> b') -> ((a, c) -> b) -> (a' -> (c -> b'))

p2 f g h = (g . ) . curry h . f

In words: You get the same result if you:

(a) take a function \$$h\$$ of two arguments, precompose it with \$$(f \times id)\$$, postcompose with \$$g\$$, and curry the result; or

(b) first curry \$$h\$$ then precompose the resulting function with \$$f\$$ and postcompose its result with \$$g\$$.