Unification (discussion and ideas)
So this is a long-standing issue. I don't have a fully mature reflection on this topic, but I think this could work:
- building one term with unifying tokens, while continuously adding constraints for them;
- calling a
unify
function with arguments (term, constraints), which would resolve the constraints, associating the tokens with their concrete types, and then change in place the references to these tokens in memory, inductively replacing the subterms by concrete terms (potentially existing already). - As for the memory management, it could be interesting to store the tokens in a separate location, that could be freed afterwards.
[Really this is the draftiest of all drafty things]