alt Hacker News> 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.
> 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.