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

Eugene Kirpichov ekirpichov at gmail.com
Wed Sep 23 12:30:28 EDT 2009

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

More information about the Haskell-Cafe mailing list