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.

# Back to Haskell

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

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

October 15, 2013 at 5:41 am

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

From computational point of view, it’s not true. There is no way to write a function with “forall c . (a -> c) -> c -> a” signature without using “undefined” or “unsafePerformIO”. That’s because such type is CH-isomorphic to proposition NOT(NOT(A)) => A, which doesn’t hold in intuitionistic logic.

The fact that Yoneda lemma, CPS and double-negation are just three faces of one thing always amazed me.

October 15, 2013 at 10:50 am

Great observation! Frankly I wasn’t aware of this. Of course the isomorphism still holds in category theory, which is all that matters. The main reason I switched to Haskell notation was that I’m not fluent in mathematical notation and the blog was intended for Haskell programmers.

November 1, 2013 at 9:31 pm

Joker_vD: Um, yes there is

ying :: (forall c. (a -> c) -> c) -> a

ying f = f id

November 2, 2013 at 11:38 am

@Russell : That’s a good point.

But Joker_vD has a point too, if you define:

I think the apparent contradiction is there because the forall quantifier in Haskell also includes uninhabited types like Void. Here’s another definition of Not, which I think is equivalent:

So what does it mean to call ying with:

Does it make sense to say that if you call id with a Void argument it will return a Void result? These are the confusing bits of Haskell, at least to me, so take what I say with a grain of salt 😉

November 2, 2013 at 11:43 am

I’ve found a much better explanation here.

January 14, 2014 at 10:40 am

[…] A container is not a very well defined term — an ambiguity I exploited in this blog post — but there is a well defined notion of finitary containers, and they indeed have a strong connection to functors. Russell O’Connor and Mauro Jaskelioff have recently shown that every traversable functor is a finitary container (I’m grateful to the authors for providing me with the preliminary copy of their paper, in which they have also indenpendently and much more rigorously shown the connection between the Yoneda lemma for the functor category and the van Laarhoven formulation of th…). […]

December 11, 2014 at 8:40 am

I think Joker_vD has confused

with

The latter is trivial to define as Russell O’Connor has shown. The former is not (without cheating).

September 4, 2015 at 1:53 pm

[…] Lenses, Stores, and Yoneda | Bartosz Milewski’s Programming Cafe https://bartoszmilewski.com/2013/10/08/lenses-stores-and-yoneda/ […]

October 31, 2017 at 7:36 am All of this (as is often the case in category theory) is a special case of the Yoneda lemma’s statement with Kan extensions. Here’s my implementation of it in Lean which I find a bit more enlightening since there’s less noise from fancy Haskell extensions, rather it’s all vanilla dependent types: .gist table { margin-bottom: 0; } This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters Show hidden characters def ran (g h : Type → Type) (α : Type) := Π β, (α → g β) → h β def lan (g h : Type → Type) (α : Type) := Σ β, (g β → α) × h β def mapr {g h} {α β} (s : α → β) (x : ran g h α) : ran g h β := λ b t, x b (t ∘ s) def mapl {g h} {α β} (s : α → β) (x : lan g h α) : lan g h β := ⟨x.1, ⟨s ∘ x.2.1, x.2.2⟩⟩ attribute [reducible] id attribute [simp] function.comp — @[simp] lemma prod.mk.eta {α β} : Π {p : α × β}, (p.1, p.2) = p — | (a, b) := rfl @[simp] lemma sigma.mk.eta {α} {β : α → Type} : Π {p : Σ α, β α}, sigma.mk p.1 p.2 = p | ⟨a, b⟩ := rfl instance {g h} : functor (ran g h) := { map := @mapr g h } instance {g h} : is_lawful_functor (ran g h) := { id_map := by intros; simp [functor.map, mapr], comp_map := by intros; simp [functor.map, mapr] } instance {g h} : functor (lan g h) := { map := @mapl g h } instance {g h} : is_lawful_functor (lan g h) := { id_map := by intros; simp [functor.map, mapl], comp_map := by intros; simp [functor.map, mapl] } def natural {f g} [functor f] [functor g] (t : Π {α}, f α → g α) := Π {α β} {x : f α} (s : α → β), s <$> (t x) = t (s <$> x) axiom free_theorem {f g} [functor f] [functor g] (t : Π α, f α → g α) : natural t section yoneda variables {f : Type → Type} [functor f] [is_lawful_functor f] {α : Type} @[reducible] def yoneda := ran id def check (x : f α) : yoneda f α := λ b s, s <$> x def uncheck (x : yoneda f α) : f α := x α id def uncheck_check (x : f α) : uncheck (check x) = x := begin simp [check, uncheck, is_lawful_functor.id_map] end def check_uncheck (x : yoneda f α) : check (uncheck x) = x := begin simp [check, uncheck], funext, apply free_theorem (@uncheck f _ _) end @[reducible] def coyoneda := lan id def cocheck (x : f α) : coyoneda f α := ⟨α, ⟨id, x⟩⟩ def councheck (x : coyoneda f α) : f α := x.2.1 <$> x.2.2 def councheck_cocheck (x : f α) : councheck (cocheck x) = x := begin simp [cocheck, councheck, is_lawful_functor.id_map] end def cocheck_councheck (x : coyoneda f α) : cocheck (councheck x) = x := begin simp [councheck], rw ←free_theorem (@cocheck f _ _), simp [cocheck, functor.map, mapl] end end yoneda structure {u v} iso (α : Type u) (β : Type v) := (f : α → β) (g : β → α) (gf : Π x, g (f x) = x) (fg : Π x, f (g x) = x) namespace iso def inv {α β} (i : iso α β) : iso β α := ⟨i.g, i.f, i.fg, i.gf⟩ def comp {α β γ} (i : iso α β) (j : iso β γ) : iso α γ := ⟨j.f ∘ i.f, i.g ∘ j.g, by simp [j.gf, i.gf], by simp [i.fg, j.fg]⟩ universes u v w variables {f : Type u → Type v} {g : Type u → Type w} (i : Π {α}, iso (f α) (g α)) def imap [functor f] {α β : Type u} (s : α → β) (x : g α) : g β := i.f $ s <$> i.g x def ipure [applicative f] {α : Type u} (x : α) : g α := i.f $ pure x def iseq [applicative f] {α β : Type u} (s : g (α → β)) (x : g α) : g β := i.f $ i.g s <*> i.g x def ibind [monad f] {α β : Type u} (x : g α) (s : α → g β) : g β := i.f $ i.g x >>= i.g ∘ s @[priority std.priority.default-1] instance functor [functor f] : functor g := { map := @imap f g @i _ } — @[priority std.priority.default-1] — instance is_lawful_functor [functor f] : is_lawful_functor g := — { id_map := — begin — intros, — simp [imap, is_lawful_functor.id_map, i.fg] — end, — comp_map := — begin — intros, — simp [imap, i.gf], — rw is_lawful_functor.comp_map — end } @[priority std.priority.default-1] instance applicative [applicative f] : applicative g := { pure := @ipure f g @i _, seq := @iseq f g @i _ } — @[priority std.priority.default-1] — instance is_lawful_applicative [is_lawful_applicative f] : is_lawful_applicative g := — { pure_seq_eq_map := by intros; simp, — id_map := — begin — intros, — simp [ipure, iseq, i.gf], — simp [is_lawful_applicative.pure_seq_eq_map, is_lawful_functor.id_map, i.fg] — end, — map_pure := — begin — intros, — simp [ipure, iseq, i.gf], — simp [is_lawful_applicative.pure_seq_eq_map, is_lawful_applicative.map_pure] — end, — seq_pure := — begin — intros, — simp [ipure, iseq, i.gf], — simp [is_lawful_applicative.pure_seq_eq_map, is_lawful_applicative.seq_pure] — end, — seq_assoc := — begin — intros, — simp [ipure, iseq, i.gf], — simp [is_lawful_applicative.pure_seq_eq_map, is_lawful_applicative.seq_assoc] — end } @[priority std.priority.default-1] instance monad [monad f] : monad g := { pure := @ipure f g @i _, bind := @ibind f g @i _ } — @[priority std.priority.default-1] — instance is_lawful_monad [is_lawful_monad f] : is_lawful_monad g := — { id_map := — begin — intros, — simp [ipure, ibind, i.gf], — rw monad.bind_pure_comp_eq_map, — simp [is_lawful_functor.id_map, i.fg] — end, — pure_bind := — begin — intros, — simp [ipure, ibind, i.gf], — simp [is_lawful_monad.pure_bind, i.fg] — end, — bind_assoc := — begin — intros, — simp [ibind, i.gf], — simp [is_lawful_monad.bind_assoc] — end } end iso section yoneda_iso variables (f : Type → Type) [functor f] [is_lawful_functor f] ⦃α : Type⦄ def yoneda_iso : iso (f α) (yoneda f α) := ⟨check, uncheck, uncheck_check, check_uncheck⟩ def coyoneda_iso : iso (f α) (coyoneda f α) := ⟨cocheck, councheck, councheck_cocheck, cocheck_councheck⟩ def yoco_iso : iso (yoneda f α) (coyoneda f α) := (@yoneda_iso f _ _ α).inv.comp (@coyoneda_iso f _ _ α) end yoneda_iso — instance {f} [applicative f] : applicative (yoneda f) := iso.applicative (yoneda_iso f) — instance {f} [applicative f] : applicative (coyoneda f) := iso.applicative (coyoneda_iso f) — instance {f} [monad f] : monad (yoneda f) := iso.monad (yoneda_iso f) — instance {f} [monad f] : monad (coyoneda f) := iso.monad (coyoneda_iso f) section naturality_proofs variables {f : Type → Type} [functor f] [is_lawful_functor f] def natural_check : natural (@check f _ _) := begin unfold natural, intros, dsimp [check, functor.map, mapr], funext, rw is_lawful_functor.comp_map end def natural_uncheck : natural (@uncheck f _ _) := begin unfold natural, intros, dsimp [uncheck, functor.map, mapr], admit — ← stuck here end def natural_cocheck : natural (@cocheck f _ _) := begin unfold natural, intros, dsimp [cocheck, functor.map, mapl], admit — ← stuck here end def natural_councheck : natural (@councheck f _ _) := begin unfold natural, intros, dsimp [councheck, functor.map, mapl], rw ←is_lawful_functor.comp_map end end naturality_proofs view raw kan.lean hosted with ❤ by GitHub

March 16, 2019 at 7:57 am

Loving reading your blogs about the category theory, but the image seems lost: https://i2.wp.com/www.bartosz.com/images/Yoneda/FunctorYoneda.png,

could you reupload it again? thank you!

March 16, 2019 at 9:06 am

Fixed. Thanks!

March 23, 2021 at 1:13 pm

[…] Lenses, Stores, and Yoneda […]

June 11, 2021 at 5:39 pm

[…] Milewski’s posts on “From Lenses to the Yoneda Embedding“, “Lenses, Stores and Yoneda“, and general posts from him on Lenses, as well as […]