Three Dollar Quill

Slight update to yesterday: "Wait, 1ML sealing is pure under many circumstances, so there's a chance I don't need to try to get it pure in every circumstance."

In any case, now I'm trying to go through the elaboration judgments and modify and bidirectionalize them, and one of the early-on judgments is for function types, which ended up getting me distracted thinking about how to handle effects. My hunch currently is that I want to have two total rows instead of just one; one for "pure" and one for "impure". Although, this could lead to some weird issues, so I'm not committed to it. Another possibility is simply that purity and other effects are simply tracked in the same data structure, but in separate fields. The key thing is the semantics of effects, which must somehow make various changes to a function type.

I've been struggling to understand this better and have something else to say, but it's late, I'm tired, and I don't think I'm going to get any further tonight.

Good night.