Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] An encoding of parametricity in Agda

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: Eugene Kirpichov <ekirpichov AT gmail.com>
  • To: Taral <taralx AT gmail.com>
  • Cc: Haskell Cafe <haskell-cafe AT haskell.org>, coq-club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] An encoding of parametricity in Agda
  • Date: Wed, 23 Sep 2009 20:30:28 +0400
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=oCOCScAKa26wS7j1Av5hm05W/Nf8gglTyztMXRDgchBU+6BsOTmQRCs3aEB3HOn09y 7zIKVEtWmdcBTNb7pNpZ6imVt/Iy/sce8AVs9JF5Oa/eh+ptR+qyByjrVnXmTWHKJFfi qRMnsAzztifkO6Iw1POAcZ+qHRQG6zlnE5Lrg=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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



Archive powered by MhonArc 2.6.16.

Top of Page