Three Dollar Quill

I've come to the conclusion that I was probably misinterpreting something in the last post, but I'm not totally sure what. I'm seeing that it could be that some of the stuff I thought was true about sealing in 1ML was a result of the syntactic sugar, rather than an inherent quality of sealing versus ascription. Unfortunately, this means I'm back to not being sure what the difference between sealing and ascription is.

I'm reading over a bunch of stuff, but it's not making things clearer, and some of it looks really scary to implement.

Let's take one last stab at this before I get ready for bed...

The difference would seem to matter in the context of a structure containing a type variable, and another type derived from that variable. If ML ascription and bidirectional ascription are the same thing, and distinct from sealing (I'm starting to feel very skeptical of this), then we have... I got the context wrong. If we have a functor, let's say that takes a type, and returns a record type, which we use ascription to coerce to type type. Does such a coercion result in inferring impure type for the functor? I believe I understand why sealing results in an impure type in this context. Sort of. And the sugar version of ascription produces a pure function which is instantiated with the relevant types, and, hm. That is indeed a pure function that somehow "exposes" the argument.

What it comes down to, then, is the question of whether I need sealing for semantics, and ascription for bidirectional typing, or if a slightly modified version of sealing would handle both use cases. One thing that complicates the question is that they have the same behavior on concrete types, so asking questions about how to handle weird type constructs is required to develop a proper idea of what's going on.

Anyway, it's late and I'm probably confused about something. I'm going to go lie down.

Good night.