[Agda] Polymorphism is not (always) naturality

[Andrea Vezzosi]

On Thu, Oct 8, 2015 at 7:07 AM, Dan Doel <dan.doel at gmail.com> wrote:
> No need for sigmas or tricks with identity types.

Ah! I did consider the constant functor into Set, but I didn't
consider that you could just return the quantified type.

About free theorems involving universes, there's a DSL to get the
right type for the abstraction theorem:

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.LightweightFreeTheorems

In case of a function Set -> Set -> Set it just tells you that it also
maps relations to relations.
But that DSL will only give you naturality from parametricity for
concrete functors, since it doesn't tell you how the relational part
of a functor compares with equality.

If you use the model from this paper and interpret Set as the universe
of discrete reflexive graphs, then you also know that it sends the
equality relation to the equality relation. There you can get
naturality results for functors over that universe.

http://bentnib.org/dtt-parametricity.html

I would say that phi and functions Nat -> Nat -> Nat are actually
parametric, but while we could argue that functions Nat -> Nat -> Nat
are also natural since Nat is the discrete category, we don't get the
same for phi.

The irrelevance modality seems appropriate here because naturality is
the same as constancy, but it might be too strong in general. It does
seem like we need a modality though.

By the way, you can actually have dependent irrelevant quantification now.

Cheers,
Andrea



> ----
>
> module AntiNatural where
>
> open import Data.Empty
> open import Data.Unit
> open import Function
> open import Relation.Binary.PropositionalEquality
>
> F : Set -> Set₁
> F A = Set
>
> map-F : ∀{A B} -> (A -> B) -> F A -> F B
> map-F _ C = C
>
> phi : ∀{A} -> F A -> F A
> phi {A} _ = A
>
> module Contradiction
>     (natural : ∀{A B} (f : A -> B) (e : F A) -> phi {B} (map-F f e) ≡
> map-F f (phi {A} e))
>   where
>   lemma : ⊤ ≡ ⊥
>   lemma = natural ⊥-elim ⊥
>
>   void : ⊥
>   void = subst id lemma _
>
>   supplemental₁ : (A : Set) -> A ≡ ⊥
>   supplemental₁ A = natural ⊥-elim ⊥
>
>   supplemental₂ : (B : Set) -> ⊤ ≡ B
>   supplemental₂ B = natural (const _) B
>
>   supplemental₃ : (A B : Set) -> A ≡ B
>   supplemental₃ A B =
>     trans (supplemental₁ A)
>       (trans (sym lemma) (supplemental₂ B))
>
> ----
>
> I don't really remember how parametricity is defined when universe
> hierarchies are involved (actually, I don't remember if I've ever seen
> a work-up of such a thing). `natural` is the typical free theorem you
> get from parametricity, though, so it can't look anything like that
> for this example. And when you consider that the type of `phi` is
> really `Set -> Set -> Set`, it's not surprising. We have no reason to
> assume that functions of type `Nat -> Nat -> Nat` are parametric in
> their first argument, either.
>
> This actually gives a motivation for (dependent) irrelevance, even for
> types like Set which can't be 'inspected'. For instance, `phi` cannot
> be given the type `.Set -> Set -> Set`, nor would it allow the
> equivalent type `.(A : Set) -> F A -> F A` (supposing that kind of
> type were allowed). I would conjecture that functions with that type
> are natural transformations (and parametric in the first argument).
>
> -- Dan
>
>
> On Tue, Oct 6, 2015 at 4:24 AM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
>> It is FP folklore that polymorphic functions of type
>>
>> (a : Set) -> F a -> G a
>>
>> correspond to natural transformations via parametricity.
>> (Assuming F and G are "Functor"s)
>>
>> So it was a bit surprising to me that the result fails in dependent type theory.
>>
>> open import Data.Product
>> open import Data.Unit
>> open import Data.Empty
>> open import Data.Bool
>> open import Relation.Binary.PropositionalEquality
>>
>> S : Set → Set₁
>> S X = Σ Set \ R → R → X
>>
>> mapS : ∀ {X Y} → (X → Y) → S X → S Y
>> mapS f (R , g) = (R , \ x → f (g x))
>>
>> eta : ∀ {X} → S X → S X
>> eta (R , g) = (Σ R \ r → ∀ r' → g r ≡ g r') , (λ x → g (proj₁ x))
>>
>> postulate
>>   eta-nat : ∀ {X Y} → (f : X → Y) → ∀ s → eta (mapS f s) ≡ mapS f (eta s)
>>
>> counter : ∀ {X : Set} → eta (mapS (λ _ → tt) (X , (λ x → x)))
>>                       ≡ mapS (λ _ → tt) (eta (X , (λ x → x)))
>> counter {X} = eta-nat {X} {⊤} _ (X , (λ x → x))
>>
>> empty-sigma : Σ Bool (λ r → (r' : Bool) → r ≡ r') → ⊥
>> empty-sigma (b , p) with p (not b)
>> empty-sigma (true , p) | ()
>> empty-sigma (false , p) | ()
>>
>> impossible : ⊥
>> impossible = empty-sigma (subst (\ x -> x) (cong proj₁ (counter {Bool}))
>>                                 (true , (λ _ → refl)))
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda