Three Dollar Quill

All right, I didn't take any notes or touch any code, but I've got a working hypothesis about how the stuff I've been thinking about fits together:

Ascription in the 1ML sense is irrelevant to bidirectional typing, but not a big deal to implement. Furthermore, transparent sealing is also irrelevant, and confusing to implement, and also I'm still a little confused what the distinction is between transparent sealing and ascription. Anyway—oh. Okay, that's not transparent sealing, that's pure opaque sealing. That might be worth looking into later. Regardless, I can get by for now with impure opaque sealing, and that should fulfill the role of ascription in bidirectional typing. That said, pure sealing does sound good to look into later, in case I run into issues with function purity. Hard to guess whether I'll run into problems.

Anyway, reading over stuff about refinement typing has given me some things to keep in mind for choosing nodes, so here's my plan:

• Get a fresh set of notes on node syntax.
• Note likely changes to support algebraic effects.
• Review refinement typing.
• Decide whether to start with impure sealing, or to jump straight to pure sealing.
• Wait, dangit, if sealing is impure, and I'm doing bidirectional stuff, then all of the function definitions are going to be impure, probably.
• That's bad.
• Okay, anyway, if that reasoning holds, then I'm going to need to properly understand the principles of pure sealing. Reading about "Skolemization" always freaks me out a little, until I realize I somehow did it by accident.
• Anyway, I'm going to need to understand the nature of the pure sealing rewrite, because literally every new node I come up with is going to need to support it.

Here's how things look now:

• For each node, determine the types of the fields.
• For each expression-typed field, determine the typing direction.
• Determine the typing direction of all expressions.
• Bidirectionalize and work out pure sealing, in some order.
• Effect polymorphism.
• Algebraic effects.
• Refinement types.
• Front-end syntax.

Anyway, I desperately need to get to bed, so I'll get back to this at some point in the next few days.

Good night.