When I get the opportunity to do research these days, it’s mostly focused on trying to formalize the abstract syntax, typing and operational semantics from the programming language’s point-of-view, not the logic’s point-of-view, once and for all. Once of the major problems is that the typing for Pola is complicated, much more complicated than typing systems I’ve done in the past. On the one hand this makes me very pleased with myself that I was able to get type inference going as well as I have, but on the other hand it’s a huge obstacle to getting other people interested in what we’re doing.

I apologize for the sloppy prose, but this is from a rough draft of notes I’m keeping for myself. The notation used in this typing rule is actually much simpler than what I’d had previously.

It’s horrendously confusing and yet, through many revisions, it’s the simplest and most straight-forward I’ve been able to come up with to describe what’s happening at the type level. Sometimes I think it would be easier to just show people the code instead of the sequents, ha!

Anyway, I shall keep at trying to simplify this stuff. It’s further emboldened the motivation I have for prettying of the “face” of this language for mortal users.