Hacker News Reader

Comment by catnaroek | Hacker News Reader

Oleg has a nice article on how to implement OCaml-style type inference. It's a more sophisticated approach than just Algorithm W: http://okmij.org/ftp/ML/generalization.html

View on HN

For me, this article was the one where it "clicked": http://okmij.org/ftp/Haskell/AlgorithmsH.html#teval. Summary: type inference is just "evaluating" the program/expression, but the result is a type instead of a value. Each time you evaluate a function call, use unification to bind the arguments rather than pattern matching. Another way to understand it: pattern matching only works "one way", whereas unification works "both ways" - implying the caller's types as well as the callee's types. It also has a nice introduction of using a monad to simplify state management.

What OCaml's type checker do is a little bit fancier:

Damas-Milner type inference uses an "occurs check" to prevent the type equation solver from unifying a type variable with a compound type expression containing the same variable. The "obviously correct" way to perform this check is eagerly - as soon as possible.

However, performance-wise, delaying the occurs check can speed up the inference process - and this is exactly what OCaml does. The downside is that the resulting algorithm is quite involved, because the solver can now run into type expressions containing cycles, so naively recursively walking type expressions can cause an infinite loop.

oh right yes - I was replying to your comment because it was another article by Oleg, not because it was another article about OCaML type inference.

> For me, this article was the one where it “clicked”

Same. When I was just starting to learn about type systems, I found it very useful to have the concepts explained alongside an implementation, to see how they fit together. I don’t think I’ve ever gone so quickly from “I have no idea how this works” to “I could write this from memory” as I did when following that tutorial.

I wrote a full implementation of this version in Haskell as part of my dissertation [0]. I'm linking to a specific commit because in the coming month, I will be modifying it to introduce structural type inference (so that what would typically be considered a data type declaration can also be inferred).

[0]: https://github.com/amnn/typed_geomlab/blob/c79c4bbb3179ef66b...

Reply on news.ycombinator.com