[Agda] Polymorphism is not (always) naturality

[Harley Eades III]

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 <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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151006/22745d5f/attachment.html