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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe