system-F icon indicating copy to clipboard operation
system-F copied to clipboard

Published 20 hours ago • verified publisher icon Lysxia

TApp?

Open sgraf812 opened this issue 8 months ago • 4 comments

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?

sgraf812 avatar Mar 16 '25 14:03 sgraf812

I forgot TApp!

Lysxia avatar Mar 16 '25 20:03 Lysxia

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...

sgraf812 avatar Mar 17 '25 06:03 sgraf812

Yeah it turns out I dodged the one difficult construct.

Lysxia avatar Mar 17 '25 08:03 Lysxia

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...

sgraf812 avatar Mar 17 '25 19:03 sgraf812