In the previous post I explored the application of the Yoneda lemma in the functor category to derive some results from the Haskell lens library. In particular I derived the profunctor representation of isos. There is one more trick that is used in the lens library: combining the Yoneda lemma with adjunctions. Jaskelioff and O’Connor used this trick in the context of free/forgetful adjunctions, but it can be easily generalized to any pair of adjoint higher order functors.

## Adjunctions

An adjunction between two functors, `L`

and `R`

(left and right functor) is a natural isomorphism between hom-sets:

C(L d, c) ≅ D(d, R c)

The left functor `L`

goes from the category *D* to *C*, and the right functor `R`

goes in the opposite direction. Formally, having an adjunction allows us to shift the action of the functor from one end of the hom-set to the other. The shortcut notation for an adjunction is `L ⊣ R`

.

Since adjunctions can be defined for arbitrary categories, they will also work between functor categories. In that case objects are functors and hom-sets are sets of natural transformations. For instance, Let’s consider an adjunction between two higher order functors:

ρ :: [C, C'] -> [D, D'] λ :: [D, D'] -> [C, C']

Here, `[C, C']`

is a category of functors between two categories *C* and *C’*, `[D, D']`

is a category of functors between *D* and *D’*, and `ρ`

maps functors (and natural transformations) between these two categories. `λ`

goes in the opposite direction. The adjunction `λ ⊣ ρ`

is expressed as a natural isomorphism between sets of natural transformations:

[C, C'](λ g, h) ≅ [D, D'](g, ρ h)

The two objects in functor categories are themselves functors:

h :: C -> C' g :: D -> D'

Here’s the same adjunction written using ends:

∫_{x∈C}C'((λ g) x, h x) ≅ ∫_{y∈D}D'(g y, (ρ h) y)

The end notation is easily translatable to Haskell. The end corresponds to a universal quantifier `forall`

, and hom-sets become function types:

forall x. (lambda g) x -> h x ≅ forall y. g y -> (rho h) y

Since `lambda`

and `rho`

act on functors, they have kinds `(*->*)->(*->*)`

.

## Yoneda with Adjunctions

Let’s recall the formula for the Yoneda embedding of the functor category:

∫_{f}Set(∫_{x}D(g x, f x), ∫_{y}D(h y, f y)) ≅ ∫_{z}D(h z, g z)

Here, `g`

, `h`

, and `f`

, are functors — objects in the functor category `[C, D]`

. The ends represent natural transformations — morphisms in the functor category. The end over `f`

is a higher order natural transformation.

Since `g`

and `h`

are arbitrary, let’s replace them with the results of the action of some higher order functors, `λ g`

and `λ' h`

. The idea is that `λ`

and `λ'`

are left halves of some higher order adjunctions.

∫_{f}Set(∫_{x}D'((λ g) x, f x), ∫_{y}D'((λ' h) y, f y)) ≅ ∫_{z}D'((λ' h) z, (λ g) z)

The right halves of these adjunctions are, respectively, `ρ`

and `ρ'`

.

λ ⊣ ρ λ' ⊣ ρ'

Let’s apply these adjunctions inside the hom-sets:

∫_{f}Set(∫_{x}D(g x, (ρ f) x), ∫_{y}D(h y, (ρ' f) y)) ≅ ∫_{z}D(h z, (ρ' (λ g)) z)

Let’s focus our attention on the category of sets. If we replace *D* with **Set**, we can pick `g`

and `h`

to be hom-functors (which are the simplest representable functors) parameterized by some arbitrary objects `b`

and `t`

:

g = C(b, -) h = C(t, -)

We get:

∫_{f}Set(∫_{x}Set(C(b, x), (ρ f) x), ∫_{y}Set(C(t, y), (ρ' f) y) ≅ ∫_{z}Set(C(t, z), (ρ' (λ C(b, -))) z)

Remember, hom-functors behave like Dirac delta functions under the integration sign. That is to say, we can use the Yoneda lemma to “integrate” over `x`

, `y`

, and `z`

:

∫_{f}Set((ρ f) b, (ρ' f) t) ≅ (ρ' (λ C(b, -))) t

We are now free to pick a pair of adjoint higher order functors to suit our goal. Here’s one such choice for `ρ`

: the functor that maps a functor `f`

(an endofunctor in *C*) to a set of morphisms from some fixed object `a`

to `f`

acting on another object. This is an operation that lifts a functor to a profunctor. In Haskell it’s defined as `UpStar`

. This higher-order functor is parameterized by the choice of the object `a`

in *C*:

κ_{a}f = C(a, f -)

It can also be written in terms of the exponential object:

κ_{a}f = (f -)^{a}

This functor has an obvious left adjoint:

λ_{a}g = a × g -

This follows from the standard adjunction between the product and the exponential.

Our pick for `ρ'`

is the same functor but taken at a different carrier, `s`

:

ρ' = κ_{s}

With those choices, the left side of the identity

∫_{f}Set((ρ f) b, (ρ' f) t) ≅ (ρ' (λ C(b, -))) t

becomes:

∫_{f}Set(C(a, f b), C(s, f t))

This is the categorical version of the van Laarhoven lens.

Let’s now evaluate the right hand side. First we apply `λ`

to the hom-functor _{a}`C(b, -)`

to get:

λ_{a}C(b, -) = a × C(b, -)

The action of `ρ'`

produces the result:

C(s, (a × C(b, t)))

This, in turn, is the categorical version of the getter/setter representation of the lens.

## Translation

In Haskell, our formula derived from the higher-order Yoneda lemma with the adjoint pair:

∫_{f}Set((ρ f) b, (ρ' f) t) ≅ (ρ' (λ C(b, -))) t

takes the form:

forall f. Functor f => (rho f) b -> (rho' f) t ≅ (rho' (lambda ((->)b))) t

With our choice for `ρ`

as the up-star functor:

rho f = a -> f - rho' f = s -> f -

or, in proper Haskell:

type Rho a f b = a -> f b type Rho' s f t = s -> f t

we get:

forall f. Functor f => (a -> f b) -> (s -> f t) ≅ (rho' (lambda ((->)b))) t

To get the `λ`

, we plug our `ρ`

into the adjunction formula. We get:

forall x. (lambda g) x -> h x ≅ forall x. g x -> a -> h x

which has the obvious solution:

lambda g = (a, g -)

or, in proper Haskell,

type Lambda a g x = (a, g x)

Indeed, with the currying and flipping of arguments, we get the adjunction:

forall x. (a, g x) -> h x ≅ forall x. g x -> a -> h x

Now let’s evaluate the right hand side:

(rho' (lambda ((->) b))) t

We start with:

lambda (b -> -) = (a, b -> -)

The action of `rho'`

gives us:

rho' (a, b -> -) = s -> (a, b -> -)

Altogether:

(rho' (lambda ((->) b))) t = s -> (a, b -> t)

So the right hand side is just the getter/setter pair:

(s -> a, s -> b -> t)

The final result is the well known van Laarhoven representation of the lens:

forall f. Functor f => (a -> f b) -> (s -> f t) ≅ (s -> a, s -> b -> t)

This is not a new result, but I like the elegance of this derivation — especially the role played by the exponential adjunction and the lifting of a functor to a profunctor. This formulation has the additional advantage of being generalizable towards the profunctor formulation of lenses.