[Haskell-cafe] Re: [Coq-Club] An encoding of parametricity in Agda

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 :

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

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