7
$\begingroup$

This question asks for an informal explanation of why all polymorphic functions between functors are natural transformations (This is a claim made by Bartosz Milewski). One answer to that question refers to the Theorems for free! paper. However, after reading it I'm not seeing how it implies the result.

The parametricity theorem from "Theorems for free!" can be applied to a function that has the "natural transformation type signature": $\eta:\forall X,F (X) \to G (X)$ for some $F, G : \text{Type} \to \text{Type}$. Basically parametricity gives us (applying it to a functional relation): For any types $A_1,A_2$ and function $f:A_1\to A_2$, the following equation holds:

$$f_G\circ \eta_{A_1}=\eta _{A_2}\circ f_{F}$$

where I define $f_G$ and $f_F$ as the relations that Wadler would write as $[[F(X)]]\mathcal A[f\setminus X]$ and $[[G(X)]]\mathcal A[f\setminus X]$ respectively (I can't write the double square bracket symbol \llbracket).

This looks like the right equation for $\eta$ to be a natural transformation, but the problem is that $f_G$ and $f_F$ aren't necessarily equal to the functions $G(f)$ and $F(f)$. In fact, we haven't even defined $F$ and $G$ as functors. Instead, $f_G$ and $f_F$ are the specific functions that you get when you apply Wadler's definition of the relation that belongs to each type.

Therefore I don't see how you would use the parametricity theorem to show that polymorphic functions between functors are natural transformations, because as far as I can tell, the parametricity theorem doesn't even allow you to specify the morphism part of the functors $F,G$. It only takes them as type constructors.

Is there something I'm missing? Is there a formal proof? It would be nice to have a self-contained proof that "parametric polymorphism implies naturality", that requires minimal background knowledge.

$\endgroup$
0
6
$\begingroup$

The missing part is the "identity extension lemma", which is mentioned in Reynolds' original paper but not in Wadler's.

For $F : \text{Type} \to \text{Type}$, this says that if the relational interpretation of $F$ is instantiated with a type $A$ and the identity relation on $A$, we get the identity relation on $F\,A$.

For System F, identity extension can be proven for types-in-contexts, but note that there is no $F : \text{Type} \to \text{Type}$ in System F. To gracefully handle identity extension for type operators in general, it's better to switch to reflexive graph models, where identity extension is given mutually with the rest of the model.

Let's use the reflexive graph model of some type theory. This means that for every closed $F : \text{Type} \to \text{Type}$, we get a semantic $F^S : \text{Set} \to \text{Set}$, together with $F^R : (A, B : \text{Set}) \to \text{Rel}\,A\,B \to \text{Rel}\,(F\,A)\,(F\,B)$ where $\text{Rel}\,A\,B$ denotes a set of proof-irrelevant relations. We also get identity extension: $F^R\,A\,A\,(\text{Id}\,A) = \text{Id}\,(F\,A)$, where $\text{Id}\,A$ is the identity relation. In the following, let's omit all $^S$-es and don't talk about syntactic things, only about semantic things, so that we may write $F : \text{Set} \to \text{Set}$.

Assume $F, G : \text{Set} \to \text{Set}$ are functors, and $\eta : (A : \text{Set}) \to F\,A \to G\,A$. Let's write $\text{map}$ for functorial mapping. We assume that everything is parametric. This means that we get $F^R$, $G^R$, $\eta^R$ and ${\text{map}_F}^R$ and ${\text{map}_G}^R$. Assume $f : A \to B$ and $x : F\,A$.

To show:

$$ \text{map}_G\,f\,(\eta_A\,x) = \eta_B\,(\text{map}_F\,f\,x) $$

By identity extension for $G$, this is equivalent to

$$ G^R\,B\,B\,(\text{Id}\,B)\,(\text{map}_G\,f\,(\eta_A\,x))\,(\eta_B\,(\text{map}_F\,f\,x)) $$

Category law:

$$ G^R\,B\,B\,(\text{Id}\,B)\,(\text{map}_G\,f\,(\eta_A\,x))\,(\text{map}_G\,id\,(\eta_B\,(\text{map}_F\,f\,x))) $$

To show the above, we use ${\text{map}_G}^R$, i.e. that $\text{map}_G$ preserves all relations. We have to pick two relations, one in $\text{Rel}\,A\,B$ and one in $\text{Rel}\,B\,B$ and show that $f : A \to B$ and $id : B \to B$ are pointwise related. We pick the graph of $f$ and $\text{Id}\,B$, and the functions are clearly pointwise related. It remains to show:

$$ G^R\,A\,B\,(\text{Graph}\,f)\,(\eta_A\,x)\,(\eta_B\,(\text{map}_F\,f\,x)) $$

We know that $\eta$ preserves all relations, so it's enough to show:

$$ F^R\,A\,B\,(\text{Graph}\,f)\,x\,(\text{map}_F\,f\,x) $$

Category law:

$$ F^R\,A\,B\,(\text{Graph}\,f)\,(\text{map}_F\,id\,x)\,(\text{map}_F\,f\,x)$$

We instantiate ${\text{map}_F}^R$ with $\text{Id}\,A$ and $\text{Graph}\,f$ and it remains to show:

$$ F^R\,A\,A\,(\text{Id}\,A)\,x\,x $$

By identity extension for $F$, this is equivalent to:

$$ x = x $$


The same thing in Agda:

-- Agda 2.6.1, stdlib 1.5

open import Relation.Binary.PropositionalEquality
  renaming (sym to infix 6 _⁻¹; cong to ap; trans to infixr 5 _◾_; subst to tr)
open import Function

coe : ∀{i}{A B : Set i} → A ≡ B → A → B
coe refl a = a

Rel : Set → Set → Set₁
Rel A B = A → B → Set

Id : (A : Set) → Rel A A
Id A x y = x ≡ y

Graph : {A B : Set} → (A → B) → Rel A B
Graph f a b = f a ≡ b

happly : ∀{i j}{A : Set i}{B : Set j}{f g : A → B} → f ≡ g → ∀ x → f x ≡ g x
happly refl x = refl

record Functor : Set₁ where
  field
    !      : Set → Set
    map    : {A B : Set} → (A → B) → ! A → ! B
    map-id : ∀ {A} → map {A} id ≡ id
    map-∘  : ∀ {A B C}(f : B → C)(g : A → B) → map (f ∘ g) ≡ map f ∘ map g

record Functorᴿ (F : Functor) : Set₁ where
  private module F = Functor F
  field
    !     : ∀{A₀ A₁} → Rel A₀ A₁ → Rel (F.! A₀) (F.! A₁)
    map   : ∀ {A₀ A₁}(Aᴿ : Rel A₀ A₁){B₀ B₁}(Bᴿ : Rel B₀ B₁)
            (f₀ : A₀ → B₀)(f₁ : A₁ → B₁)(fᴿ : ∀ {a₀ a₁} → Aᴿ a₀ a₁ → Bᴿ (f₀ a₀) (f₁ a₁))
            {fa₀ fa₁} → ! Aᴿ fa₀ fa₁ → ! Bᴿ (F.map f₀ fa₀) (F.map f₁ fa₁)

    idext : ∀ {A} → ! (Id A) ≡ Id (F.! A)

  reflexive : ∀ {A x} → ! (Id A) x x
  reflexive {A} {x} = tr (λ f →  f x x) (idext ⁻¹) refl

module _
  (F G : Functor) (Fᴿ : Functorᴿ F) (Gᴿ : Functorᴿ G) where

  module F  = Functor F   ; module G  = Functor G
  module Fᴿ = Functorᴿ Fᴿ ; module Gᴿ = Functorᴿ Gᴿ

  module _ (η  : ∀ {A} → F.! A → G.! A)
           (ηᴿ : ∀ {A₀ A₁}(Aᴿ : Rel A₀ A₁){fa₀ fa₁}
                 → Fᴿ.! Aᴿ fa₀ fa₁ → Gᴿ.! Aᴿ (η fa₀) (η fa₁)) where

    η-is-natural : ∀ {A B}(f : A → B) x → G.map f (η x) ≡ η (F.map f x)
    η-is-natural {A} {B} f x =
      let lem1 : Fᴿ.! (Graph f) (F.map id x) (F.map f x)
          lem1 = Fᴿ.map (Id A) (Graph f) id f (ap f) {x} {x} Fᴿ.reflexive

          lem2 : Fᴿ.! (Graph f) x (F.map f x)
          lem2 = tr (λ y → Fᴿ.! (Graph f) y (F.map f x)) (happly F.map-id x) lem1

          lem3 : Gᴿ.! (Graph f) (η x) (η (F.map f x))
          lem3 = ηᴿ (Graph f) lem2

          lem4 : Gᴿ.! (Id B) (G.map f (η x)) (G.map id (η (F.map f x)))
          lem4 = Gᴿ.map (Graph f) (Id B) f id id lem3

          lem5 : Gᴿ.! (Id B) (G.map f (η x)) (η (F.map f x))
          lem5 = tr (λ y → Gᴿ.! (Id B) (G.map f (η x)) y) (happly G.map-id _) lem4

      in coe (happly (happly Gᴿ.idext (G.map f (η x))) (η (F.map f x))) lem5
$\endgroup$
5
  • $\begingroup$ I've been trying to understand this, but I cannot follow the Agda code. Could you at least give an informal explanation of the proof? That would be helpful. $\endgroup$
    – user56834
    Mar 10 at 6:09
  • $\begingroup$ @user56834 Edited the answer, I hope this helps. $\endgroup$ Mar 10 at 8:27
  • $\begingroup$ Thanks! some initial questions: 1. by a "proof-irrelevant relation" $\text{Rel} A B$ you simply mean a relation on sets $A$ and $B$ right? 2. By $F^R$ do you intend to refer to the relation belonging to the term $F$? i.e. the thing Wadler would write as $[[F]]\mathcal A$? (except that Wadler doesn't talk about terms of type $\text{Type}\to \text{Type}$) $\endgroup$
    – user56834
    Mar 10 at 11:09
  • $\begingroup$ @user56834 1. yes, it's just a relation. In type theory proof-relevant and irrelevant relations are often disambiguated. 2. If we have that $F$ is a type with a single free type variable, then $F^R$ is the "relation belonging to $F$", but it depends on a relation belonging to the single type in the context. A closed $F : \text{Type} \to \text{Type}$ is pretty much the same, modulo some universe sizes, which are not relevant now. $\endgroup$ Mar 10 at 11:35
  • $\begingroup$ I've tried to understand it, but I haven't been able to. Please see my bounty. $\endgroup$
    – user56834
    Mar 11 at 6:40
1
$\begingroup$

$\newcommand{\Type}{\text{Type}}\newcommand{\llb}{[\![}\newcommand{\rrb}{]\!]}\newcommand{\map}{\text{map}}$

Note: This answer is not a standalone answer, but an incomplete attempt to give some intuition for András Kovács's answer.

One important thing to point out is that is that type constructors are not always functors. In particular, the type constructor

$$F : \Type\to\Type\\ X\mapsto (X\to X)$$ is not functorial because there is no way to map a morphism $$f : A \to B \quad \overset{?}{\mapsto} \quad Ff : (A\to A)\to(B\to B).$$ So the theorem you mention only makes sense when $F$ is a functor. An attempt to generalize this statement to arbitrary type constructors requires generalizing categories, functors, and natural transformations to reflexive graph categories, relational functors, and parametric transformations (see section 6).


The parametricity translation is given for types as follows: $$\text{Rel} := \llb \Type \rrb^R = \Type \to \Type \to \Type$$ where it is then a (meta)-theorem of the parametricity translation that whenever $t : A$, then $$\llb t\rrb^R : \llb A \rrb^R(t,t)$$ where $\llb A\rrb^R(t,t)$ is the "free theorem", and $\llb t\rrb^R$ is the proof of this theorem.

In particular this means $$\llb A\to B\rrb^R: \text{Rel} (A\to B,A\to B)\\ \llb A\times B\rrb^R : \text{Rel}(A\times B,A\times B)$$ and we define $$\llb A\to B\rrb^R(f,g) = (x_0,x_1:A) \to \llb A\rrb^R(x_0,x_1)\to\llb B\rrb^R(f x_0,gx_1)$$ $$\llb A\times B\rrb^R(p,q) = \llb A\rrb^R(\pi_1 p,\pi_1 q) \times \llb B\rrb^R(\pi_2 p,\pi_2 q).$$

A similar definition can be given for dependent function, sum, and equality types, which I use below but I won't define them here. You additionally need to define $\llb\cdot\rrb^R$ for contexts and for terms. If you prefer, The Girard–Reynolds isomorphism (second edition) gives a more mathematical presentation of this translation.


So given a functor $F = (F_!,F_{\text{map}},F_{\text{id}},F_{\circ}) : \text{Functor}$ (as defined by András), we can apply the parametricity translation to get $$\llb F\rrb^R : \llb\text{Functor}\rrb^R(F,F)$$ In particular this means \begin{align*} \llb F_!\rrb^R &: \llb\Type\to\Type\rrb^R(F_!,F_!)\\ &= (A_0,A_1 : \Type)\to \text{Rel}(A_0,A_1)\to \text{Rel}(F_! A_0,F_! A_1) \end{align*} \begin{align*} \llb F_{\map}\rrb^R &: \llb (A,B:\Type)\to(A\to B)\to(F_! A \to F_! B)\rrb^R(F_\map,F_\map)\\ &=(A_0,A_1: \Type)\to(A^R :\text{Rel}(A_0,A_1))\to (B_0,B_1:\Type)\to(B^R :\text{Rel}(B_0,B_1))\\ &\quad\to\llb(A\to B)\to(F_! A \to F_! B)\rrb^R(F_\map (A_0,B_0),F_\map (A_1,B_1))\\ &=(A_0,A_1: \Type)\to(A^R:\text{Rel}(A_0,A_1))\to (B_0,B_1:\Type)\to(B^R:\text{Rel}(B_0,B_1))\\ &\quad\to(f_0 :A_0\to B_0)\to(f_1 : A_1\to B_1)\to \llb A\to B\rrb^R(f_0,f_1)\\ &\quad\to\llb (F_! A \to F_! B)\rrb^R(F_\map (A_0,B_0,f_0),F_\map (A_1,B_1,f_1))\\ &=(A_0,A_1: \Type)\to(A^R:\text{Rel}(A_0,A_1))\to (B_0,B_1:\Type)\to(B^R:\text{Rel}(B_0,B_1))\\ &\quad\to(f_0:A_0\to B_0)\to(f_1 : A_1\to B_1)\to \llb A\to B\rrb^R(f_0,f_1)\\ &\quad\to(x_0,x_1 : F_! A)\to \llb F_! A\rrb^R(x_0,x_1) \\ &\quad\to\llb F_! B \rrb^R(F_\map (A_0,B_0,f_0,x_0),F_\map (A_1,B_1,f_1,x_1)) \end{align*}

Where application is defined so that $$\llb F_! A\rrb^R(x_0,x_1) = \llb F_! \rrb^R(A_0,A_1,A^R, x_0,x_1)$$

This gives precisely the fields !,map for the Functorᴿ that András described. My guess is that applying this translation to $F_\text{id}$ should give a generalization of idext, but I have not yet figured out how to do this. Note that we could do the same for $F_\circ$, but it is not needed.


So now, given functors (actually they don't even need to respect composition, since $F_\circ,G_\circ$ are never used in the proof) $F,G : \text{Functor}$, and a map $\eta:(A :\Type)\to F_! A\to G_! A$, we obtain the following "free theorems": $$\llb F\rrb^R : \llb \text{Functor}\rrb^R(F,F)$$ $$\llb G\rrb^R : \llb \text{Functor}\rrb^R(G,G)$$ and $$\llb\eta\rrb^R : \llb (A :\Type)\to F_! A\to G_! A \rrb^R(\eta,\eta)$$

Since the formal construction of these terms is very messy, András instead assumes the existence of $F^R, G^R$, and $\eta^R$ of the appropriate type, and then derives that $\eta$ is a natural transformation, that is

$$A, B : \Type, f: A\to B, x:A\vdash G_\map(f,\eta(A,x)) = \eta(B,F_\map(f,x)).$$

$\endgroup$
2
  • $\begingroup$ I don't think we get identity extension from ${F_{id}}^R$. It's a trivial statement in the Atkey et al. paper, because it equates relational witnesses, which are proof-irrelevant, assuming that $\text{Type}$ is a small proof-irrelevant universe. If $\text{Type}$ is a larger Hofmann-Streicher universe, we still don't get anything like identity extension from ${F_{id}}^R$, plus in that case we don't get the right parametricity statements to begin with. $\endgroup$ Mar 14 at 19:32
  • $\begingroup$ @AndrásKovács I'm happy to assume $\text{Type}$ is proof irrelevant. I have not read this article, so I don't understand your comment yet. But my thought was that if $F_{id}^R$ did give identity extension, then the pair $(F,F^R)$ would give a relational functor in the sense of the article I linked, which seems very elegant even though I don't understand it. I asked a related question about this on cstheory. $\endgroup$
    – Couchy
    Mar 14 at 20:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.