by *Tom Ellis* on **30th September 2012**

`Category`

and lenses`Category`

While reading Edward Kmett’s blog post on Mirrored Lenses I was struck by his observation that “By far their nicest property is that you can compose them using just (.) and id from the Prelude rather than having to go off and write a Category.” The (non-polymorphic van Laarhoven) `Lens`

data type is

`type Lens a b = forall f. Functor f => (b -> f b) -> a -> f a`

and to compose them you just use `(.) :: (b -> c) -> (a -> b) -> (a -> c)`

specialised to

`((b -> f b) -> (c -> f c)) -> ((a -> f a) -> (b -> f b)) -> ((a -> f a) -> (c -> f c))`

This made me wonder whether you can do a similar thing for `Category`

itself. The answer is yes! For any `Category k`

there is an embedding of `k`

into the category of Haskell functions that preserves the category structure:

```
{-# LANGUAGE Rank2Types #-}
import Prelude hiding ((.), id)
import Control.Category
embed :: Category k => k a b -> (forall r. k r a -> k r b)
embed f = (f .)
recover :: Category k => (forall r. k r a -> k r b) -> k a b
recover f = f id
```

`embed`

turns `f :: k a b`

into the function “post-compose with `f`

”. When we have “post-compose with `f`

” we can of course recover it by post-composing `id`

with `f`

!

`(recover . embed) f = in_ (f .) = f . id = f`

Notice that `embed`

does indeed preserve the `Category`

structure

```
embed id = (id .) = id
(embed f) . (embed g) = (f .) . (g .) = (f . g .) = embed (f . g)
```

so there’s an alternative representation of `Category`

instances that just needs `(.)`

and `id`

from the `Prelude`

!

Be careful though: not all `forall r. k r a -> k r b`

arise from a `k a b`

.

For the technically minded, fixing `b`

and mapping `a`

to `k a b`

gives a contravariant functor (not a `Functor`

!) from `k`

to Hask. Call this functor `k`

– `b`

. The Yoneda embedding gives us a correspondence between `k a b`

and natural transformations from `k`

– `a`

to `k`

– `b`

. Then the value of type `(forall r. k r a -> k r b)`

that `embed`

returns is always a natural transformation, but in much the same way that Dan Doel presented recently, not *all* values of that type need be natural transformations. The counterexamples to naturality here are thus exactly the complement of the image of `embed`

. I haven’t thought about explicit examples. Please tell me if you have thought of one.

There is an application of the Yoneda embedding to lenses themselves! An equivalent definition of `Lens`

is

`type Lens a b = (a -> b, a -> b -> a)`

the Yoneda embedding suggests rewriting this as

`type Lens a b = forall r. (r -> a, r -> a -> r) -> (r -> b, r -> b -> r)`

This gives another way of composing lenses using Prelude. However I cannot see how to make these lenses polymorphic and the composition is the opposite way round from what we might expect. The contravariant Yoneda embedding is better

`type Lens a b = forall r. (b -> r, b -> r -> b) -> (a -> r, a -> r -> a)`

because it allows

`type Lens a b a' b' = forall r. (b -> r, b -> r -> b') -> (a -> r, a -> r -> a')`

but here I don’t see how to avoid using `undefined`

to extract the getter and setter.

The contravariant embedding suggests some connection between `Functor f => a -> f a`

and `(a -> r, a -> r -> a)`

, and more generally between `Functor f => (a -> f a')`

and `(a -> r, a -> r -> a')`

. I can’t see what this should be though.