An encoding of parametricity in Agda

[jkff]

Hi,

I've discovered the following post on the internets:
http://gelisam.blogspot.com/2009/09/samuels-really-straightforward-proof-of.html

It contains an ingenious (to my mind) encoding of parametricity in
Agda that makes the Free Theorems a trivial consequence.

I've tried to formalize it in Coq, but, as of now, with no success.

--
Eugene Kirpichov
Web IR developer, market.yandex.ru

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Taral]

On Wed, Sep 23, 2009 at 6:46 AM, Eugene Kirpichov <ekirpichov@...> 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.

--
Taral <taralx@...>
"Please let me know if there's any further trouble I can give you."
    -- Unknown

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[jkff]

Under parametricity, I mean the Reynolds Abstraction Theorem, from
which free theorems follow.
The encoding allows one to prove the theorem for any particular
function by implementing this function in terms of "relativized"
types.
The type of the relativized function is precisely an instance of
Reynolds theorem for it, and its implementation is a proof.

2009/9/23 Taral <taralx@...>:

> On Wed, Sep 23, 2009 at 6:46 AM, Eugene Kirpichov <ekirpichov@...> 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.
>
> --
> Taral <taralx@...>
> "Please let me know if there's any further trouble I can give you."
>    -- Unknown
>

--
Eugene Kirpichov
Web IR developer, market.yandex.ru

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Dan Doel]

On Wednesday 23 September 2009 12:21:00 pm Taral wrote:
> On Wed, Sep 23, 2009 at 6:46 AM, Eugene Kirpichov <ekirpichov@...>
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

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Benja Fallenstein]

Hi Taral, Eugene,

[Taral]
>> 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.

[Eugene]
> Under parametricity, I mean the Reynolds Abstraction Theorem, from
> which free theorems follow.

Would it help to say that the Abstraction Theorem states that every
*definable* function is parametric, whereas Taral's formula states
that *every* function of that type is parametric?

(Both concepts are useful; Agda presumably has models where Taral's
formula does not hold (if it's consistent, i.e. has models at all), so
that formula presumably isn't provable in Agda without additional
axioms.)

All the best,
- Benja

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[muad]

jkff wrote:

Hi,

I've discovered the following post on the internets:
http://gelisam.blogspot.com/2009/09/samuels-really-straightforward-proof-of.html

It contains an ingenious (to my mind) encoding of parametricity in
Agda that makes the Free Theorems a trivial consequence.

I've tried to formalize it in Coq, but, as of now, with no success.

--
Eugene Kirpichov
Web IR developer, market.yandex.ru

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

Seems to be writing out the proofs manually, unless I am confused? Not really free theorems if you have to prove them yourself.

[Samuel Gélineau]

muad wrote:
> Seems to be writing out the proofs manually, unless I am confused? Not
> really free theorems if you have to prove them yourself.

You are correct, I am rewriting the function implementations into proofs manually.

My blog post wasn't supposed to be an Agda proof of parametricity (I don't think that's possible), but the outline of a proof of parametricity which happens to use Agda as an encoding for both functions and proofs.

If you want to prove parametricity formally, you still need to encode terms and types and proofs and propositions, and then write an induction proof, just like in Wadler's paper. And even then, your proof will convert term encodings to proof encodings, not proof-language terms to proof-language terms-which-happen-to-be-proofs. My contribution does not change this.

The first thing to notice is that if you encode all of this as one dependent language, instead of a language for terms and a language for proofs, then you can easily generalize parametricity to dependent languages, instead of just System F. But I don't think I'm the first to point this out.

My real contribution is to encourage you to abstract over all Set1s instead of focusing on the case Set# = relations. Then,
1) you get an even more general parametricity theorem, and
2) the induction proof gets easier (to the point where generalized parametricity seems intuitively true).


But since encoding dependent languages is hard, I don't think a formal proof of generalized parametricity is going to happen anytime soon. Meanwhile, I'm happy to just postulate it and see how many neat new results the generalization will yield.

– Samuel

[Robert Atkey-2]

Hello All,

If anyone is interested, I have encoded a model of System F inside Coq
(+ impredicative set and some other axioms) that supports Reynolds style
parametricity and allows you to prove the properties such as the one
Taral mentioned---at least for System F types.

The model is set up so that every value in the denotations of the types
is parametric, and I proved that the obvious denotations of all System F
terms are in the denotations of the types.

The Coq development is available from:
  http://homepages.inf.ed.ac.uk/ratkey/parametricity

The Coqdoc "documentation" is just the code itself, but there is a short
two-page note on the formalisation and a paper about an application of
it to proving representation results for higher-order abstract syntax.
There are some slides linked from my homepage too.

Bob


--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club