Coding 2024-12-23
Okay, let's see what we've got here.
1ML defines a core language without type inference, which can be translated to System Fω. The paper I'm reading gives the typing rules for System Fω, so I'm currently figuring that the idea is to translate down to System Fω and type check it in that form?
Given that, my plan of attack looks something like this:
- Implement 1ML without effects.
- Extend it with aspects of F-ing modules that the 1ML paper leaves as an exercise for the reader.
- See what goes wrong if I attempt to implement row typing in the core language. (Reading ahead, I see that this was considered, and specific pain points identified.)
- Extend row typing to the point where it can handle what I have in mind for effects.
- Implement a basic form of tail-resumptive effects.
- Add further capabilities until I'm satisfied.
- Somewhere in there, try to handle predicates some way.
One thing that's fairly obvious to me, looking at the papers, is that I'll need to have some kind of trace or source map associated with the different translations, because an error in terms of System Fω would be entirely incomprehensible.
In any case, reading over the papers, I'm cautiously optimistic about integrating row types, but it may end up being the case that I end up hacking on System Fω instead of the 1ML core.
For now, though, I need to wind down.
Good night.