Three Dollar Quill

I didn't have proper internet for about two days there, so I've been closely reading over the 1ML paper. My goal was to create a blueprint for a 1ML-like language that fits naturally on top of the somewhat idiosyncratic version of System Fω I've been building up. This means supporting bidirectional typing, which is straightforward in some respects, but getting it right will require a better understanding of 1ML subtyping than I currently have. It also means supporting call-by-push-value, with the restriction of type variables to ranging over value types. I think if I can get that restriction working in this context, then I have a good chance of carrying it forward into the planned semantics.

My ideas for how to resolve this may break something, so let's try to pin down exactly what I have in mind here.

The obvious difficulty in reconciling 1ML with call-by-push-value is that 1ML terms are in some ways obviously values, and in other ways obviously computations, sometimes containing both conclusions in a single node. Call-by-push-value should have something to do with "purity", but the encoding of purity in the context of elaborating 1ML, using record types with reserved labels, to me just further obscures what this should represent.

So, I intend to try replacing these record types with specific transformations in the context of call-by-push-value. The key thing that rests at the center of my approach is noting that 1ML programs must elaborate to complete call-by-push-value programs; in other words, computations, not values. At the same time, the semantic types that guide the elaboration are associated with variables in the environment, which strongly suggests that they should be value types. Furthermore, many semantic types involve computation types, so the obvious resolution is to do something with thunk types.

Now, what makes this interesting is to notice the parts of the elaboration that definitely correspond to computation purity. These represent some but not all of the contexts where the type "should" represent a computation instead of a value. There are two purity annotations (pure and impure), and two "obvious" ways to convert a value to a computation (return and force).

What got this to make sense to me was to consider the pure and impure function types, and what their usage should correspond to in call-by-push-value. In 1ML, a multi-parameter function corresponds to several chained pure functions, ultimately returning either an impure function, or a pure function returning a base value. In call-by-push-value, a multi-parameter function corresponds to functions reducing to functions, until it reduces to a return type. What this suggests to me is that "purity" corresponds to forcing a thunk, and "impurity" to returning, and that the representation of a base type is a thunk of a return of a base type.

This all feels like it will accomplish something, but there are various questions that I haven't addressed yet, such as:

• What's the proper semantic type representation for nested universal types?
• What about record types?
• Should I be working with higher-level representations of semantic types, or could it work to manipulate System Fω types directly? One point of confusion here is looking at limitations of the representation, and distinguishing bugs from features. Like, I can't convert a type variable into a pure computation in the context of typing; but is that a problem, or something I shouldn't even be trying to do?

Anyway, rather than try to write more, I'm going to publish this early and take another shot at understanding subtyping.

Good night.