Coding 2026-02-18
Okay, so, I'm trying to work on notes because I know if I just type in more code now, it'll be chaos, but I'm having trouble getting things formatted nicely; like, am I going to have to just take pictures of handwritten notes? Either way, I'm trying to avoid any large leaps, so here's the deal:
- To start with, the 1ML syntax from the paper.
- Plus support for first-class modules.
- Now, adapt this to bidirectional typing, with some variables replaced with expressions, and note where using expressions complicates the elaboration logic (Eapp and Eseal, principally).
- Now, make the changes required to support effect polymorphism, but not defining arbitrary effects.
- Add the nodes and updates needed for algebraic effects. Note that aesthetics/symmetry indicate that it may be meaningful to speak of "large" vs "small" effects. At this point, I want to figure out whether any more work is required to support modular implicits, or if it's possible to support them via effectful functors.
- Add or update as needed to support refinement types. Getting basic functionality is hopefully sufficient to replace the concept of "unsafe", but I also want to know whether the type-directed aspects of elaboration can create specializations of functions that explicitly lack effects, based on some kind of annotation.
I think in order to make progress here, I need to devote more work on Impliciula fully to taking notes and planning, and switch to another project when I want to actually write code. (Perhaps I could get back to increasingly-delayed Conlang Year?)
Anyway, I need to wind down now, so I'll call things here and try to get something more satisfying done later.
Good night.