Coding 2026-03-19
Okay, now that I'm figuring out how 1ML actually works, I'm seeing how I messed up in my attempt to bidirectionalize it. I'm fairly sure that the way I was thinking of implementing function application would have done it in a way not visible to the type system, which defeats the point.
So, to try to make things work properly, I'm going to put together some requirements that my version of elaboration has to satisfy:
- Synthesizing judgments should produce identical types and elaborations
- Checking judgments should accept the same types, and "pure" judgments should be extended to impure judgments in the obvious way, given an abstracted type.
- Because checking can't jump into the middle of the subclassing machinery, this has to be accomplished by destructuring and reworking the elaborations from checking terms.
- Efun will require some minor improvements to handle abstraction.
- Eapp will need a comprehensize overhaul to "fake" accessing the type substitutions.
- Eseal might be fine, but need to check.
- Ewrap cannot replicate its semantics unless it keeps on using the full sugar; unclear whether this is a problem.
- Eunw should be fine if Eseal is fine.
Actually, let's see if I'm getting Ewrap right. To actually replicate the semantics, we'd need to accept abstracted value wrapper types, and the abstractions would allow us to interact with the wrapped expression as if it had a concrete type, by, um, hm. Quite aside from the fact that my current draft of the elaboration has some trivial issues I can fix up, for the rest of it, I really need to consider just how load-bearing the precise semantics are, because I've thoroughly confused myself at this point.
...
Given that I'm already carving out an exception for if expressions to match what refinement types want, I don't feel bad saying that Ewrap keeping the old semantics is on the table, even if it does make the bidirectionalization in that context a little pointless.
So, where things stand now is, I could work on cleaning this all up, but I feel like I really need to take a break for a few days. Not sure how I'll accomplish that, but I feel it's what I need to do.
First thing I can do in service of that is finishing up this entry on a reasonable time frame. No reason to draw it out further.
Good night.