Parametricity theorems in functional programming II
The usual story of parametricity is given in the paper "Theorems for free" by Wadler. https://ecee.colorado.edu/ecen5533/fall11/reading/free.pdf
In that paper, the exposition of the actual parametricity theorem is very terse and difficult to understand. It is based on the idea of replacing functions by "relations". So, we first need to learn how to work with relations between types and relations between values. Then, we need to prove that any program t of type T is in a a certain relation with itself, where the relation is generated by the type T. The paper does not actually show a detailed proof of that theorem; it just says that we need to perform induction on the typing rules.
After finishing the proof for a relation, we are still not done; we need to specialize a relation to a function in some way. The theorem does not say how to do that; it seems we have to guess that, and we are not guaranteed to get a useful law.
I tried to prove the parametricity law directly. A parametricity law has the form of naturality law for a dinatural transformation. All terms in simply typed lambda calculus are dinatural. Initially I thought that the proof would just work easily by induction on the term structure, just like Wadler's paper said. But when I started to write up the proof, I found that I cannot prove 2 induction cases out of 9. I started digging around and found that the proof cannot actually go the way I thought. Dinatural transformations do not compose, but my proof would have needed their composition when I consider the "cut" rule (application of a function to an argument). So, I'm stuck for a good reason.
This paper seems to be the most promising way out: https://www.researchgate.net/publication/221442794_Dinatural_Terms_in_System_F
Another one by the same author:
https://www.irif.fr/~delatail/param.pdf
In that paper, the exposition of the actual parametricity theorem is very terse and difficult to understand. It is based on the idea of replacing functions by "relations". So, we first need to learn how to work with relations between types and relations between values. Then, we need to prove that any program t of type T is in a a certain relation with itself, where the relation is generated by the type T. The paper does not actually show a detailed proof of that theorem; it just says that we need to perform induction on the typing rules.
After finishing the proof for a relation, we are still not done; we need to specialize a relation to a function in some way. The theorem does not say how to do that; it seems we have to guess that, and we are not guaranteed to get a useful law.
I tried to prove the parametricity law directly. A parametricity law has the form of naturality law for a dinatural transformation. All terms in simply typed lambda calculus are dinatural. Initially I thought that the proof would just work easily by induction on the term structure, just like Wadler's paper said. But when I started to write up the proof, I found that I cannot prove 2 induction cases out of 9. I started digging around and found that the proof cannot actually go the way I thought. Dinatural transformations do not compose, but my proof would have needed their composition when I consider the "cut" rule (application of a function to an argument). So, I'm stuck for a good reason.
This paper seems to be the most promising way out: https://www.researchgate.net/publication/221442794_Dinatural_Terms_in_System_F
Another one by the same author:
https://www.irif.fr/~delatail/param.pdf