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 λa to the hom-functor 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.