Yoneda lemma

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

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

φ_{b} (k) = φ_{b} (k \circ id_{a}) = F (k) (φ_{a} (id_{a}))

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

The Yoneda form of a functor, in Haskell.

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.

The same, specialized to lists in OCaml, with a counter on traversals.

(* 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))) }

Running it.

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 f b$ , makes any type constructor a functor: it stores the function until something that knows how to apply it comes along.