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

Benja Fallenstein benja.fallenstein at gmail.com
Thu Sep 24 13:07:58 EDT 2009

Hi Taral, Eugene,

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

> 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

All the best,
- Benja

More information about the Haskell-Cafe mailing list