Three Dollar Quill

Okay, let's see. I didn't have the focus to do much today, yet again, and I don't want to draw this out, so let's see if I can do some stuff quickly.

First off, I've decided that I'm going to put "more advanced unification" on the back burner, at best. I've worked out that it's way too easy to construct simple combinations of sequences that must allow for multiple unifications. What I need to guide any design work is concrete examples of desirable code that fails to type check.

So, let's see about things I decided to do. I realized that I'd typed the "walk" methods for the variable substitutions wrong, and made it so that they both take an arbitrary single or sequence type, and reduce it to a version of the corresponding single or sequence type that doesn't just map straightforwardly. I'm not sure if the sequence version needs to walk single types, or to walk and construct types, so right now it just... doesn't. My hope is that this logic better fits in the unification code, but I don't really know.

Still paranoid about my laptop, so I'm going to just try to quick run through how unification should work.

So, say you have two single values. First, walk them, and then you either end up with a base type, an unbound variable, or a function type. Base types and unbound variables all interact with each other reasonably. Function types need to do sequence unification.

So, sequence unification. After walking, the options are "empty sequence", "fully determined sequence", "sequence with determined head but variable tail", and unbound sequence variable. If there's an unbound sequence variable, ez. While both have a determined head, just unify single types. At some point, one of them is going to run out, and then you need to walk that again, and continue unifying the result. If you don't reach an unbound sequence variable, then you reach a determined sequence, and at that point you just pop stuff off until you either unify an unbound variable with a determined sequence, or you hit the empty sequence and you really hope it unifies with an empty sequence or an unbound variable.

Not sure what kind of recursion depth a naive implementation would hit, but it's probably fine, at least to start with.

Oh, one other thing that I forget whether I mentioned before my laptop went *bloop*. I'm going to figure out ascription, but instead of bidirectional typing, I want to see if I can make it work with just really aggressively using unification everywhere. The hope of this is that I can properly extract a sufficiently concrete value to implement typing of let words.

Aw dang, I just realized I didn't sketch anything about type schemes. So type schemes, you get them from the environment, and the trick is, all of their bound variables need to be instantiated with fresh copies. I think. I kind of want to put that logic in the unification code. And one other thing I feel like should be in there is "Hey, the freshened variables of type schemes probably shouldn't be free after unification." I need to give some thought to whether that's actually true, or if I just find it intuitively appealing.

Anyway, I don't feel like staying on my laptop any longer, let's wrap this up.

Good night.