Coding 2025-06-29
Okay, after a good but exhausting day, I've successfully culled the type variables in the trees down to "term, type, and kind". Now, the different sorts of term and type that I had before are distinguished by the specific class that they inherit from, not which type variable they are associated with. This is a step forward, because now I can introduce more base classes into the node hierarchy without multiplying the number of type variables in play.
And I want to do that because I'm investigating bidirectional typing, which introduces a distinction in which all nodes can check types, but some nodes can also synthesize types, and I want to try encoding that distinction into the node types, such that, if a particular node type needs one of its children to synthesize a type, then that child will be able to synthesize, if a valid type exists. In other words, the Python type system should be able to guarantee that all necessary type ascriptions are carried out.
Now, one of the reasons I want to explore bidirectional typing is that I suspect it will improve some of the ergonomics around function typing; this justification is kind of just there to make me feel better about totally redoing the typing system in a way that will also break most of my tests.
It's late, and I don't currently have the energy to evaluate two important questions:
- Have I picked the right directions for everything, or should I make some fairly obvious tweaks?
- What do I want the new interface to look like? I'm currently leaning toward an "inferred_type" property and a "check_type" method.
- The secret third question: is it possible to guarantee that a synthesizing node always reduces to a synthesizing node, and if so, what compromises are required? (I mean, a synthesizing node knows its own type, by definition, so I guess it could just generate a possibly-redundant ascription node? Or there could be methods on the relevant node types to say "given this type, return some node that has the same behavior, and synthesizes the type, if it synthesizes at all".)
Anyway, that's a lot to think about, and there's no way I'm making any good decisions on it in the next half hour, so I'm going to wrap things up.
Good night.