### Lens

The connection between the Haskell lens library and category theory is a constant source of amazement to me. The most interesting part is that lenses are formulated in terms of higher order functions that are polymorphic in functors (or, more generally, profunctors). Consider, for instance, this definition:

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

In Haskell, saying that a function is polymorphic in functors, which form a class parameterized by type constructors of the kind `*->*` (or `*->*->*`, in the case of profunctors) and supporting a special method called `fmap` (or `dimap`, respectively) is rather mind-boggling.

In category theory, on the other hand, functors are standard fare. You can form categories of functors. The properties of such categories are described by pretty much the same machinery as those of any other category.

In particular, one of the most important theorems of category theory, the Yoneda lemma, works in the category of functors out of the box. I have previously shown how to employ the Yoneda lemma to derive the representation for Haskell lenses (see my original blog post and, independently, this paper by Jaskelioff and O’Connor — or a more recent expanded post). Continuing with this program, I’m going to show how to use the Yoneda lemma with profunctors. But let’s start with the basics.

By the way, if you feel intimidated by mathematical notation, don’t worry, I have provided a translation to Haskell. However, math notation is often more succinct and almost always more general. I guess, the same ideas could be expressed using C++ templates, but it would look like an incomprehensible mess.

## Functor Categories

Functors between any two given categories C and D can themselves be organized into a category, which is often called `[C, D]` or `DC`. The objects in that category are functors, and the morphisms are natural transformations. Given two functors `f` and `g`, the hom-set between them can be either called

`Nat(f, g)`

or

`[C, D](f, g)`

depending how much information you want to expose. (For simplicity, I’ll assume that the categories are small, so that the “sets” or natural transformations are sets indeed.)

What’s interesting is that, since functor categories are just categories, we can have functors going between them. We sometimes call them higher order functors. We can also have higher order functors going from a functor category to a regular category, in particular to the category of sets, Set. An example of such a functor is a hom-functor in a functor category. You construct this functor (also called a representable functor) when you fix one end of the hom-set and vary the other. In any category, the mapping:

`x -> C(a, x)`

is a functor from C to Set. We often use a shorthand notation for this functor:

`C(a, -)`

If we replace C by a functor category then, for a fixed functor `g`, the mapping:

`f -> [C, D](g, f)`

is a higher order functor. It maps `f` to a set of natural transformations — itself an object in Set.

Representable functors play an important role in the Yoneda lemma. Take the set of natural transformations from a representable functor in C to any functor `f` that goes from C to Set. This set is in one-to-one correspondence with the set of values of this functor at the object `a`:

`[C, Set](C(a, -), f) ≅ f a`

This correspondence is an isomorphism, which is natural both in `a` and `f`.

The set of natural transformations between two functors `f` and `g` can also be expressed as an end:

`[C, D](f, g) = ∫x∈C D(f x, g x)`

The end notation is sometimes more convenient because it makes the object `x` (the “integration variable”) explicit. The Yoneda lemma, in this notation, becomes:

`∫x∈C Set(C(a, x), f x) ≅ f a`

If you’re familiar with distributions, this formula will immediately resonate with you — it looks like the definition of the Dirac delta function:

`∫ dx δ(a - x) f(x) ≅ f(a)`

We can apply the Yoneda lemma to a functor category to get:

`Nat([C, D](g, -), φ) ≅ φ g`

or, in the end notation,

`∫f Set(∫x D(g x, f x), φ f) ≅ φ g`

Here, the “integration variable” `f` is itself a functor from C to D, and so is `g`; `φ`, however, is a higher order functor. It maps functors from `[C, D]` to sets from Set. The natural transformations in this formula are higher order natural transformations between higher order functors.

Furthermore, if we substitute for `φ` another instance of the representable functor, `[C, D](h, -)`, we get the formula for the higher order Yoneda embedding:

`Nat([C, D](g, -), [C, D](h, -)) ≅ [C, D](h, g)`

which reduces higher order natural transformations to lower order natural transformations. Notice the inversion of `g` and `h` on the right hand side.

Using the end notation, this becomes:

```∫f Set(∫x D(g x, f x), ∫y D(h y, f y))
≅ ∫z D(h z, g z)```

We can further specialize this formula by replacing D with Set. We can then choose both functors to be hom-functors (for some fixed `a` and `b`):

```g = C(a, -)
h = C(b, -)```

We get:

```∫f Set(∫x Set(C(a, x), f x), ∫y Set(C(b, y), f y))
≅ ∫z Set(C(b, z), C(a, z))```

This can be simplified by applying the Yoneda lemma to the internal ends (“integrating” over x, y, and z) to get:

`∫f Set(f a, f b) ≅ C(a, b)`

This simple formula has some interesting possibilities that I will explore later.

## Translation

All this might be easier to digest for programmers when translated to Haskell. Natural transformations are polymorphic functions:

`forall x. f x -> g x`

Here, `f` and `g` are arbitrary Haskell `Functor`s. It’s a straightforward translation of the end formula:

`∫x∈Set Set(f x, g x)`

where the end is replaced by the universal quantifier, and the hom-set in Set by a function type. I have deliberately used Set rather than Hask as the category of Haskell types, because I’m not going to pretend that I care about non-termination.

A higher order functor of the kind we are interested in is a mapping from functors to types, which could be defined as follows:

```class HFunctor (phi :: (* -> *) -> *) where
hfmap :: (forall a. f a -> g a) -> (phi f -> phi g)```

The higher order hom-functor is defined as:

`newtype HHom f g = HHom (forall a. f a -> g a)`

Indeed, it’s easy to define `hfmap` for it:

```instance HFunctor (HHom f) where
hfmap nat (HHom nat') = HHom (nat . nat')```

The types give it away:

```nat    :: forall a. g a -> h a
nat'   :: forall a. f a -> g a
result :: HHom (forall a. f a -> h a)```

Higher order natural transformations between such functors will have the signature:

```type HNat (phi :: (* -> *) -> *) (psi :: (* -> *) -> *) =
forall f. Functor f => phi f -> psi f```

The standard Yoneda lemma establishes the isomorphism between `f a` and the following higher order polymorphic function:

`forall x. (a -> x) -> f x  ≅  f a`

The Yoneda lemma for higher order functors is the equivalence between `φ g` and:

`forall f. Functor f => forall x. (g x -> f x) -> φ f  ≅  φ g`

Compare this again with:

`∫f Set(∫x Set(g x, f x), φ f) ≅ φ g`

The higher order Yoneda embedding takes the form of the equivalence between:

`forall f. Functor f => forall x. (g x -> f x) -> forall y. (h y -> f y)`

and

`forall z. h z -> g z`

The earlier result of the double application of the Yoneda lemma:

`∫f Set(f a, f b) ≅ C(a, b)`

translates to:

`forall f. Functor f => f a -> f b ≅ a -> b`

One direction of this equivalence simply reiterates the definition of a functor: a function `a->b` can be lifted to any functor. The other direction is a little more interesting. Given two types, `a` and `b`, if there is a function from `f a` to `f b` for any functor `f`, than there is a direct function from `a` to `b`. In Set, where there are functions between any two types, with the exception of `a->Void`, this is not a big surprise.

But there are other categories embedded in Set, and the same categorical formula will lead to more interesting translations. In particular, think of categories where the hom-set is not equivalent to a simple function type with trivial composition. A good example is the basic formulation of lens as the getter/setter pair, or a function of type:

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

Such functions don’t compose naturally, but their functor-polymorphic representations do.

## Profunctors

You’ve seen the reusability of categorical constructs in action. We can have functors operate on functors, and natural transformations that work between higher order functors. The same Yoneda lemma works as well in the category of types and functions, as in the category of functors and natural transformations. From that perspective, a profunctor is just a special case of a functor. Given two categories C and D, a profunctor is a functor:

`Cop × D -> Set`

It’s a map from a product category to Set. Because the first component of the product is the opposite category (all morphisms reversed), this functor is contravariant in the first argument.

Let’s translate this definition to Haskell. We substitute all three categories with the same category of types and functions, which is essentially Set (remember, we ignore the bottom values). So a profunctor is a functor from Setop×Set to Set. It’s a mapping of types — a two-argument type constructor `p`  — and a mapping of morphisms. A morphism in Setop×Set is a pair of functions going between pairs `(a, b)` and `(s, t)`. Because of contravariance, the first function goes in the opposite direction:

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

A profunctor lifts this pair to a single function:

`p a b -> p s t`

The lifting is done by the function `dimap`, which is usually written in the curried form:

```class Profunctor p where
dimap :: (s -> a) -> (b -> t) -> p a b -> p s t```

All said and done, a profunctor is still a functor, so we can reuse all the machinery of functor calculus, including all versions of the Yoneda lemma.

`[Cop×D, Set]((Cop×D)(<c, d>, -), p) ≅ p <c, d>`

or, in the end notation:

`∫<x, y>∈Cop×D Set((Cop×D)(<c, d>, <x, y>), p <x, y>) ≅ p <c, d>`

Here, `p` is the profunctor operating on pairs of objects, such as `<c, d>`. A hom-set in the product category Cop×D goes between two such pairs:

`(Cop×D)(<c, d>, <x, y>)`

Here’s the straightforward translation to Haskell:

`forall x y. (x -> c) -> (d -> y) -> p x y ≅ p c d`

Notice the customary currying and the reversal of source with target in the first function argument due to contravariance.

Since profunctors are just functors, they form a functor category:

`[Cop×D, Set]`

(not to be confused with Prof, the profunctor category, where profunctors serve as morphisms rather than objects):

We can easily rewrite the higher-order Yoneda lemma replacing functors with profunctors:

`∫p Set(∫<x, y> Set(q <x, y>, p <x, y>), π p) ≅ π q`

And this is what it looks like in Haskell:

`forall p. Profunctor p => (forall x y. q x y -> p x y) -> pi p ≅ pi q`

Here, π is a higher order functor acting on profunctors, with values in Set. In Haskell it’s defined by a type class:

```class HFunProf (pi :: (* -> * -> *) -> *) where
fhpmap :: (forall a b. p a b -> q a b) -> (pi p -> pi q)```

Natural transformations between such functors have the type:

```type HNatProf (pi :: (* -> * -> *) -> *) (rho :: (* -> * -> *) -> *) =
forall p. Profunctor p => pi p -> rho p```

Notice that we are now defining functions that are polymorphic in profunctors. This is getting us closer to the profunctor formulation of the lens library, in particular to prisms and isos.

## Understanding Isos

An iso is a perfect example of a data structure straddling the gap between lenses and prisms. Its first order definition is simple:

`type Iso s t a b = (s -> a, b -> t)`

The name derives from isomorphism, which is a special case of an iso (I think a cuter name for an iso would be `Mirror`). The crucial observation is that this is nothing but the type corresponding to a hom-set in the product category Setop×Set:

`(Setop×Set)(<a b>, <s t>)`

We know how to compose such morphisms:

```compIso :: Iso s t a b -> Iso a b u v -> Iso s t u v
(f1, g1) `compIso` (f2, g2) = (f2 . f1, g1 . g2)```

but it’s not as straightforward as function composition. Fortunately, there is a higher order representation of isos, which composes using simple function composition. The trick is to make it profunctor-polymorphic:

`type Iso s t a b = forall p. Profunctor p => p a b -> p s t`

Why are the two definitions isomorphic? There is a standard argument based on parametricity, which I will skip, because there is a better explanation.

Recall the earlier result of applying the Yoneda lemma to the functor category:

`forall f. Functor f => f a -> f b ≅ a -> b`

The similarity is striking, isn’t it? That’s because, the categorical formula for both identities is the same:

`∫f Set(f a, f b) ≅ C(a, b)`

All we need is to replace C with Cop×D and rewrite it in terms of pairs of objects:

`∫p Set(p <a b>, p <s t>) ≅ (Cop×D)(<a b>, <s t>)`

But that’s exactly what we need:

`forall p. Profunctor p => p a b -> p s t  ≅ (s -> a, b -> t)`

The immediate advantage of the profunctor-polymorphic representation is that you can compose two isos using straightforward function composition. Instead of using `compIso`, we can use the dot:

```p :: Iso s t a b
q :: Iso a b u v
r :: Iso s t u v
r = p . q```

Of course, the full power of lenses is in the ability to compose (and type-check) combinations of different elements of the library.

Note: The definition of `Iso` in the lens library involves a functor `f`:

```type Iso s t a b = forall p f. (Profunctor p, Functor f) =>
p a (f b) -> p s (f t)```

This functor can be absorbed into the definition of the profunctor `p` without any loss of generality.

Next: Combining adjunctions with the Yoneda lemma.

## Acknowledgments

I’m grateful to Gershom Bazerman and Gabor Greif for useful comments and to André van Meulebrouck for checking the grammar and spelling.

Lenses are a fascinating subject. Edward Kmett’s lens library is an indispensable tool in every Haskell programmer’s toolbox. I set out to write this blog post with the goal of describing some new insights into their categorical interpretation, but then I started reviewing all the different formulations of lenses and their relations to each other. So this post turned into a little summary of the theoretical underpinning of lenses.

If you’re already familiar with lenses, you may skip directly to the last section, which describes some new results.

# The Data-Centric Picture

Lenses start as a very simple idea: an accessor/mutator or getter/setter pair — something familiar to every C++, Java, or C# programmer. In Haskell they can be described as two functions:

```get :: s -> a
set :: s -> a -> s```

Given an object of type `s`, the first function produces the value of the object’s sub-component of type `a` — which is the focus of the particular lens. The second function takes the object together with a new value for the sub-component, and produces a modified object.

A simple example is a lens that focuses on the first component of a pair:

```get :: (a, a') -> a
get (x, y) = x```
```set :: (a, a') -> a -> (a, a')
set (x, y) x' = (x', y)```

In Haskell we can go even further and define a lens for a polymorphic object, in which the setter changes not only the value of the sub-component, but also its type. This will, of course, also change the type of the resulting object. So, in general we have:

```get :: s -> a
set :: s -> b -> t```

Our pair example doesn’t change much on the surface:

```get :: (a, a') -> a
get (x, y) = x```
```set :: (a, a') -> b -> (b, a')
set (x, y) x' = (x', y)```

The difference is that the type of `x'` can now be different from the type of `x`. The first component of the pair is of type `a` before the update, and of type `b` (the same as that of `x'`) after it. This way we can turn a pair of, say, `(Int, Bool)` to a pair of `(String, Bool)`.

We can always go back to the monomorphic version of the lens by choosing `b` equal to `a` and `t` equal to `s`.

Not every pair of functions like these constitutes a lens. A lens has to obey a few laws (first formulated by Pierce in the database context). In particular, if you `get` a component after you `set` it, you should get back the value you just put in:

`get . set s = id`

If you call `set` with the value you obtained from `get`, you should get back the unchanged object:

`set s (get s) = s`

Finally, a `set` should overwrite the result of a previous `set`:

`set (set s a) b = set s b`

So this is what I would call a “classical” lens. It’s formulated in easy to understand programming terms.

# The Algebraic Picture

It was Russell O’Connor who noticed that when you refactor the common element from the getter/setter pair, you get an interesting algebraic structure. Instead of writing the lens as two functions, we can write it as one function returning a pair:

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

Think of this as factoring out the “this” pointer in OO and returning the interface. Of course, the difference is that, in functional programming, the setter does not mutate the original — it returns a new version of the object instead.

Let’s for a moment concentrate on the monomorphic version of the lens — one in which `a` is the same as `b`, and `s` is the same as `t`. We can define a data structure:

`data Store a s = Store a (a -> s)`

and rewrite the lens as:

`s -> Store a s`

For instance, our first-component-of-a-pair lens will take the form:

```fstl :: (a, b) -> Store a (a, b)
fstl (x, y) = Store x (\x' -> (x', y))```

The first observation is that, for any `a`, `Store a` is a functor:

```instance Functor (Store a) where
fmap f (Store x h) = Store x (f . h)```

It’s a well-known fact that you can define algebras for a functor, so-called F-algebras. An algebra for a functor `f` consists of a type `s` called the carrier type and a function called the action:

`alg :: f s -> s`

This is almost like a lens (with `f` replaced by `Store a`), except that the arrow goes the wrong way. Not to worry: there is a dual notion called a coalgebra. It consists of a carrier type `s` and a function:

`coalg :: s -> f s`

Substitute `Store a` for `f` and you see that a lens is nothing but a coalgebra for this functor. This is not saying much — we have just given a mathematical name to a programming construct, no big deal. Except that `Store a` is more than a functor — it’s also a comonad.

You know that you can define a monad in Haskell using `return` and `join`. Reverse the arrows on those two, and you get `extract` and `duplicate`, the two functions that define a comonad.

```class (Functor w) => Comonad w where
extract :: w a -> a
duplicate :: w a -> w (w a)```

Here, `w` is a type constructor that is also a functor.

This is how you can implement those two functions for `Store a`:

```instance Comonad (Store a) where
-- extract :: Store a s -> s
extract (Store x h) = h x
-- duplicate :: Store a s -> Store a (Store a s)
duplicate (Store x h) = Store x (\y -> Store y h)```

So now we have two structures: a comonad `w` and a coalgebra:

`type Coalgebra w s = s -> w s`

A lens is a special case of this coalgebra where `w` is `Store a`.

Every time you have two structures, you may legitimately ask the question: Are they compatible? Just by looking at types, you may figure out some obvious compatibility conditions. In particular, since they go the opposite way, it would make sense for `extract` to undo the action of `coalg`:

```coalg :: Coalgebra w s
extract . coalg = id```

Also, duplicating the result of `coalg` should be the same as applying `coalg` twice (the second time lifted by `fmap`):

`fmap coalg . coalg = duplicate . coalg`

If these two conditions are satisfied, we call `coalg` a comonad coalgebra.

And here’s the clencher:

These two conditions when applied to the `Store a` comonad are equivalent to our earlier lens laws.

Let’s see how it works. First we’ll express the result of our lens coalgebra acting on some object `s` in terms of `get` and `set` (curried `set s` is a function `a->s`):

`coalg s = Store (get s) (set s)`

The first condition `extract . coalg = id` immediately gives us the law:

`set s (get s) = s`

When we act with `duplicate` on `coalg s`, we get:

`Store (get s) (\y -> Store y (set s))`

On the other hand, when we `fmap` our `coalg` over `coalg s`, we get:

`Store (get s) ((\s' -> Store (get s') (set s')) . set s)`

Two functions — the second components of the `Store` objects in those equations — must be equal when acting on any `a`. The first function produces:

`Store a (set s)`

In the second one, we first apply `set s` to `a` to get `set s a`, which we then pass to the lambda to get:

`Store (get (set s a)) (set (set s a))`

This reproduces the other two (monomorphic) lens laws:

`get (set s a) = a`

and

`set (set s a) = set s`

This algebraic construction can be extended to type-changing lenses by replacing `Store` with its indexed version:

`data IStore a b t = IStore a (b -> t)`

and the comonad with its indexed counterpart. The indexed store is also called `Context` in the lens parlance, and an indexed comonad is also called a parametrized comonad.

So what’s an indexed comonad? Let’s start with an indexed functor. It’s a type constructor that takes three types, `a`, `b`, and `s`, and is a functor in the third argument:

```class IxFunctor f where
imap :: (s -> t) -> f a b s -> f a b t```

`IStore` is obviously an indexed functor:

```instance IxFunctor IStore where
-- imap :: (s -> t) -> IStore a b s -> IStore a b t
imap f (IStore x h) = IStore x (f . h)```

An indexed comonad has the indexed versions of `extract` and `duplicate`:

```class IxComonad w where
iextract :: w a a t -> t
iduplicate :: w a b t -> w a j (w j b t)```

Notice that `iextract` is “diagonal” in the index types, whereas the double application of `w` shares one index, `j`, between the two applications. This plays very well with the unit and multiplication interpretation of a monad — here it looks just like matrix multiplication (although we are dealing with a comonad rather than a monad).

It’s easy to see that the instantiation of the indexed comonad for `IStore` works the same way as the instantiation of the comonad for `Store`. The types just work out that way.

```instance IxComonad IStore where
-- iextract :: IStore a a t -> t
iextract (IStore a h) = h a
-- iduplicate :: IStore a b t -> IStore a c (IStore c b t)
iduplicate (IStore a h) = IStore a (\c -> IStore c h)```

There is also an indexed version of a comonad coalgebra, where the coalgebra is replaced by a family of mappings from some carrier type `s` to `w a b t`; with the type `t` determined by `s` together with the choice of of the indexes `a` and `b`:

`type ICoalg w s t a b = s -> w a b t`

The compatibility conditions that make it an (indexed) comonad coalgebra are almost identical to the standard compatibility conditions, except that we have to be careful about the index types. Here’s the first condition:

```icoalg_aa :: ICoalg w s t a a
iextract . icoalg_aa = id```

Let’s analyze the types. The inner part has the type:

`icoalg_aa :: s -> w a a t`

We apply `iextract` to it, which has the type:

`iextract :: w a a t -> t`

and get:

`iextract . icoalg_aa :: s -> t`

The right hand side of the condition has the type:

`id :: s -> s`

It follows that, for the diagonal components of `ICoalg w s t`, `t` must be equal to `s`. The diagonal part of `ICoalg w s t` is therefore a family of regular coalgebras.

As we have done with the monomorphic lens, we can express `(ICoalg IStore s t a b)`, when acting on `s`, in terms of `get` and `set`:

`icoalg_ab s = IStore (get s) (set s)`

But now `get s` is of type `a`, while `set s` if of the type `b -> t`. We can still apply `extract` to the diagonal term `IStore a a t` as required by the first compatibility condition. When equating the result to `id`, we recover the lens law:

`set s (get s) = s`

Similarly, it’s straightforward to see that the second compatibility condition:

```icoalg_bc :: ICoalg w s t b c
icoalg_ab :: ICoalg w s t a b
icoalg_ac :: ICoalg w s t a c
imap icoalg_bc . icoalg_ab = iduplicate . icoalg_ac```

is equivalent to the other two lens laws.

# The Parametric Picture

Despite being theoretically attractive, standard lenses were awkward to use and, in particular, to compose. The breakthrough came when Twan van Laarhoven realized that there is a higher-order representation for them that has very nice compositional properties. Composing lenses to focus on sub-objects of sub-objects turned into simple function composition.

Here’s Twan’s representation (generalized by Russell for the polymorphic case):

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

So a lens is a polymorphic higher order function with a twist. The twist is that it’s polymorphic with respect to a functor rather than a type.

You can think of it this way: the caller provides a function to modify a particular field of `s`, turning it from type `a` to `f b`. What the caller gets back is a function that transforms the whole of `s` to `f t`. The idea is that the lens knows how to reconstruct the object, while putting it under a functor `f` — if you tell it how to modify a field, also under this functor.

For instance, continuing with our example, here’s the van Laarhoven lens that focuses on the first component of a pair:

```vL :: Lens (a, c) (b, c) a b
vL h (x, x') = fmap (\y -> (y, x')) (h x)```

Here, `s` is `(a, c)` and `t` is `(b, c)`.

To see that the van Laarhoven representation is equivalent to the get/set one, let’s first change the order of arguments and pull `s` outside of the `forall` quantifier:

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

Here’s how you can read this definition: For a given `s`, if you give me a function from `a` to `f b`, I will produce a value of type `f t`. And I don’t care what functor you use!

What does it mean not to care about the functor? It means that the lens must be parametrically polymorphic in `f`. It can’t do case analysis on a functor. It must be implemented using the same formula for `f` being the list functor, or the `Maybe` functor, or the `Const` functor, etc. There’s only one thing all these functors have in common, and that’s the `fmap` function; so that’s what we are allowed to use in the implementation of the lens.

Now let’s think what we can do with a function `a -> f b` that we were given. There’s only one thing: apply it to some value of type `a`. So we must have access to a value of type `a`. The result of this application is some value of type `f b`, but we need to produce a value of the type `f t`. The only way to do it is to have a function of type `b->t` and sneak it under the functor using `fmap` (so here’s where the generic functor comes in). We conclude that the implementation of the function:

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

must be hiding a value of type `a` and a function `b->t`. But that’s exactly the contents of `IStore a b t`. Parametricity tells us that there is an `IStore` hiding inside the van Laarhoven lens. The lens is equivalent to:

`s -> IStore a b t`

In fact, with a clever choice of functors we can recover both `get` and `set` from the van Laarhoven representation.

First we select our functor to be `Const a`. Note that the parameter `a` is not the one over which the functor is defined. `Const a` takes a second parameter `b` over which it is functorial. And, even though it takes `b` as a type parameter, it doesn’t use it at all. Instead, like a magician, it palms an `a`, and then reveals it at the end of the trick.

```newtype Const a b = Const { getConst :: a }

instance Functor (Const a) where
-- fmap :: (s -> t) -> Const a s -> Const a t
fmap _ (Const a) = (Const a)```

The constructor `Const` happens to be a function

`Const :: a -> Const a b`

which has the required form to be the first argument to the lens:

`a -> f b`

When we apply the lens, let’s call it `vL`, to the function `Const`, we get another function:

`vL Const :: s -> Const a t`

We can apply this function to `s`, and then, in the final reveal, retrieve the value of `a` that was smuggled inside `Const a`:

`get vL s = getConst \$ vL Const s`

Similarly, we can recover `set` from the van Laarhoven lens using the `Identity` functor:

`newtype Identity a = Identity { runIdentity :: a }`

We define:

`set vL s x = runIdentity \$ vL (Identity . const x) s`

The beauty of the van Laarhoven representation is that it composes lenses using simple function composition. A lens takes a function and returns a function. This function can, in turn, be passed as the argument to another lens, and so on.

There’s an interesting twist to this kind of composition — the function composition operator in Haskell is the dot, just like the field accessor in OO languages like Java or C++; and the composition follows the same order as the composition of accessors in those languages. This was first observed by Conal Elliott in the context of semantic editor combinators.

Consider a lens that focuses on the `a` field inside some object `s`. It’s type is:

`Lens s t a b`

When given a function:

`h :: a -> f b`

it returns a function:

`h' :: s -> f t`

Now consider another lens that focuses on the `s` field inside some even bigger object `u`. It’s type is:

`Lens u w s t`

It expects a function of the type:

`g :: s -> f t`

We can pass the result of the first lens directly to the second lens to form a composite:

`Lens u w s t . Lens s t a b`

We get a lens that focuses on the `a` field of the object `s` that is the sub-object of the big object `u`. It works just like in Java, where you apply a dot to the result of a getter or a setter, to dig deeper into a subobject.

Not only do lenses compose using regular function composition, but we can also use the identity function as the identity lens. So lenses form a category. It’s time to have a serious look at category theory. Warning: Heavy math ahead!

# The Categorical Picture

I used parametricity arguments to justify the choice of the van Laarhoven representation for the lens. The lens function is supposed to have the same form for all functors `f`. Parametricity arguments have an operational feel to them, which is okay, but I feel like a solid categorical justification is more valuable than any symbol-shuffling argument. So I worked on it, and eventually came up with a derivation of the van Laarhoven representation using the Yoneda lemma. Apparently Russell O’Connor and Mauro Jaskelioff had similar feelings because they came up with the same result independently. We used the same approach, going through the `Store` functor and applying the Yoneda lemma twice, once in the functor category, and once in the Set category (see the Bibliography).

I would like to present the same result in a more general setting of the Yoneda embedding. It’s a direct consequence of the Yoneda lemma, and it states that any category can be embedded (fully and faithfully) in the category of functors from that category to Set.

Here’s how it works: Let’s fix some object `a` in some category C. For any object `x` in that category there is a hom-set `C(a, x)` of morphisms from `a` to `x`. A hom-set is a set — an object in the category Set of sets. So we have defined a mapping from C to Set that takes an `x` and maps it to the set `C(a, x)`. This mapping is called `C(a, _)`, with the underscore serving as a placeholder for the argument.

It’s easy to convince yourself that this mapping is in fact a functor from C to Set. Indeed, take any morphism `f` from `x` to `y`. We want to map this morphism to a function (a morphism in Set) that goes between `C(a, x)` and `C(a, y)`. Let’s define this lifted function component-wise: given any element `h` from `C(a, x)` we can map it to `f . h`. It’s just a composition of two morphisms from C. The resulting morphism is a member of `C(a, y)`. We have lifted a morphism `f` from C to Set thus establishing that `C(a, _)` is a functor.

Now consider two such functors, `C(a, _)` and `C(b, _)`. The Yoneda embedding theorem tells us that there is a one-to-one correspondence between the set of natural transformations between these two functors and the hom-set `C(b, a)`.

`Nat(C(a, _), C(b, _)) ≅ C(b, a)`

Notice the reversed order of `a` and `b` on the right-hand side.

Let’s rephrase what we have just seen. For every `a` in C, we can define a functor `C(a, _)` from C to Set. Such a functor is a member of the functor category `Fun(C, Set)`. So we have a mapping from C to the functor category `Fun(C, Set)`. Is this mapping a functor?

We have just seen that there is a mapping between morphisms in C and natural transformations in `Fun(C, Set)` — that’s the gist of the Yoneda embedding. But natural transformations are morphisms in the functor category. So we do have a functor from C to the functor category `Fun(C, Set)`. It maps objects to objects and morphisms to morphisms. It’s a contravariant functor, because of the reversal of `a` and `b`. Moreover, it maps the hom-sets in the two categories one-to-one, so it’s a fully faithful functor, and therefore it defines an embedding of categories. Every category C can be embedded in the functor category `Fun(C, Set)`. That’s called the Yoneda embedding.

There’s an interesting consequence of the Yoneda embedding: Every functor category can be embedded in its own functor category — just replace C with a functor category in the Yoneda embedding. Recall that functors between any two categories form a category. It’s a category in which objects are functors and morphisms are natural transformations. Yoneda embedding works for that category too, which means that a functor category can be embedded in a category of functors from that functor category to Set.

Let’s see what that means. We can fix one functor, say `R` and consider the hom-set from `R` to some arbitrary functor `f`. Since we are in a functor category, this hom-set is a set of natural transformations between the two functors, `Nat(R, f)`.

Now let’s pick another functor `S`. It also defines a set of natural transformations `Nat(S, f)`. We can keep picking functors and mapping them to sets (sets of natural transformations). In fact we know from the previous argument that this mapping is itself a functor. This time it’s a functor from a functor category to Set.

What does the Yoneda embedding tell us about any two such functors? That the set of natural transformations between them is isomorphic to the (reversed) hom-set. But this time hom-sets are sets of natural transformations. So we have:

`Nat(Nat(R, _), Nat(S, _)) ≅ Nat(S, R)`

All natural transformations in this formula are regular natural transformation except for the outer one, which is more interesting. You may recall that a natural transformation is a family of morphisms parameterized by objects. But in this case objects are functors, and morphisms are themselves natural transformations. So it’s a family of natural transformations parameterized by functors. Keep this in mind as we proceed.

To get a better feel of what’s happening, let’s translate this to Haskell. In Haskell we represent natural transformations as polymorphic functions. This makes sense, since a natural transformation is a family of morphisms (here functions) parameterized by objects (here types). So a member of `Nat(R, f)` can be represented as:

`forall x. R x -> f x`

Similarly, the second natural transformation in our formula turns into:

`forall y. S y -> f y`

As I said, the outer natural transformation in the Yoneda embedding is a family of natural transformations parameterized by a functor, so we get:

`forall f. Functor f => (forall x. R x -> f x) -> (forall y. S y -> f y)`

You can already see one element of the van Laarhoven representation: the quantification over a functor.

The right hand side of the Yoneda embedding is a natural transformation:

`forall z. S z -> R z`

The next step is to pick the appropriate functors for `R` and `S`. We’ll take `R` to be `IStore a b` and `S` to be `IStore s t`.

Let’s work on the first part:

`forall x. IStore a b x -> f x`

A function from `IStore a b x` is equivalent to a function of two arguments, one of them of type `a` and another of type `b->x`:

`forall x. a -> (b -> x) -> f x`

We can pull `a` out of `forall` to get:

`a -> (forall x. (b -> x) -> f x)`

If you squint a little, you recognize that the thing in parentheses is a natural transformation between the functor `C(b, _)` and `f`, where C is the category of Haskell types. We can now apply the Yoneda lemma, which says that this set of natural transformations is isomorphic to the set `f b`:

`forall x. (b -> x) -> f x ≅ f b`

We can apply the same transformation to the second part of our identity:

`forall y. (IStore s t y -> f y) ≅ s -> f t`

Taking it all together, we get:

```forall f. Functor f => (a -> f b) -> (s -> f t)
≅ forall z. IStore s t z -> IStore a b z```

Let’s now work on the right hand side:

```forall z. IStore s t z -> IStore a b z
≅ forall z. s -> (t -> z) -> IStore a b z```

Again, pulling `s` out of `forall` and applying the Yoneda lemma, we get:

`s -> IStore a b t`

But that’s just the standard representation of the lens:

`s -> IStore a b t ≅ (s -> a, s -> b -> t) = (get, set)`

Thus the Yoneda embedding of the functor category leads to the van Laarhoven representation of the lens:

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

This is all very satisfying, but you may wonder what’s so special about the `IStore` functor? The crucial step in the derivation of the van Laarhoven representation was the application of the Yoneda lemma to get this identity:

`forall x. IStore a b x -> f x ≅ a -> f b`

Let’s rewrite it in the more categorical language:

`Nat(IStore a b, f) ≅ C(a, f b)`

The set of natural transformations from the functor `IStore a b` to the functor `f` is isomorphic to the hom-set between `a` and `f b`. Any time you see an isomorphism of hom-sets (and remember that `Nat` is the hom-set in the functor category), you should be on the lookout for an adjunction. And indeed, we have an adjunction between two functors. One functor is defined as:

`a -> IStore a b`

It takes an object `a` in C and maps it to a functor `IStore a b` parameterized by some other object `b`. The other functor is:

`f -> f b`

It maps a functor, an object in the functor category, to an object in C. This functor is also parameterized by the same `b`. Since this is a flipped application, I’ll call it `Flapp`:

`newtype Flapp b f = Flapp (f b)`

So, for any `b`, the functor-valued functor `IStore _ b` is left adjoint to `Flapp b`. This is what makes `IStore` special.

As a side note: `IStore a b` is a covariant functor in `a` and a contravariant functor in `b`. However, `Store a` is not functorial in `a`, because `a` appears in both positive and negative position in its definition. So the adjunction trick doesn’t work for a simple (monomorphic) lens.

We can now turn the tables and use the adjunction to define the functor `IStore` in an arbitrary category (notice that the Yoneda lemma worked only for Set-valued functors). We just define a functor-valued functor `IStore` to be the left adjoint to `Flapp`, provided it exists.

`Nat(IStore a b, f) ≅ C(a, f b)`

Here, Nat is a set of natural transformations between endofunctors in C.

We can substitute the so defined functor into the Yoneda embedding formula we used earlier:

```Nat((Nat(IStore a b, f), Nat(IStore s t, f))
≅ Nat(IStore s t, IStore a b)```

We can now use the adjunction, rather than the Yoneda lemma, to eliminate some of the occurrences `IStore`:

```Nat(C(a, f b), C(s, f t))
≅ C(s, IStore a b t)```

This is slightly more general than the original van Laarhoven equivalence.

We can go even farther and reproduce the Jaskelioff and O’Connor trick of constraining the generic functor in the definition of the van Laarhoven lens to a pointed or applicative functor. This results in a multi-focus lens. In particular, if we use pointed functors, we get lenses with zero or one targets, so called affine lenses. Restricting the functors further to applicative leads to lenses with any number of targets, or traversals.

The trick is that any pointed or applicative functor can be stripped of the additional functionality and treated just like any other functor. This act of “forgetting” about `pure` and `<*>` may itself be considered a functor in the functor category. It’s called, appropriately, a forgetful functor. The left adjoint to a forgetful functor (if it exists) is called a free functor. It takes an arbitrary functor and creates a pointed functor by generating an artificial `pure`; or it creates an applicative functor by adding `<*>`. This adjunction is described by a natural isomorphism of hom-sets — in this case sets of natural transformations:

`Nat(S, U f) ≅ Nat(S*, f)`

Here, `U` is the forgetful functor, and `S*` is the free applicative/pointed version of the functor `S`. The functor `f` ranges across applicative (respectively, pointed) functors.

Now we can try to substitute the free version of `IStore` in the Yoneda embedding formula:

```Nat((Nat(IStore* a b, f), Nat(IStore* s t, f))
≅ Nat(IStore* s t, IStore* a b)```

The formula holds for any applicative (pointed) functor `f` and a set of natural transformations over such functors.

The first step is to use the forgetful/free adjunction:

```Nat((Nat(IStore a b, U f), Nat(IStore s t, U f))
≅ Nat(IStore s t, U IStore* a b)```

Then we can use our defining adjunction for `IStore` to get:

```Nat(C(a, U f b), C(s, U f t))
≅ C(s, U IStore* a b t)```

```forall f. Applicative f => (a -> f b) -> (s -> f t)
≅ s -> IAppStore a b t```

(the action of `U` is implicit).

The free applicative version of `IStore` is defined as:

```data IAppStore a b t =
Unit t
| IAppStore a (IAppStore a b (b -> t))```

These are all known results, but the use of the Yoneda embedding and the adjunction to define the `IStore` functor makes the derivation more compact and slightly more general.

# Acknowledgments

I’m grateful to Mauro Jaskelioff, Gershom Bazerman, and Joseph Abrahamson for reading the draft and providing helpful comments and to André van Meulebrouck for editing help.

# Bibliography

1. Edward Kmett, The Haskell Lens Library
2. Simon Peyton Jones, Lenses: Compositional Data Access and Manipulation. A Skills Matter video presentation.
3. Joseph Abrahamson, A Little Lens Starter Tutorial
4. Joseph Abrahamson, Lenses from Scratch
5. Artyom, lens over tea tutorial
6. Twan van Laarhoven, CPS based functional references
7. Bartosz Milewski, Lenses, Stores, and Yoneda
8. Mauro Jaskelioff, Russell O’Connor, A Representation Theorem for Second-Order Functionals
9. Bartosz Milewski, Understanding Yoneda

Edward Kmett’s lens library made lenses talk of the town. This is, however, not a lens tutorial (let’s wait for the upcoming Simon Peyton Jones’s intro to lenses (edit: here it is)). I’m going to concentrate on one aspect of lenses that I’ve found intriguing — the van Laarhoven representation.

Quick introduction: A lens is a data structure with a getter and a setter.

```get :: b -> a
set :: b -> a -> b```

Given object of type `b`, the getter returns the value of type `a` of the substructure on which the lens is focused (say, a field of a record, or an element of a list). The setter takes the object and a new value and returns a modified object, with the focus substructure replaced by the new value.

A lens can also be represented as a single function that returns a `Store` structure. Given the object of type `b` the lens returns a pair of: old value at the focus, and a function to modify it. This pair represents the `Store` comonad (I followed the naming convention in Russell O’Connor’s paper, see bibliography):

```data Store a b = Store
{ pos  :: a
, peek :: a -> b
}```

The two elements of `Store` are just like getter and setter except that the initial `b ->` was factored out.

Here’s the unexpected turn of events: Twan van Laarhoven came up with a totally different representation for a lens. Applied to the `Store` comonad it looks like this:

`forall g . Functor g => (a -> g a) -> g b`

The `Store` with `pos` and `peek` is equivalent to this single polymorphic function. Notice that the polymorphism is in terms of the functor `g`, which means that the function may only use the functor-specific `fmap`, nothing else. Recall the signature of `fmap` — for a given `g`:

`fmap :: (a -> b) -> g a -> g b`

The only way the van Laarhoven function could produce the result `g b` is if it has access to a function `a -> b` and a value of type `a` (which is exactly the content of `Store`). It can apply the function `a -> g a` to this value and `fmap` the function `a -> b` over it. Russell O’Connor showed the isomorphism between the two representations of the `Store` comonad.

This is all hunky-dory, but what’s the theory behind this equivalence? When is a data structure equivalent to a polymorphic function? I’ve seen this pattern in the Yoneda lemma (for a refresher, see my tutorial: Understanding Yoneda). In Haskell we usually see a slightly narrower application of Yoneda. It says that a certain set of polymorphic functions (natural transformations) is equivalent to a certain set of values in the image of the functor `g`:

```forall t . (a -> t) -> g t
≈ g a```

Here, `(a -> t)` is a function, which is mapped to `g t` — some functor `g` acting on type `t`. This mapping is defined once for all possible types `t` — it’s a natural transformation — hence `forall t`. All such natural transformations are equivalent to (parameterized by, isomomophic to) a type (set of values) `g a`. I use the symbol `≈` for type isomorphism.

There definitely is a pattern, but we have to look at the application of Yoneda not to Haskell types (the Hask category) but to Haskell functors.

# Yoneda on Functors

We are in luck because functors form a category. Objects in the Functor Category are functors between some underlying categories, and morphisms are natural transformations between those functors.

Here’s the Yoneda construction in the Functor Category. Let’s fix one functor `f` and consider all natural transformations of `f` to an arbitrary functor `g`. These transformations form a set, which is an object in the Set Category. For each choice of `g` we get a different set. Let’s call this mapping from functors to sets a representation, `rep`. This mapping, the canonical Yoneda embedding, is actually a functor. I’ll call this a second order functor, since it takes a functor as its argument. Being a functor, its action on morphisms in the Functor Category is also well-defined — morphisms being natural transformations in this case.

Now let’s consider an arbitrary mapping from functors to sets, let’s call it `eta` and let’s assume that it’s also a 2nd order functor. We have now two such functors, `rep` and `eta`. The Yoneda lemma considers mappings between these 2nd order functors, but not just any mappings — natural transformations. Since those transformations map 2nd order functors, I’ll also call them 2nd order natural transformations (thick yellow arrow in the picture).

What does it mean for a transformation to be natural? Technically, it means that a certain diagram commutes (see my Yoneda tutorial), but the Haskell intuition is the following: A natural transformation must be polymorphic in its argument. It treats this argument generically, without considering its peculiarities. In our case the 2nd order natural transformation will be polymorphic in its functor argument `g`.

The Yoneda lemma tells us that all such 2nd order natural transformations from `rep` to `eta` are in one-to-one correspondence with the elements of `eta` acting on `f`. I didn’t want to overcrowd the picture, but imagine another red arrow going from `f` to some set. That’s the set that parameterizes these natural transformations.

Let’s get down to earth. We’ll specialize the general Functor Category to the category of endofunctors in Hask and replace the Set Category with Hask (a category of Haskell types, which are treated as sets of values).

Elements of the Functor Category will be represented in Haskell through the `Functor` class. If `f` and `g` are two functors, a natural transformation between them can be defined pointwise (e.g., acting on actual types) as a polymorphic function.

`forall t . f t -> g t`

Another way of looking at this formula is that it describes a mapping from an arbitrary functor `g` to the Haskell type `forall t . f t -> g t`, where `f` is some fixed functor. This mapping is the Yoneda embedding we were talking about in the previous section. We’ll call it `RepF`:

```{-# LANGUAGE Rank2Types #-}

type RepF f g = (Functor f, Functor g)
=> forall t . f t -> g t```

The second ingredient we need is the mapping `Eta` that, just like `Rep` maps functors to types. Since the kind of the functor `g` is `* -> *`, the kind of `Eta` is `(* -> *) -> *`.

`type family Eta :: (* -> *) -> *`

Putting all this together, the Yoneda lemma tells us that the following types are equivalent:

```{-# LANGUAGE Rank2Types, TypeFamilies #-}

type family Eta :: (* -> *) -> *

type NatF f = Functor f
=> forall g . Functor g
=> forall t. (f t -> g t) -> Eta g

-- equivalent to

type NatF' = Functor f => Eta f```

There are many mappings that we can substitute for `Eta`, but I’d like to concentrate on the simplest nontrivial one, parameterized by some type `b`. The action of this `EtaB` on a functor `g` is defined by the application of `g` to `b`.

```{-# LANGUAGE Rank2Types #-}

type EtaB b g = Functor g => g b```

Now let’s consider 2nd order natural transformations between `RepF` and `EtaB` or, more precisely, between `RepF f` and `EtaB b` for some fixed `f` and `b`. These transformations must be polymorphic in `g`:

```type NatFB f b = Functor f
=> forall g . Functor g
=> forall t. (f t -> g t) -> EtaB b g```

This can be further simplified by applying `EtaB` to its arguments:

```type NatFB f b = Functor f
=> forall g . Functor g
=> forall t. (f t -> g t) -> g b```

The final step is to apply the Yoneda lemma which, in this case, tells us that the above type is equivalent to the type obtained by acting with `EtaB b` on `f`. This type is simply `f b`.

Do you see how close we are to the van Laarhoven equivalence?

```forall g . Functor g => (a -> g a) -> g b
≈ (a, a -> b)```

We just need to find the right `f`. But before we do that, one little exercise to get some familiarity with the Yoneda lemma for functors.

# Undoing fmap

Here’s an interesting choice for the functor `f` — function application. For a given type `a` the application `(->) a` is a functor. Indeed, it’s easy to implement `fmap` for it:

```instance Functor ((->) a) where
-- fmap :: (t -> u) -> (a -> t) -> (a -> u)
fmap f g = f . g```

Let’s plug this functor in the place of `f` in our version of Yoneda:

```type NatApA a b =
forall g . Functor g
=> forall t. ((a -> t) -> g t) -> g b

NatApA a b ≈ a -> b```

Here, `f t` was replaced by `a -> t` and `f b` by `a -> b`. Now let’s dig into this part of the formula:

`forall t. ((a -> t) -> g t)`

Isn’t this just the left hand side of the regular Yoneda? It’s a natural transformation between the Yoneda embedding functor `(->) a` and some functor `g`. The lemma tells us that this is equivalent to the type `g a`. So let’s make the substitution:

```type NatApA a b =
forall g . Functor g
=> g a -> g b

NatApA a b ≈ a -> b```

On the one hand we have a function `g a -> g b` which maps types lifted by the functor `g`. If this function is polymorphic in the functor `g` than it is equivalent to a function `a -> b`. This equivalence shows that `fmap` can go both ways. In fact it’s easy to show the isomorphism of the two types directly. Of course, given a function `a -> b` and any functor `g`, we can construct a function `g a -> g b` by applying `fmap`. Conversely, if we have a function `g a -> g b` that works for any functor `g` then we can use it with the trivial identity functor `Identity` and recover `a -> b`.

So this is not a big deal, but the surprise for me was that it followed from the Yoneda lemma.

# The Store Comonad and Yoneda

After this warmup exercise, I’m ready to unveil the functor `f` that, when plugged into the Yoneda lemma, will generate the van Laarhoven equivalence. This functor is:

`Product (Const a) ((->) a)`

When acting on any type `b`, it produces:

`(Const a b, a -> b)`

The `Const` functor ignores its second argument and is equivalent to its first argument:

`newtype Const a b = Const { getConst :: a }`

So the right hand side of the Yoneda lemma is equivalent to the `Store` comonad `(a, a -> b)`.

Let’s look at the left hand side of the Yoneda lemma:

```type NatFB f b = Functor f
=> forall g . Functor g
=> forall t. (f t -> g t) -> g b```

and do the substitution:

```forall g . Functor g
=> forall t. ((a, a -> t) -> g t) -> g b```

Here’s the curried version of the function in parentheses:

`forall t. (a -> (a -> t) -> g t)`

Since the first argument `a` doesn’t depend on `t`, we can move it in front of `forall`:

`a -> forall t . (a -> t) -> g t`

We are now free to apply the 1st order Yoneda

`forall t . (a -> t) -> g t ≈ g a`

Which gives us:

`a -> forall t . (a -> t) -> g t ≈ a -> g a`

Substituting it back to our formula, we get:

```forall g . Functor g => (a -> g a) -> g b
≈ (a, a -> b)```

Which is exactly the van Laarhoven equivalence.

# Conclusion

I have shown that the equivalence of the two formulations of the `Store` comonad and, consequently, the `Lens`, follows from the Yoneda lemma applied to the Functor Category. This equivalence is a special case of the more general formula for functor-polymorphic representations:

```type family Eta :: (* -> *) -> *

Functor f
=> forall g . Functor g
=> forall t. (f t -> g t) -> Eta g
≈ Functor f => Eta f```

This formula is parameterized by two entities: a functor `f` and a 2nd order functor `Eta`.

In this article I restricted myself to one particular 2nd order functor, `EtaB b`, but it would be interesting to see if more complex `Eta`s lead to more interesting results.

In the choice of the functor `f` I also restricted myself to just a few simple examples. It would be interesting to try, for instance, functors that generate recursive data structures and try to reproduce some of the biplate and multiplate results of Russell O’Connor’s.

# Appendix: Another Exercise

Just for the fun of it, let’s try substituting `Const a` for `f`:

The naive substitution would give us this:

```forall g . Functor g
=> (forall t . Const a t -> g t) -> g b
≈ Const a b```

But the natural transformation on the left:

`forall t . Const a t -> g t`

cannot be defined for all `g`s. `Const a t` doesn’t depend on `t`, so the co-domain of the natural transformation can only include functors that don’t depend on their argument — constant functors. So we are really only looking for `g`s that are `Const c` for any choice of `c`. All the allowed variation in `g` can be parameterized by type `c`:

```forall c . (Const a t -> Const c t) -> Const c b
≈ Const a b```

If you remove the `Const` noise, the conclusion turns out to be pretty trivial:

`forall c . (a -> c) -> c ≈ a`

It says that a polymorphic function that takes a function `a -> c` and returns a `c` must have some fixed `a` inside. This is pretty obvious, but it’s nice to know that it can be derived from the Yoneda lemma.

# Acknowledgment

Special thanks go to the folks on the Lens IRC channel for correcting my Haskell errors and for helpful advice.

# Update

After I finished writing this blog, I contacted Russel O’Connor asking him for comments. It turned out that he and Mauro Jaskelioff had been working on a paper in which they independently came up with almost exactly the same derivation of the van Laarhoven representation for the lens starting from the Yoneda lemma. They later published the paper, A Representation Theorem for Second-Order Functionals, including the link to this blog. It contains a much more rigorous proof of the equivalence.

# Bibliography

1. Twan van Laarhoven, [CPS based functional references](http://twanvl.nl/blog/haskell/cps-functional-references)
2. Russell O’Connor, [Functor is to Lens as Applicative is to Biplate](http://arxiv.org/pdf/1103.2841v2.pdf)

« Previous Page