Three Dollar Quill

All right, let's see. I've got rough drafts of all of the basic expression typing rules. Convincing myself that I've got convincing typing rules is a lot easier than getting the elaborations to look good. It's also been a pattern that the bidirectionalized typing can look more elegant by some standards, but the resulting elaboration is more of a mixed bag.

The big thing missing is a proper re-interpretation of the purity annotations. The more I think about it, the more the whole thunk-return instead of record thing just seems like stubbornness. I'll have to consider whether I keep on with that, or just do what the paper says. Of course, it is possible that the real answer is "just focus on the monad behavior, and the actual implementation is just a detail".

Regardless, I let it get late, and I have to go to bed. I'll maybe take a break from this for a few days; we'll see.

Good night.