Three Dollar Quill

Okay, I let time get away from me again, but hopefully not as badly this time. Having reviewed the literature on extensions to 1ML, and implementing algebraic effects, I've reaffirmed that there's no good way to skip ahead in implementing things.

Here's my current short-term plan:

• Rewrite the 1ML elaboration rules in a form that does more to permit/require bidirectionalization.
• Specialize the semantic types to my weird finicky System Fω variant.
• Implement it all.
• Write tests based on all applicable code snippets.
• Given what I've learned from this, plan out the next steps.

For now, I need to get to bed and hope I'm better rested tomorrow.

Good night.