Jaguarpaw Blog - Category and lenses

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!

A technicality

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.

Lenses

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.

Functor

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.