Parametricity theorems in functional programming
I'm trying to find a simple proof of parametricity theorems, without using relations. I hoped that I can use dinatural transformations https://en.wikipedia.org/wiki/Dinatural_transformation directly and prove that any purely functional code of type P[A, A] -> Q[A, A] is a dinatural transformation. However, after starting to write up a proof, I ran into a snag: dinatural transformations do not compose. For example, this paper shows some conditions for them to compose https://drops.dagstuhl.de/opus/volltexte/2018/9700/pdf/LIPIcs-CSL-2018-33.pdf But it seems that I can't restrict programs to those conditions. So I'm stuck.