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\\).

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\\).