Three Dollar Quill

All right, let's take stock. I'm improving my understanding of 1ML, and I'm getting a general handle on refinement types, and that's making me think that it might make sense to work on refinement types before algebraic effects. This is because algebraic effects (or at least the implementation I'm looking at) want sum types to exist, but don't really have strong constraints on the design, while refinement types have a bunch of things to say about sum types, some things that I don't yet fully understand...

I've got some things that I'm pondering about refinement types in general. It's talking about stuff like the type of an ordered list, and I'm wondering if it's possible to express "is an ordered list" as a predicate using the grammar specified in this tutorial, because I think I would prefer "refinement of generic type" to "bespoke type that happens to have the same representation".

Anyway, some stuff that I've been thinking about but haven't written down. Of the expression elaboration rules in 1ML, the big ones to make sure I haven't broken them in my attempts to bidirectionalize are Eapp, Eseal, Ewrap, and Eunw. In each case, there is a variable (two, in the case of Eapp) that I'm replacing with an expression. This removes the implicit binding that was putting the rest of the program or module inside the existential. At a glance, the effects of this look mostly safe, though I need to take another look at Eseal. But Eapp...

Existential types on the "function" type in Eapp shouldn't be a big deal, but the problems come in when I tried to replace explicit subtyping with a checking judgment. It looks to me like one of the consequences of this is that abstract types on the "argument" get bound "inside" the function call, rather than "before" it, which I don't think really matters, but it is a difference. The big difference that has me questioning things is that I guessed(?) that the way to handle universal types was to convert them to an abstraction attached to the parameter type; the argument is then checked against this new type, creating an expression of the new type, which encodes type information from the argument, in a form that should be accessible to the rest of the function application.

The main thing I'm now understanding is that, unlike how I was thinking of things, the structure of a function really does determine how it has to be called, so that (at least in the context of the explicit version of 1ML), generic functions need to be called with proper type arguments, so that the first argument to a polymorphic identity function has to be a type to specify which type it is the identity of. If I'm going to figure out a way to make this nicer, it's going to be solely within the realm of 1ML, since algebraic effects don't have any bearing on this, and in this context, the refinement types paper I'm reading explicitly does not specify how types should be inferred.

Anyway, I'm still not totally sure my ideas for function application are valid, and I'll be legitimately surprised if I've written the correct elaboration for them, but if this works, I can finish specifying things, and then either work on phase polymorphism, or investigating whether I want to beef up type inference in some manner.

For now, though, I'm sleepy and want to wind down, um, a few minutes ago.

Good night.