Coding 2026-03-07
All right, I'm back to thinking about bidirectionalization. Basically, there are several rules from 1ML that I want to bidirectionalize, and I'm not totally sure whether that's actually workable. The rules are:
- Eif; I want to make it checking instead of containing an ascription
- Efun; I want to make it checking
- Eapp; I want to make it operate on expressions, and make the argument checking
- Eseal; I want to make it operate on an expression, and make that expression checking
- Ewrap; I want to make it operate on expressions, and make both the overall node and the argument checking
- Eunw; I want to make it operate on expressions, but only the overall node can be made checking; the argument actually has to synthesize
And, like, I could just do this, but switching from sugar to "the node actually contains expressions" has consequences for typing that I'm not sure of the impact of. And these consequences only manifest in the context of "doing something with modules". Basically, in the context of the 1ML sugar, if an expression has existential type, then the pack statements get wrapped around the node's type, whereas with what I'm trying to make work, type checking doesn't send the packing back up, which I think means that stuff like sealing has to "know" about existential types which would simply be inferred under the pure synthesis paradigm. If I'm understanding this correctly, I'm then not sure about the actual consequences that this has for usability. Basically, how much of a pain is it to type functors in this paradigm?
Or, I guess, it's a matter of questions of usability, but also whether there are inferrable types that cannot be expressed explicitly? Well, always, the only way to introduce an existential type is through the type type. Now, I think for an expression to supertype a type involving an existential type, in the context of synthesis, the expression would have to reference the variable bound to the existential type itself. So, if we move the expression out of the existential, then it basically needs to just duplicate the relevant existential bindings. If I'm thinking about this right, it doesn't seem too onerous.
Well, that was some good thinking. I'll try to make more updates to my notes tomorrow, but right now I just want to take things easy.
Good night.