Three Dollar Quill

Okay, I took a closer look at the problems I was seeing with my modifications to 1ML, and found... more problems. The top-level goal is, I want bidirectional typing because, as I understand things, that will help support refinement types. My initial plan was to "just" bidirectionalize 1ML elaboration, but it turns out that before I do that, I need to render it bidirectionalizable.

Here's what I mean: 1ML defines most of its expression nodes using variables rather than expressions, and provides syntactic sugar to implement ascription, and versions of nodes with expressions instead of variables. This is problematic for bidirectionalization because it limits the opportunities for checking; my general goal was to replace explicit subtyping checks with checking-based elaboration.

Now, my original plan was to make all of the changes I thought I needed, but that turns out to be difficult, because expressions and variables kind of behave differently. Or rather, some expressions type "like variables", and some don't. See, one of the distinctions that 1ML draws between types is "abstracted" versus "concrete" (I'm not sure if the paper uses "concrete" in this sense; it's been... a while since I read the whole thing closely). Variables and a few other expressions have "concrete" types, while generic expressions may have "abstracted" types. The difference is that "abstracted" types associate some number of existentially quantified type variables to a "concrete" type. This means that, when replacing a variable with a generic expression, in an elaboration rule, this means that suddenly there are a bunch of extra type variables that need to be accounted for.

For an example of this, if I'm understanding things properly, the major difference in behavior between ascription and sealing is that ascription entirely replaces the existential quantifications in the wrapped value, while sealing combines all of the existential quantifiers from the value and the type.

This kind of thing happens in a few other contexts, and seems to mean that I want to find some way of having a term synthesize its existential quantifiers, but check its concrete type. Now, it does look like I also want to be checking full abstract types in other contexts, so it kind of looks like I want three methods instead of two, maybe.

So, in order to have bidirectional elaboration, I first need to define the purely synthesizing elaboration for the nodes that I want to have. Then, I can figure out how to reverse some of the arrows. I could do that right now, but I don't feel like it, so I'm going to wrap up and find something else to do before bed.

Good night.