Three Dollar Quill

As I said yesterday, I decided to actually properly implement subsumption. This will allow me to do stuff like avoid cascading errors when a coercion fails, so the user can focus on whatever caused the coercion to fail.

Now, this isn't really a snap-my-fingers deal. What I'm very confident of is as follows:

• The parameter type of a function type is contravariant.
• Most other types are covariant, probably including universal and existential.
• Some types are apparently invariant, but I'm a little confused there.
• Kinds don't have variance, so call them invariant.

Now, subsumption, in terms of the behavior of my code, is only relevant when a synthesizing node is checked. In the default implementations I wrote, the synthesizing node synthesizes, and then we check that the passed-in value subsumes the synthesized value. Currently, both of these values could contain or be failing node, just according to the Python-level type annotations. Let's see if we can find examples of both possibilities. Hm. If a function node is checked against an incompatible type, the body will definitely be checked against a failing node, and may synthesize a failing node. And if a node synthesizes a failing node, and is wrapped in an ascription, then it's the other way around. Well, that's inconclusive.

Anyway, there's some other things I wanted to check. Because of ascriptions, synthesis has to happen before reduction. This is only relevant for higher-kinded types. As it stands, this means that synthesizing the kind of an operator application may fail if it's partially reduced before synthesis, but, um, partial reduction indicates that typing failed, so the biggest concern here is whether the failure message ends up being confusing. In general, I believe we want to always check kinds before performing type reduction, so the question is whether I hold to that.

...

I do not. So, first major question: Should I be checking type kinds before performing reduction? If the answer is yes, it appears I only need to edit the base classes.

In any case, the other major question I have is whether I properly understand the operator types and kinds. Now, kinds can only subsume by equality, so that's nice and easy. What I need to figure out is, have I properly grasped the subsumption/"subtyping" behavior for the relevant types? In other words, is it possible that some kind of compound value type can result in subsumption checks between two non-proper types? Let's check the reference on bounded quantification.

...

Not sure. Let's check the code.

The type must be synthesized from a value, so the overall value type is proper. To contain further structure, it must be a thunk type. The only computation types that can be well-kinded despite dealing with non-proper types are universal and existential types. Maybe just existential types.

So, an existential type consists of a type parameter, a kind, and a type that ideally has the type parameter as a free variable. We need that this type is proper, if the type variable is bound to the specified kind.

So, it could be the case that the value type is of the form list[T], which might have a structure very much like an operator application around an ascription around an operator. (Operators would only be strictly necessary if it were doing something like passing in different container types for the variable, and applying them to a constant type.) The structure could be arbitrarily obfuscated. What I want is that if, for all T, the existential types under consideration evaluate the value types to compatible types, then the subsumption holds.

Now, once we get here, we're guaranteed that the types have been reduced before we do any checks for subsumption. (This sounds like it goes against what I was saying before, but that was about kinding; this is about typing.) It should be the case that the only subsumption checks we care about between operator types are for the operator type itself, though we can throw in operator application checking as a treat.

In fact, it may be necessary, because the only way I see to handle existential types, universal types, and operators, is to substitute the type parameter with a fresh type variable, and covariantly check for subsumption.

In the end, I've got a few things to look into:

• Am I doing reduction and kind checking in the wrong order in the base classes?
• Do I have the right approach for subsumption checks between types with type parameters?
• Is there a good way to force subsumption to succeed if either type/kind is a failure node?
• Failing that, is there a direction for checking subsumption that makes much more sense than the alternative?

Anyway, it's late and I need to get to bed half an hour ago.

Good night.