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

[Eugene Kirpichov]

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 at gmail.com>:
> 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.
>
> --
> Taral <taralx at gmail.com>
> "Please let me know if there's any further trouble I can give you."
>    -- Unknown
>



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