### Co-Yoneda Lemma

#### by oleksandrmanzyuk

The purpose of this humble blog post is to understand this insightful comment by Edward Kmett to the question “Is operational really isomorphic to a free monad?” posted at StackOverflow.

Consider the following data type definition in Haskell, which can also be found in Edward Kmett’s package kan-extensions:

data CoYoneda f a = forall b. CoYoneda (b -> a) (f b)

In Haskell, a `forall`

before the data constructor means existential rather than universal quantification, so that `CoYoneda f a`

is isomorphic to the type . The `forall`

hints at the polymorphic type of the constructor

CoYoneda :: forall b. (b -> a) -> f b -> CoYoneda f a

Every polymorphic function satisfies a theorem that can be extracted by reading its type as a relation. This is referred to as parametricity. The reader is referred to Wadler’s classic paper “Theorems for free!” for more details.

Suppose that `f`

is a functor. Then parametricity implies the following free theorem for the function `CoYoneda`

: if `g :: b -> a`

and `y :: f c`

, then `CoYoneda (g . h) y == CoYoneda g (fmap h y)`

for any `h :: c -> b`

.

Consider the following two functions:

phi :: f a -> CoYoneda f a phi x = CoYoneda id x psi :: Functor f => CoYoneda f a -> f a psi (CoYoneda g y) = fmap g y

Then obviously `psi . phi == id`

:

(psi . phi) x == fmap id x == x

The above free theorem implies also that `phi . psi == id`

:

(phi . psi) (CoYoneda g y) == CoYoneda id (fmap g y) == CoYoneda g y

We conclude that `CoYoneda f`

is isomorphic `f`

. This is a Haskell version of the co-Yoneda Lemma.

### Appendix

The only thing that is missing in Wadler’s paper is how to associate a relation with the type `f b`

. Wadler only explains this in the case of the list functor. We assume that the Haskell functor `f`

is modeled by a functor on the category of sets. Suppose that is a relation associated with the type `b`

. That is, is a subset of . Let denote the inclusion map. We define the relation associated with the type `f b`

as the image of the composite , where and are the canonical projections.

For example, if `f = []`

, so that is the list functor, then the above definition says that two lists and are related if there exists a list such that

In other words, and are related if they have the same length and corresponding elements are related, which coincides with Wadler’s definition.

It follows from this definition that if is the relation associated with a function , then is the relation associated with the function . Indeed, if is the graph of , i.e., the image of the map , then is the image of the composite , which coincides with . Therefore, coincides with the graph of .

Struggling with the last paragraph, my calculation falls into:

\langle \mathrm{id} _ {FB}, Fg \rangle \circ F(\pi \circ \iota)

Without surjective F(\pi \circ \iota), the images don’t coincide?

Hi! The map \langle \mathrm{id}_{B}, g \rangle induces an isomorphism from B onto its image, and \pi \circ \iota is the inverse. Therefore, F(\pi \circ \iota) is also an isomorphism.

Elementary!

(Actually you’ve solved my one-year problem.)

Many thanks.