Three Dollar Quill

We'll see about actually taking proper notes tomorrow, but I have at least finally figured out how to read some of the paper correctly. I might as well lay that out, since I don't know what else I would write this entry about.

Here's the deal: 1ML's elaboration is divided into several parts, and the part that I think will end up changing the least as a result of my syntax/semantics changes is the subtyping system. Now, subtyping works on what are called semantic types, which are a subset of System Fω types. (I'm right now planning to represent them using helper classes that can convert back and forth between actual types, for various practical reasons.) In the 1ML papers, subtyping relates two semantic types (and sometimes a sequence of "paths", which are a particular kind of semantic type), and produces two pieces of information that are required for the elaboration: a sequence of type variable substitutions, and a coercion function in System Fω. The substitutions should be safe to use as presented, and the coercion function requires some light modification.

Basically, because I'm messing with call-by-push-value, I need to have the coercion function wrap a ReturnType around the, uh, return type. Then, the nested calls the paper gives can be replaced with sequencing.

Now, the part I'd been missing was how the substitutions are created, because I'd been misreading one of the rules. All substitutions ultimately derive from the "Sforget" rule, which equates a very specific form of path with a "small" type. The substitution given in the rule involves a type operation, and it wasn't until today that I realized that the type operation was inside the subsitution, rather than the other way around. Minutes of reading could have saved me hours of confusion. Anyway, the meaning of it was "So, you have a type variable that takes some number of types as arguments, here represented by type variables specifically; to unify this whole expression with a small type, replace the outermost type variable with a type function that takes all of those other type variables as arguments, and returns the small type". This substitution acts on the supertype, to make it compatible with the subtype.

Looking over what remains, I'm still not quite sure how "Sstr" divides up the path sequences, and I'm going to need to do some worked examples of effect subtyping, because effect encoding is something I intend to do differently than the paper, and it's going to need some form of coercion that I'll have to do some worked examples of, even though there are only three possible things that can even happen. Hopefully I'll have enough pep to work on that tomorrow.

Anyway, it's late, although not extremely late, and I want to go lie down.

Good night.