4 ms·

For me, this article was the one where it "clicked": http://okmij.org/ftp/Haskell/AlgorithmsH.html#teval http://okmij.org/ftp/Haskell/AlgorithmsH.html#teval. Su

For me, this article was the one where it "clicked": http://okmij.org/ftp/Haskell/AlgorithmsH.html#teval 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.

catnaroek 10y ago
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.
- Patient0 10y ago
  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.
evincarofautumn 10y ago
> 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.

catnaroek 10y ago

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.

Patient0 10y ago
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.

evincarofautumn 10y ago

> 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.