Coding 2026-02-04
I got distracted from improving the code, by the question "Hey, what obstacles are there to using this implementation as a substrate for all of the higher-level features I want?" Right now, I'm focusing on the module language, because that's directly based on System Fω, and my implementation of it is... eccentric. As I recall, refinement typing is going to somehow tie into bidirectional typing, and algebraic effects is somehow going to come from call by push-value, and I've got those, so the major question is whether the tweaks that those two inspired me to make to System Fω will be a problem or not.
Ultimately, I've got a mixture of concrete goals and open-ended questions. Concrete goals include:
- Provide additional implementations of Variable, in order to represent higher-level identifiers.
- Provide additional implementations of Label, in order to represent variables.
Open-ended questions include:
- The core semantics I want differ from traditional ML. Does this present any problems for adapting 1ML? Is there any chance this makes the implementation easier?
- My implementation of System Fω is sort of impredicative. Is this enough for F-ing Modules?
- The 1ML paper combines elaboration and typing; what does an implementation of this look like, especially given that I'd ideally like to still be emitting constraints?
I want to get a better grasp on the open questions, before working on the concrete goals, which should be pretty simple. I'm going to get off my laptop and try to make some progress there.
Good night.