4 ms·

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/genera

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 http://okmij.org/ftp/ML/generalization.html

Patient0 11y ago
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 11y 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 11y 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 11y 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.
asQuirreL 11y ago
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/c79c4bbb3179ef66bf6ffbda9b032a0bce94fb87/src/Infer.hs https://github.com/amnn/typed_geomlab/blob/c79c4bbb3179ef66b...

Patient0 11y ago

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

asQuirreL 11y ago

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/c79c4bbb3179ef66bf6ffbda9b032a0bce94fb87/src/Infer.hs https://github.com/amnn/typed_geomlab/blob/c79c4bbb3179ef66b...