[Haskell-cafe] An encoding of parametricity in Agda

Eugene Kirpichov ekirpichov at gmail.com
Wed Sep 23 09:46:44 EDT 2009


I've discovered the following post on the internets:

It contains an ingenious (to my mind) encoding of parametricity in
Agda that makes the Free Theorems a trivial consequence.

I've tried to formalize it in Coq, but, as of now, with no success.

Eugene Kirpichov
Web IR developer, market.yandex.ru

More information about the Haskell-Cafe mailing list