The Coq mailing list

[Samuel Gélineau <gelisam AT gmail.com>]

muad wrote:
> Seems to be writing out the proofs manually, unless I am confused? Not
> really free theorems if you have to prove them yourself.

You are correct, I am rewriting the function implementations into proofs manually.

My blog post wasn't supposed to be an Agda proof of parametricity (I don't think that's possible), but the outline of a proof of parametricity which happens to use Agda as an encoding for both functions and proofs.

If you want to prove parametricity formally, you still need to encode terms and types and proofs and propositions, and then write an induction proof, just like in Wadler's paper. And even then, your proof will convert term encodings to proof encodings, not proof-language terms to proof-language terms-which-happen-to-be-proofs. My contribution does not change this.

The first thing to notice is that if you encode all of this as one dependent language, instead of a language for terms and a language for proofs, then you can easily generalize parametricity to dependent languages, instead of just System F. But I don't think I'm the first to point this out.

My real contribution is to encourage you to abstract over all Set1s instead of focusing on the case Set# = relations. Then,
1) you get an even more general parametricity theorem, and
2) the induction proof gets easier (to the point where generalized parametricity seems intuitively true).


But since encoding dependent languages is hard, I don't think a formal proof of generalized parametricity is going to happen anytime soon. Meanwhile, I'm happy to just postulate it and see how many neat new results the generalization will yield.

– Samuel