Comment by StopDisinfo910
8 days ago
The real question is unification vs bidir more than HM vs bidir.
Unification is simple, not very hard to implement and more powerful. Bidir gives better error messages and is more "predictable".
I personnaly lean strongly towards unification. I think you can get good enough error messages and what you lose with bidir is not worse it. But clearly the Rust core team disagreed. They clearly don't mind annotations.
Anyway, here is my non answer: it's a trade off.
> The real question is unification vs bidir
Quite the opposite, imo. Unification does not exclude bidir and the two fit together very well. You can have one system with both Unification and bidir and get all the advantages of both.
Not really, no. You can get localised unification but bidir as a whole like in Rust but you lose most of the advantage of unification. Hybrid systems are bidir for parts, unification for others.
But, I maintain that what the article calls HM is trully unification independantly of what's above. This is not about algorithm W. It's actually about the tension between solving types as a large constraint problem or using annotations to check.
> You can get localised unification but bidir as a whole like in Rust but you lose most of the advantage of unification.
Could you expand on this? I do not follow. You can create a bidir system that never requires annotations and uses unification to infer all types in the style of Haskell or OCaml. It is not often done because people are coming around to the idea that global type inference causes spooky action at a distance, but nothing prevents it from working.
> I maintain that what the article calls HM is trully unification
In some sense I think HM == unification because you can't really implement HM without unification. The first time a type variable encounters another type you'd be stuck.
2 replies →