[Haskell-cafe] Re: [Coq-Club] An encoding of parametricity in
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,
More information about the Haskell-Cafe