Co-Yoneda Lemma

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 $\exists b. (b\to a, f\, b)$. 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 $F$ on the category of sets. Suppose that $\mathcal{B}: B \Leftrightarrow B'$ is a relation associated with the type b. That is, $\mathcal{B}$ is a subset of $B\times B'$. Let $\iota: \mathcal{B}\hookrightarrow B\times B'$ denote the inclusion map. We define the relation associated with the type f b as the image of the composite $\langle F\pi, F\pi'\rangle\circ F\iota: F(\mathcal{B})\to FB\times FB'$, where $\pi: B\times B'\to B$ and $\pi': B\times B'\to B'$ are the canonical projections.

For example, if f = [], so that $F=(-)^*$ is the list functor, then the above definition says that two lists $xs \in B^*$ and $ys \in B'^*$ are related if there exists a list $zs\in \mathcal{B}^* \subset (B\times B')^*$ such that $\displaystyle \begin{array}{rcl} map\; fst\; zs & \equiv & xs,\\ map\; snd\; zs & \equiv & ys. \end{array}$

In other words, $xs$ and $ys$ 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 $\mathcal{B}$ is the relation associated with a function $g: B\to B'$, then $F(\mathcal{B})$ is the relation associated with the function $Fg$. Indeed, if $\mathcal{B}$ is the graph of $g$, i.e., the image of the map $\langle\mathrm{id}_B, g\rangle: B\to B\times B'$, then $F(\mathcal{B})$ is the image of the composite $\langle F\pi, F\pi'\rangle\circ F(\langle\mathrm{id}_B, g\rangle)$, which coincides with $\langle F\mathrm{id}_B, Fg\rangle = \langle \mathrm{id}_{FB}, Fg\rangle$. Therefore, $F(\mathcal{B})$ coincides with the graph of $Fg$.