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.
f is a functor. Then parametricity implies the following free theorem for the function
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
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.
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 .