patternModerate
Rigorous proof that parametric polymorphism implies naturality using parametricity?
Viewed 0 times
naturalitypolymorphismparametricityimpliesthatusingparametricrigorousproof
Problem
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.
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.
Solution
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
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
Code Snippets
-- 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))) lem5Context
StackExchange Computer Science Q#136359, answer score: 12
Revisions (0)
No revisions yet.