Coding 2026-01-26
Hm.
Hm.
Hmmm.
I'm running into some issues here that I'm not totally sure what to do about. Basically, I came up with this whole fancy "pass a function to handle fresh variable bindings" thing for the helper functions for basic simply-typed lambda calculus. It would be really nice to do something similar with the various types introduced by quantification, but right now, that doesn't work, because the type variables being used are part of the type. Due to the way the universal and existential types are defined, right now the types have to match up completely. Where I currently do an equality check, it would be pretty much trivial to perform a substitution, though I'd also need to make sure to make sure that the type variable I'm substituting in isn't a free variable of the existential/universal type.
However, if I want to go this route, then I need to actually implement subsumption, because suddenly these types are "equivalent" without being literally the same.
Although...
Since what I'm going for currently is actually completely symmetric, I could also keep on calling it "equality", and simply redefine equality and hashes in some way... Not a big deal for equality, potentially somewhat cursed for hashing.
Also, I'm currently in the middle of rewriting the universal types tests; if I'm going to have any confidence that I'm updating it correctly, I need to do things in the order of:
- Finish updating tests
- Update equality, hashing, and type inference/checking
- Once the tests are passing, it's time to update them again.
In any case, whether I do the later steps or not, I do have to finish the first one, so let's see about that. Later, since it's late now and I need to wrap up.
Good night.