TApp?

[sgraf812]

This project is quite an instructive reference in a jungle of design decisions that need to be taken (PHOAS or not, etc.) in order to arrive at a working model of parametricity, thanks for writing it down.
However, I'm missing a data constructor for type application TApp. Was this a conscious omission?

[Lysxia]

I forgot TApp!

[sgraf812]

Wow, thanks so much! That was quick :)

Edit: Ah, but I see it's still WIP. Well, no pressure, really; I just wanted to know if there were known road blocks. Seems that there might be a few unknown road blocks, though...

[Lysxia]

Yeah it turns out I dodged the one difficult construct.

[sgraf812]

FWIW, https://github.com/yiyunliu/system-f-omega seems to be a more ambitious project and claims to derive parametricity for Fω without defining any axioms or impredicative set, which is nice. It looks a lot more involved than what I had hoped for, but if that is what it takes, so be it...