[Agda] Polymorphism is not (always) naturality

[Dan Doel]

No need for sigmas or tricks with identity types.

----

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