The Yoneda lemma and parametricity

I’ve always felt that I don’t have a good grasp of the Yoneda lemma, in particular the various sorts of naturality about it. Recently I’ve got a chance to rethink the lemma, and I think my intuition about parametricity (reinforced since last summer) —which is obviously closely related to naturality (cf Hermida et al’s treatment)— may help. Parametricity characterises representation independence of a construction by saying that whatever property that holds for one or more representations is preserved by the construction. This preservation most frequently arises from intensional constraints imposed on parametrically typed programs, which must be defined uniformly over representations of parametric types without being able to peek into representation detail (and thus cannot interfere with whatever property that holds). What’s genius about parametricity, though, is that it’s an extensional characterisation, and a program can even use non-parametric constructs such as type-case carefully and still satisfy parametricity as long as it behaves uniformly (cf semantic type soundness); although we don’t get to assume functions satisfying parametricity are defined uniformly, it can help to pretend that they are —that is, invoke the intuition gained by writing uniform programs in languages with parametric types— to predict what parametricity can say about them.

I want to apply the same strategies to the Yoneda lemma, imagining that I’m programming it in a parametrically typed language that’s basically Agda but adapted to talk about categories natively. To set the scene: Let C be a category (which can be thought of as a special sort in the language), C(c, d) : Set the hom-set from c : C to d : C, and F : C → Set a functor (here the coincidence of Set between category theory and Agda is quite pleasing). The usual Yoneda lemma says that, for every object c : C, there’s an isomorphism between functions of type ∀ d → C(c, d) → F d —which are natural in d— and elements of F c. Moreover, the forward map of type (∀ d → C(c, d) → F d) → F c is natural in both c and F. (Then a quick and generic argument shows that the naturality of the backward map follows from that of the forward map, its inverse.)

Remark. Apparently one could also talk about naturality in C, which is also a parameter, but that’s not usually talked about in standard presentations and I’ll skip it in this post, although it seems to be an interesting follow-up exercise to see how far the parametricity perspective can lead us. (End of Remark.)

Naturality in d

I’ll start from a special case: continuation-passing style. We know that ∀ X → (A → X) → X is isomorphic to A, because the only way for a function f : ∀ X → (A → X) → X to produce a result of type X is to apply a given continuation k : A → X, and therefore f must conceal an element a : A to which it can apply k; due to the special type of f, the element a can be revealed by supplying id : A → A as the continuation. This is an intensional argument (‘f can only be defined in this way’), which doesn’t necessarily hold (you can, for example, copy the element a into some data structure and do some crazy transformations before applying k to the elements and extract one of them as the result), but it gives us a good idea of what parametricity can prove: f necessarily behaves the same as λ X k → k a for some element a chosen uniformly in X (that is, the choice of a cannot depend on X), so f A id will reveal a and determine the behaviour of f for all X and k. Another example/exercise is that a function g : ∀ X → X → X → X is necessarily the first or second projection: the choice of ‘first’ or ‘second’ has to be made uniformly in X, so by evaluating a special instance like g true false we can find out which choice is made (cf Voigtländer’s ‘bidirectionalisation for free’).

To give more detail, the (binary) parametricity of f says that any relation R : X → X' → Set is preserved by f: if two inputs k : A → X and k' : A → X' are related by R, then the outputs f X k and f X' k' are related by R too. The latter means simply R (f X k) (f X' k') is inhabited, while the former intuitively means that R holds for all corresponding pairs of X and X' in k and k'; in this case k/k' can be thought of as A-indexed collections of X/X', so the logical lifting of R to relate k and k' is ∀ a → R (k a) (k' a). Suppose that the parametricity of f is witnessed by

fᴿ : {X X' : Set}                (R : X → X' → Set)
   → {k : A → X} {k' : A → X'} → (∀ a → R (k a) (k' a))
                               →  R (f X k) (f X' k')

What we want to prove is f X k ≡ k (f A id) for any input X and k (where f A id is the concealed element a in the previous paragraph); choose X' = A,k' = id, and R x a = x ≡ k a, and the result type of fᴿ instantiates to exactly what we want. fᴿ requires us to prove the condition that the input functions k and id are related, which expands to ∀ a → k a ≡ k (id a) and is obviously true.

λ X k → fᴿ (λ x a → x ≡ k a) (λ a → refl)
  : ∀ X (k : A → X) → f X k ≡ k (f A id)

Note that the condition can be compressed to k ≡ k ∘ id, which is closer to the categorical language.

The above argument can be readily generalised to the natural transformations in the Yoneda lemma, which have type

α : ∀ d → C(c, d) → F d

If we imagine programming α parametrically in F, c, and d, we’ll reach a similar conclusion that α must conceal an element of F c, which can be revealed as α c id (where id : ∀ {c} → C(c, c) denotes the identity morphisms), and in general for inputs d : C and m : C(c, d), we can determine α d m ≡ F m (α c id) (where F : ∀ {c d} → C(c, d) → F c → F d is overloaded by convention). The naturality of α is usually stated as (the diagrammatic form of)

∀ {d d'} (f : C(d, d')) → α d' ∘ (f ∘_) ≡ F f ∘ α d

but in this case we’re dealing with sets/types and functions, so this can be restated as morphism preservation (which is less higher-order and more comprehensible),

nat : ∀ {d d'}                       (f : C(d, d'))
    → {m : C(c, d)} {m' : C(c, d')} → m' ≡ f ∘ m
                                    → α d' m' ≡ F f (α d m)

and can be used in essentially the same way as fᴿ above,

λ d m → nat m (sym id-r)
  : ∀ d (m : C(c, d)) → α d m ≡ F m (α c id)

except that we need to invoke the category law id-r : ∀ {m} → m ∘ id ≡ m.

Naturality in c

The proof of naturality in c usually gets complicated rather quickly, probably because the Yoneda lemma usually appears early on in a textbook and is used as an example for the reader to get familiar with the basic definitions, but the forward map in the isomorphism

yo : ∀ c → (∀ d → C(c, d) → F d) → F c
yo c α = α c id

has order 3 if C(c, d) is counted, and most people have difficulties dealing with functions so higher-order (Peirce’s law ((P → Q) → P) → P is another example). But this naturality shouldn’t be so difficult — we actually have a uniform definition yo in hand, so we should get parametricity by construction, from which naturality shouldn’t be far away.

Formally, ‘by construction’ refers to the parametricity translation:

yoᴿ : ∀ {c c'}                    (f : C(c, c'))
    → {α  : ∀ d → C(c , d) → F d}
      {α' : ∀ d → C(c', d) → F d} (αᴿ : ∀ {d d'} (g : C(d, d'))
                                      → Related f g α α')
                                 → yo c' α' ≡ F f (yo c α)
yoᴿ f αᴿ = αᴿ f idᴿ

where

Related f g α α' =
  {m : C(c, d)} {m' : C(c', d')} → m' ∘ f ≡ g ∘ m
                                 → α' d' m' ≡ F g (α d m)

and

idᴿ : {c c' : C} {f : C(c, c')} → id ∘ f ≡ f ∘ id

I’ve adapted the translation to preserve morphisms instead of relations. Unlike relations, morphisms are directional, and in the type of yoᴿ I’ve chosen the directions of f and g, which in this case must match for the translation to work — if choosing g : C(d', d), then Related f g α α' becomes

{m : C(c, d)} {m' : C(c', d')} → g ∘ m' ∘ f ≡ m
                               → F g (α' d' m') ≡ α d m

(and is in fact a form of naturality), but then directly using αᴿ (as done by the translation in the definition of yoᴿ) no longer type-checks. My conjecture is that the full parametricity translation for this language with native support for categories —even if restricted to preserving morphisms— should allow the user to choose morphism directions. For example, αᴿ should let its user choose between g : C(d, d') and g : C(d', d); in particular, when the translation applies αᴿ and substitute f for g, it can choose the same direction as f. More generally, maybe we should preserve diagrams and allow the user to choose which diagrams to preserve (but morphism preservation (with choice of direction) may well be enough).

The type of yoᴿ goes strictly beyond naturality: when stated in the form of morphism preservation, the premise and conclusion of naturality are both functional (such as the type of nat in the previous section), whereas in Related f g α α' the premise m' ∘ f ≡ g ∘ m is not. (This was Reynolds’s original motivation for inventing relational parametricity.) Also note that even though m' ∘ f ≡ g ∘ m is conceptually morphism preservation, it can no longer be stated clearly as so (‘mapping related inputs to related outputs’), and needs to be phrased as an equality — m and m' are (abstract) morphisms rather than functions, so we can’t do pointwise expansion (as in nat above). This might make the parametricity approach less usable in more abstract settings (with more categorical structures than sets/types), where we may need to find ways to compress relations into morphisms so as to fit preservation statements into equalities.

The definition of yoᴿ shows that it’s straightforward to prove the parametricity of a uniform term by following the term’s structure. But we’re hoping to prove naturality, not parametricity. In this case, the conclusion of (the morphism-preserving form of) naturality is the same as that of parametricity, and it remains to show that the naturality premises imply the parametricity premise — that is, we need to construct αᴿ from nat above and

rel : ∀ {c c'}                       (f : C(c, c'))
    → ∀ {d}
    → {m : C(c, d)} {m' : C(c', d)} → m' ∘ f ≡ m
                                    → α' d m' ≡ α d m

which is the morphism-preserving form of

∀ {c c'} (f : C(c, c')) → ∀ {d} → α' d ≡ α d ∘ (_∘ f)

(which is already too higher-order for most people). The function _∘ (_∘ f) that maps α d to α' d (and is hopelessly higher-order) can be thought of as the result of logical lifting in the categorical language, but since we’re applying hom-functors to do the lifting, we lift only one morphism (in this case f) and change only one object (in this case from c to c') at a time:

          f  : C(c, c')
↦      _∘ f  : C(c', d) → C(c, d)
↦  _∘ (_∘ f) : (C(c, d) → F d) → (C(c', d) → F d)

On the second and third lines, we’re changing the domain by lifting the morphism from the previous line while fixing the codomain; the overall effect is that we’re changing c to c' in a complex type while keeping everything else fixed. Compare this with nat, which changes d to d'. Now compose rel and nat, and we get αᴿ, changing both objects in one go:

λ {m : C(c, d)} {m' : C(c', d'))} (mᴿ : m' ∘ f ≡ g ∘ m) →
  begin
    α' d' m'
      ≡⟨ rel f refl ⟩
    α d' (m' ∘ f)
      ≡⟨ nat g mᴿ ⟩
    F g (α d m)
  ∎ : Related f g α α'

My conjecture is that this is not a coincidence: it is well known that parametricity specialises to naturality; conversely, as observed here, we may be able to reconstruct parametricity if we have naturality in all the objects involved. Eventually we may be able to reason about uniform categorical constructions conveniently in terms of parametricity, but require only naturality as stated in the usual definitions, or can work out which naturality conditions are sufficient.

Naturality in F

This naturality is actually pretty mundane, but well, simple things should be simple to prove, so let’s verify whether this motto holds for our methodology. If we include the quantification over F in yo,

yo : ∀ F → ∀ c → (∀ d → C(c, d) → F d) → F c
yo F c α = α c id

and perform the parametricity translation only with respect to F, we get something very simple:

yoᴿ : ∀ {F F'}                    (β : ∀ d → F d → F' d))
    → ∀ {c}
    → {α  : ∀ d → C(c, d) → F  d}
      {α' : ∀ d → C(c, d) → F' d} (αᴿ : ∀ {d} {m : C(c, d)}
                                      → α' d m ≡ β d (α d m))
                                 → yo F' c α' ≡ β c (yo F c α)
yoᴿ β αᴿ = αᴿ

Since yo is only an invocation of α, if we know the result of α can be changed from F d to F' d, then surely the result of yo can be changed in the same way.

---