Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: Benja Fallenstein <benja.fallenstein AT gmail.com>
  • To: Eugene Kirpichov <ekirpichov AT gmail.com>
  • Cc: Taral <taralx AT gmail.com>, coq-club <coq-club AT pauillac.inria.fr>, Haskell Cafe <haskell-cafe AT haskell.org>
  • Subject: Re: [Haskell-cafe] Re: [Coq-Club] An encoding of parametricity in Agda
  • Date: Thu, 24 Sep 2009 19:07:58 +0200
  • 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; b=deILhGpLTp9ebnK+2rUSACXAN37hY10TyRm15ny/gzVvlnh5RbtosbkV+OATrI6qQe GW6Za+BkIbCxm8O5OUjz42DHRSK98iYORcivb75cpSf2JlaCkfyzhbcQJoHFv90TT4KJ Uf1uLVHyWBJAIQjomsWmPikj5z5b+ikWWSX5A=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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



Archive powered by MhonArc 2.6.16.

Top of Page