Hacker News Reader

Comment by incognito124 | Hacker News Reader

Before opening the article, my first thought was "wdym, it's HM and Algorithm W"

The very first sentence was: > There is more to Hindley-Milner type inference than the Algorithm W.

I guess congratulations to the author for knowing the audience well enough

That remark is actually more interesting than you think. As groundbreaking as it was, algorithm W iss far too slow for non-toy languages. All modern HM languages (that I know of) use some form of union-find trickeries, as pioneered by the one presented in the blog post (but also present in resolution-by-constraints approaches employed by Haskell and Scala).

So, in fact, it's actually never algorithm W in non-toy languages. ;)

Side note: this article is originally from 2013 and is considered a must-read by any would-be hackers trying to modify the OCaml typechecker (it's cited in the documentation).

The Wikipedia articles claims that W is efficient, but only for a core language without highly desirable features like recursion, polymorphism, and subtyping.

https://en.m.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_...

OCaml without recursion would not be the same.

In fact, those union-find trickeries come from the same paper that presented algorithm W, where they were named algorithm J. W was known from the start to be more useful for proofs than implementation:

> As it stands, W is hardly an efficient algorithm; substitutions are applied too often. It was formulated to aid the proof of soundness. We now present a simpler algorithm J which simulates W in a precise sense.

https://doi.org/10.1016/0022-0000(78)90014-4

Isn't the union-find trickery "just" standard almost-linear unification as discovered by Paterson-Wegman and Martelli-Montanari around 1976? Or is there more to it in the setting of Algorithm J?

I'm actually a bit surprised that it took so long to discover these formulations of unification. I wonder what Prolog systems were doing at the time, given the importance of efficient unification.

Paterson-Wegman and Martelli-Montanari are worst-case linear, but Algorithm J just uses the earlier almost-linear union-find approach: unification variables are represented as mutable pointers to either a) nothing, or b) another type (which may itself be the "parent" unification variable in the union-find structure). Unification is then just a recursive function over a pair of types that updates these pointers as appropriate- and often doesn't even bother with e.g. path compression.

The subtitle, "or what polymorphism and garbage collection have in common", is another hint there may be more to TFA than its HN submission title indicates.

Reply on news.ycombinator.com