This is not my area of my expertise but I feel like there are better solutions out there. I understand that this is an established approach. One thing that jumped out on me is that in the process of unification as described in the OP (and as implemented in the linked gist) it makes it hard to give useful feedback. A lot of information is lost in the unification and only the error is signalled.
With a minor tweak the constraint set can be turned into a dependency graph. Each constrain, in effect, an edge in the graph. Each node is a (variable, resolved type) pair. At the leaves of the graph we’ll have concrete types: either as defined in the code, inferred from literal values, or from function return types if specified. Then the graph is traversed in reverse order propagating types.
Nice thing about this is that graphs are relatively common. You either used them for something else, or you can find a library that implements all the basic algorithms, and probably do that efficiently. As a bonus, we have all the inference information. Once we get a type mismatch, in addition to just saying there’s one, we can also provide a whole inference chain so that the user could understand better what and where they need to change to make types align.
This algorithm has been around since the 70s. 50 years. I would hope that we would have improvements over algorithms made then, but in practice we often do not. That’s because PL theory is hard.
Unfortunately, saying “there are better solutions out there” doesn’t hold much weight. While it’s almost certainly true, getting there is hard. It’s orders of magnitude easier to criticize than to come up with a working algorithm like this, even if you have a general intuition of the idea.
You’ve already said that you wouldn’t even spend any time actually working on this. That gives this criticism even less weight.
This is not my area of my expertise but I feel like there are better solutions out there. I understand that this is an established approach. One thing that jumped out on me is that in the process of unification as described in the OP (and as implemented in the linked gist) it makes it hard to give useful feedback. A lot of information is lost in the unification and only the error is signalled.
With a minor tweak the constraint set can be turned into a dependency graph. Each constrain, in effect, an edge in the graph. Each node is a (variable, resolved type) pair. At the leaves of the graph we’ll have concrete types: either as defined in the code, inferred from literal values, or from function return types if specified. Then the graph is traversed in reverse order propagating types.
Nice thing about this is that graphs are relatively common. You either used them for something else, or you can find a library that implements all the basic algorithms, and probably do that efficiently. As a bonus, we have all the inference information. Once we get a type mismatch, in addition to just saying there’s one, we can also provide a whole inference chain so that the user could understand better what and where they need to change to make types align.
This algorithm has been around since the 70s. 50 years. I would hope that we would have improvements over algorithms made then, but in practice we often do not. That’s because PL theory is hard.
Unfortunately, saying “there are better solutions out there” doesn’t hold much weight. While it’s almost certainly true, getting there is hard. It’s orders of magnitude easier to criticize than to come up with a working algorithm like this, even if you have a general intuition of the idea.
You’ve already said that you wouldn’t even spend any time actually working on this. That gives this criticism even less weight.
You should do it!
It’s on my projects list but it’s a little bit further along so probably not any time soon, unfortunately.