Yoneda lemma

For a functor $F$ and an object $a$, $\mathrm{Nat}(\mathrm{Hom}(a,-),F)\cong Fa$. In Haskell, $\forall b.(a\to b)\to fb$ is isomorphic to $fa$, and the left-hand form turns a chain of fmaps into one composed function and a single fmap.

The two directions: a natural transformation $\phi$ goes to ${\phi }_a({\mathrm{id}}_a)\in Fa$, and an element $x\in Fa$ goes to the transformation with components $k\mapsto F(k)(x)$. Naturality of $\phi$ at $k:a\to b$, applied to ${\mathrm{id}}_a$, shows that $\phi$ is determined by that one element:

In Haskell every function of type $\forall b.(a\to b)\to fb$ is natural by parametricity, so the lemma becomes an isomorphism of types:

newtype Yoneda f a = Yoneda (forall b. (a -> b) -> f b)
 
liftYoneda :: Functor f => f a -> Yoneda f a
liftYoneda fa = Yoneda (\k -> fmap k fa)
 
lowerYoneda :: Yoneda f a -> f a
lowerYoneda (Yoneda y) = y id
 
instance Functor (Yoneda f) where
  fmap g (Yoneda y) = Yoneda (\k -> y (k . g))

fmap on Yoneda f does not use f's fmap at all; it precomposes. A chain of $n$ fmaps becomes one composed function, and lowerYoneda applies it in a single traversal. That matters for any functor whose fmap walks a large structure.

(* Yoneda for lists: a list, represented by what fmap would do to it. *)
type 'a yoneda = { run : 'b. ('a -> 'b) -> 'b list }
 
let traversals = ref 0
let map f xs = incr traversals; List.map f xs
 
let lift xs = { run = (fun k -> map k xs) }
let lower y = y.run (fun x -> x)
 
(* fmap on the Yoneda form does not touch the list: it composes. *)
let fmap f y = { run = (fun k -> y.run (fun x -> k (f x))) }

map h (map g (map f xs))          ->  [2; 4; 6; 8; 10], traversals: 3
lower (fmap h (fmap g (fmap f .)))  ->  [2; 4; 6; 8; 10], traversals: 1

The dual, Coyoneda, $\exists b.(b\to a)\times fb$, makes any type constructor a functor: it stores the function until something that knows how to apply it comes along.

• Higher-kinded typeA type that abstracts over a type constructor rather than over a type, so that Functor f can be instantiated at Maybe or at lists without naming their element types. It is what makes a single Monad class usable across every container instead of one class per shape.
• HylomorphismA function that unfolds a seed into a recursive structure and folds that structure into a result, written so the structure is never built: hylo f g = f . fmap (hylo f g) . g. The call tree of the recursion is the intermediate structure.
• FunctorA type constructor f with a map operation, fmap : (a -> b) -> f a -> f b, that preserves identity and composition. Lists, options, trees and functions out of a fixed type are functors. In OCaml the word also means something else: a module parametrised by another module, such as Map.Make.
• MonadIn functional programming, a monad is a type constructor m with two operations, return : a -> m a and bind : m a -> (a -> m b) -> m b, satisfying three laws. It lets code with some extra behaviour, such as failure, several results, configuration, state or I/O, be written as a sequence of ordinary steps, with the behaviour defined once in bind. The notion comes from category theory.

1. [1]S. Mac Lane, Categories for the Working Mathematician, Springer (2nd ed., 1998).
2. [2]P. Wadler, “Theorems for free!”, FPCA (1989).