Hacker News new | ask | show | jobs
by thunderseethe 117 days ago
> 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.
1 comments
StopDisinfo910 116 days ago
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.

link
thunderseethe 116 days ago
> 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.

link
StopDisinfo910 116 days ago
> You can create a bidir system that never requires annotations and uses unification to infer all types in the style of Haskell or OCaml.

There is no more bidir if you do that. It's just plain 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.

You can't implement HM without unification but you can do unification which is not HM. Actually a lot of what people call HM is not really HM but evolution of it and sometimes significant evolution.

link
thunderseethe 116 days ago
What are you calling bidir, if the introduction of unification means its no longer bidir?
link