Coding 2025-09-07

Tags:
By Max Woerner Chase

The tests all pass, I've got 93% branch coverage and 85% mutation coverage, and, while there are various things that make sense to do, right now I'm focused on, what even is the existential types code doing? So, let's crack it open, and see if I can sort it out into something that makes sense to me.

The existential types module defines three classes:

Let's start with Pack. An instance of Pack is just a pair of a value type and a value. The value type and value are not inherently related.

Instead, given a Type, which combines a type variable, the kind of that type variable, and a value type expression, the Pack is an instance of the Type if, when the Pack's wrapped value type is substituted for the Type's type variable in the Type's value type expression, the Pack's wrapped value can be checked against the resulting value type. Clear as mud?

Now, to actually use a Pack in computation, we need an Unpack, which has an absurd number of attributes. The key thing is that it allows constructing a Type (this differs from a pure type inference setup, in which the Pack must specify its own type), has a variable associated with it, and contains a Pack, as well as the actual computation, which has the variable and type variable free. Evaluating the Unpack involves substituting the Pack values for the variables in the computation, and then evaluating that.

To make this of general interest, note that the contained Pack can actually be a variable, in which case the Unpack could be, for example, the body of a function, and then different behavior could be obtained by passing in different Pack values, which are only constrained to match the Type of the function argument; the packed values and types can vary freely as long as they conform to the Type. This is backed up by the fact that the inferred type of an Unpack node is independent of the contents of the packed value.

However, for the type inference to work, the Unpack's variable has to be bound to the value type expression without substituting any type for the type variable, and then the computation must infer a type that doesn't depend on the type variable, which... hm. My code might be wrong? But subtly.

Figuring out what makes sense requires some kind of actual example.

All right, let's suppose we have a p = Pack(unit, Thunk(Abstraction(Variable("x"), Return(unit(None))))). Among other Types, this satisfies Type(T, TYPE_KIND, ThunkType(FuncType(T, ReturnType(T)))). So we can have Unpack(T, TYPE_KIND, Variable("f"), ThunkType(FuncType(T, ReturnType(T))), p, UMMMM).

Okay, that didn't work, let's try again. p = Pack(unit, Thunk(Abstraction(Variable("x"), Return(bool(True))))). Type(T, TYPE_KIND, ThunkType(FuncType(T, ReturnType(bool)))). Unpack(T, TYPE_KIND, Variable("f"), ThunkType(FuncType(T, ReturnType(bool))), p, OKAY LOOK WE'RE GETTING CLOSER).

Part of the stumbling block here is that I've been leaving record types as an exercise for my future self, so it's sort of hard to shove enough information into a Pack with the tools I have currently. So, let's try living in the future.

p = Pack(unit, {x: unit(None), f: Thunk(Abstraction(Variable("x"), Return(bool(True))))}). Type(T, TYPE_KIND, {x: T, f: ThunkType(FuncType(T, ReturnType(bool)))}. Unpack(T, TYPE_KIND, Variable("r"), {x: T, f: ThunkType(FuncType(T, ReturnType(bool)))}, p, Application(Force(Attr(Variable("r"), "f")), Attr(Variable("r"), "x"))).

So, the question is, ignoring that some of these nodes don't exist, can the Unpack be successfully typed as ReturnType(bool)?

...

Okay, it looks like the typing should work, but I've just realized that my actual concern is around the determination of free type variables, and whether that's an issue is a very definite maybe.

Okay, here's what I think needs to happen: type inference of Unpack must fail if the type of the computation has the type variable free. This means I need a new constraint type. Yaaaay. I'll note this down in the code and then go to sleep.

Good night.