Coding 2025-08-25
Okay, everything type-checks once again. And by "everything", I mean "everything in the src directory". If I check the tests...
Found 150 errors in 2 files (checked 6 source files)
:)
Is that bad?
Shut it.
Anyway, while I could just barge in and start spot-fixing things until it passes and sort of makes sense, now would be a really excellent time to ponder the ergonomics of these syntax trees. Things to ponder include:
- I realized that requiring bidirectional typing to always be valid doesn't work under reduction (and, fair point, the paper stated this and I just ignored it until the pain was obvious), but... suppose I had a parallel set of types just for constructing the tree, which could then generate the tree meant for typing and reduction, and have it guaranteed that the tree would at least generate a specific error rather than just... giving up.
- Working in possibly the opposite direction, the syntax for constructing a tree right now is painfully verbose. And I don't have a clear idea of what to do about that.
- If I do have two tree structures, perhaps I can generate one from the other somehow.
- Alternatively, I'm a little tempted to see if building the tree from a concatenative language would make things nicer, but I doubt it.
Anyway, I took way longer with this writeup than I planned, so I've just got to cut it off now.
Good night.