On Wed, Sep 23, 2009 at 6:46 AM, Eugene Kirpichov <ekirpic...@gmail.com> wrote:
> 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 <tar...@gmail.com>
"Please let me know if there's any further trouble I can give you."
-- Unknown
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
