The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

On Wednesday 23 September 2009 12:21:00 pm Taral wrote:
> On Wed, Sep 23, 2009 at 6:46 AM, Eugene Kirpichov 
> <ekirpichov AT gmail.com>
>  
wrote:
> > It contains an ingenious (to my mind) encoding of parametricity in
> > Agda that makes the Free Theorems a trivial consequence.
> 
> Perhaps I don't understand Agda very well, but I don't see
> parametricity here. For one, there's no attempt to prove that:
> 
> forall (P Q : forall a, a -> a), P = Q.
> 
> which is what parametricity means to me.

I've been playing with this, and the stuff in the post takes a bit of work to 
fully tease out. Working through the Theorems for Free paper along side the 
blog post should be helpful, but here's a fast version: ∀ A. A → A goes like:

  From a function from relations to relations Φ we get relations

    ∀α. Φ(α)

  where

    (φ, φ') ∈ ∀α. Φ(α) 
      iff 
    (A, A') ∈ α ⟶ (φ(A) , φ'(A')) ∈ Φ(R_A)

  or something close to that. And

    (f, f') ∈ α → α iff (x,x') ∈ α ⟶ (f x, f' x') ∈ α

  Parametricity states that:

    if f : ∀A. A → A then (f,f) ∈ ∀α. α → α

  And Theorems for Free goes on to suggest that using functions as the
  relations between two types gives us useful theorems. All together, this
  looks like:

    id : ∀A. A → A
    (id,id) ∈ ∀α. α → α   (parametricity)
  
    suppose f : B → C

    (id_B, id_C) ∈ f → f      (definition of the ∀ relation above)
    (x,f x) ∈ f               (functions as a relation)
    (id_B x, id_C (f x)) ∈ f  (definition of the → relation above)
    f (id_B x) ≡ id_C (f x)   (functions as a relation)

  which, cleaning up a bit gives:

    f ∘ id ≡ id ∘ f

  the free theorem for id : ∀A. A → A

So, that's how things are supposed to go (hopefully I got that roughly 
correct. I get a bit muddled with the types vs. relations on types and 
functions on both and whatnot). However, I don't think that Agda quite allows 
us to do all this. We can lift a function to one of these relations fine:

  record Set# : Set₁ where
    field
      A  : Set
      A' : Set
      A~ : A → A' → Set

  record value# (A# : Set#) : Set where
    open Set# A#
    field
      x  : A
      x' : A'
      x~ : A~ x x'

  Rel : ∀{A B : Set} → (f : A → B) → A → B → Set
  Rel f x y = f x ≡ y

  infix 40 _#
  _# : ∀{A B} → (A → B) → Set#
  _# {A} {B} f = record { A = A ; A' = B ; A~ = Rel f }

  _#'_ : ∀{A B} (f : A → B) → A → value# (f #)
  f #' x = record { x = x ; x' = f x ; x~ = refl }

But, what about parametricity? I'll define an alias for the relation of the 
type for identity:

  ∀A,A→A# : Set₁
  ∀A,A→A# = (A# : Set#) → value# A# → value# A#

  parametricity : (∀(A : Set) → A → A) → ∀A,A→A#
  parametricity id A# x# = record { x  = id (Set#.A A#) (value#.x x#)
                                  ; x' = id (Set#.A' A#) (value#.x' x#) 
                                  ; x~ = ? }

I don't think there's anything to be filled in for that ? unless we use some 
postulates. We can do it for 'id A x = x', but that's a specific function 
(which happens to be the only function with that type, but I don't think we 
can prove that), and the point of parametricity (I think) is that it gives us 
this fact for every function, based only on the type.

However, if we do take it as a postulate, we seem to be good to go:

  postulate
    param : ∀{B C} {x : B} {y : C} 
             (_~_ : B → C → Set)
          → (id : (A : Set) → A → A)
          → x ~ y → id B x ~ id C y

  parametricity : (∀(A : Set) → A → A) → ∀A,A→A#
  parametricity id A# x# = record { x  = id (Set#.A A#) (value#.x x#)
                                  ; x' = id (Set#.A' A#) (value#.x' x#) 
                                  ; x~ = param (Set#.A~ A#) id (value#.x~ x#)
                                  }

  module Free-id {A B : Set} (id# : ∀A,A→A#) (f : A → B) where
    -- (id,id') ∈ ∀α. α ⟶ α
    -- (x,y) ∈ f : A → B           f x ≡ y
    -- (id A x, id' B y) ∈ f       f (id x) ≡ id' (f x)

    -- id#          = (id,id')
    -- f #' x       = (x, y)
    -- id# (f #' x) = (id A x, id' B y)
  
    free : A → value# (f #)
    free x = id# (f #) (f #' x)

    free' : (x : A) → _
    free' x = value#.x~ (free x)

  free : ∀{B C}
          (f : B → C) (id : ∀ A → A → A) → (x : B)
       → f (id B x) ≡ id C (f x)
  free f id x = Free-id.free' id# f x
    where
    id# : ∀A,A→A#
    id# = parametricity id

voila! Of course, I took parametricity for only one fairly specific type. I'm 
not sure how to make it much more general, so one may have to end up taking 
quite a lot of postulates if one wants to work this way (or work in a 
language 
that actually has/lets you prove parametricity).

Hopefully I didn't steal the author's thunder too much.

Cheers,

-- Dan