[Agda] Polymorphism is not (always) naturality

[Andrea Vezzosi]

Oh, by folklore I mostly meant that it's a popular notion, not that
there isn't a solid result behind it.

However most of the work on parametricity is done in the context of
languages derived from System F where you do not have universes or
Sigma types.

Relational parametricity makes sense for dependent type theory too,
but some of the intuitions don't transfer over from System F so
easily, it seems.

Best,
Andrea

On Tue, Oct 6, 2015 at 12:30 PM, Harley Eades III
<harley.eades at gmail.com> wrote:
> Hi, Andrea.
>
> I do not know much about parametricty at the dependently typed level.
> I haven’t studied it much.
>
> However, I would like to point out that the notion of parametricity and
> its relation to natural transformations is more than folklore.
>
> It goes back to John Reynolds one of the best PL researchers.  See:
>
> http://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf
>
> For some history on the subject.
>
> Very best,
> Harley
>
> On 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
>
>