23 Sep
2009
23 Sep
'09
12:21 p.m.
On Wed, Sep 23, 2009 at 6:46 AM, Eugene Kirpichov
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