The current work on SOFP

[winitzki]

At the moment, I am working on rewriting Appendix D. I realized that Chapter 13 will need some more parametricity results than were already available in Appendix D. Specifically, I need to prove "strong dinaturality" whereas before Appendix D only proved ordinary dinaturality.

As a result, I am expanding Appendix D to include a full proof of relational parametricity and strong dinaturality. I am following the talk slides here: http://www.ioc.ee/~tarmo/tday-voore/vene-slides.pdf which seems to be a paper that was never written out. I contacted Professor Varmo Vene about this, but he did not respond.

I realized that proving relational parametricity is actually a lot easier than proving dinaturality. Since I already have a proof of dinaturality, why not include a proof of relational parametricity? Also, I hope my approach will be easier to follow and closer to applications than the standard Reynolds-Wadler approach.

I will not include the difficult derivation of dinaturality from parametricity; this is done in Voigtländer's paper here, https://arxiv.org/pdf/1908.07776.pdf
However, the derivation in that paper is quite complicated and not easy to follow. I have no time now to figure out an easier approach to deriving his result.

[winitzki]

The work on rewriting Appendix D is complete.

[winitzki]

I found serious errors in Appendix D and spent about 3 months rewriting it yet again. The rewrite is complete.