4 ms·

Show HN: Hindley-Milner Type Inference Algorithm in OCaml

136 points by krat0sprakhar 10y ago

chubot 10y ago
FWIW, I had previously bookmarked these related pages: http://smallshire.org.uk/sufficientlysmall/2010/04/11/a-hindley-milner-type-inference-implementation-in-python/ http://smallshire.org.uk/sufficientlysmall/2010/04/11/a-hind... https://github.com/tomprimozic/type-systems https://github.com/tomprimozic/type-systems
kragen 10y ago
This is cool! It's nice to have a bite-sized runnable illustration of HM. Maybe I will finally be able to understand it — both the code and the linked lecture notes (http://www.cs.cornell.edu/courses/cs3110/2011sp/lectures/lec26-type-inference/type-inference.htm http://www.cs.cornell.edu/courses/cs3110/2011sp/lectures/lec...) look pretty informative. I don't think I can digest it in time to comment before it scrolls off the HN front page. It's a little unfortunate that this version doesn't include let-polymorphism, since that's necessary for parametrically polymorphic functions to be actually polymorphic, and it's not a recent addition — it's in the original Damas-Milner paper. All the other stuff about tuples, lists, sum types, and whatnot can be emulated with functions, but not let-polymorphism, not without a potentially exponential blowup in the program size.
- krat0sprakhar 10y ago
  Thanks for the feedback! This is actually a smaller part of a much bigger full-blown type-inferred programming language[0], we've been working on as a part of course in school. Our plan was to directly add type-inference in the language but after reading through Stephen Diehl's tutorial[1] we were intimidated and wanted to have a working version on a bite-sized language. I'm assuming a lot developers like me would be keen to understand how HM works, so I was considering writing a detailed tutorial of the unification algorithm step-by-step. Would you be interested in something along those lines? [0] - http://www.cs.columbia.edu/~sedwards/classes/2016/4115-spring/proposals/JSJS.pdf http://www.cs.columbia.edu/~sedwards/classes/2016/4115-sprin... [1] - http://dev.stephendiehl.com/fun/006_hindley_milner.html http://dev.stephendiehl.com/fun/006_hindley_milner.html
  - BhavdeepSethi 10y ago
    No link to Columbia's PLT lectures? :)
    - edmob 10y ago
      Link to the PLT course home page: http://www.cs.columbia.edu/~sedwards/classes/2016/4115-spring/ http://www.cs.columbia.edu/~sedwards/classes/2016/4115-sprin...
  - kragen 10y ago
    I don't know if I understand unification well or not; I feel like the control flow in Algorithm W is still a bit of a mystery to me, but I suspect that this is more a function of the effort I've put into understanding it than of the adequacy of the explanations I've found. http://canonical.org/~kragen/sw/dev3/term-rewriting.scm http://canonical.org/~kragen/sw/dev3/term-rewriting.scm was the last time I implemented unification, in August, and sort of represented my understanding of unification at the time — but looking at it now, I see that it only does pattern-matching, which is really only kind of half of unification. I think I did a more general first-order vaguely unificationy thing for queries on triple stores some years back, but the details are now fuzzy in this thing of mine that I flatter by calling it a mind. So, yes! I'd love a detailed tutorial of unification step-by-step (or perhaps recursive function by recursive function, if that turns out to be simpler). Maybe it already exists somewhere, perhaps in a textbook, and I just haven't found it. Or maybe I got intimidated and need to calm down and work some exercises instead of going off to read Facebook and HN.
    - igravious 10y ago
      I second that. But I would also love to know why type inference and unification are so closely related. I mean, I learnt about Prolog (and thus unification) years ago. Like a decade or more later I'm learning about type systems (properly I mean, via type theory) and type inferencing and unification shows up. I kind of get that intensional typing schemes define typing relations and that logic programming is synonymous with relational programming but is that all there is to it? The second thing I would like to say. And I've said this before. Languages like Ocaml and Haskell (never mind Agda, Coq, what have you) already have too much typing 'smarts' built into them. I would like to see -- hint, I'm probably going to have to get my hands dirty! -- an implementation in either a dynamically typed language like Ruby/Python/Perl/PHP/Javascript/… or a non-functional language like C/C++/Obj-C/… What think ye?
- Peaker 10y ago
  Another really helpful resource to understand algorithm W inferring types for HM is Algorithm-W-Step-by-Step at [1]. [1]. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7733&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65....
catnaroek 10y ago
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 10y 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 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.
willtim 10y ago
The paper "Typing Haskell in Haskell" is also very readable and informative.
bsaul 10y ago
I remember doing this in a practical exercice session with a teacher at university. We coded the algorithm, and i kept saying to myself that what i was coding didn't make any sense. I only understood many years later what i did that day, and how important it was.
mbrock 10y ago
When I was in 9th grade, I frequented an IRC channel full of misfits and rejects from all over the world. One of them was a notorious drunkard whose inebriated jokes were all over the top of the quote tracker. He was studying computer science at the University of Illinois, and at one point he asked me in private message if I was interested in OCaml. I said sure, I've been playing around with it. Then he said he was on a bender and asked if I wanted to do his homework for him... due in a few days... The assignment was to implement the Hindley-Milner type inference algorithm in OCaml. And that's how I got started with learning about type theory and language implementation. Thanks, guy, whereever you are. Last I heard you were in the military.
auggierose 10y ago
The nicest and clearest presentation of first-order unification I know of is in this book: https://www21.in.tum.de/~nipkow/TRaAT/ https://www21.in.tum.de/~nipkow/TRaAT/ From there it is a simple means to form and solve the type equations needed for Hindley Milner.
mattydoincode 10y ago
I actually did a school project that was very similar for a compilers class! It was also Hindley-Minler in Ocaml and we tried to basically stuff any random features of a programming language we could into one language, and just compile it to java (because you can do anything with java). Here is the paper we did: http://www1.cs.columbia.edu/~sedwards/classes/2013/w4115-fall/reports/pubCrawl.pdf http://www1.cs.columbia.edu/~sedwards/classes/2013/w4115-fal... and the full information is available here: http://www1.cs.columbia.edu/~sedwards/classes/2013/w4115-fall/index.html http://www1.cs.columbia.edu/~sedwards/classes/2013/w4115-fal... our project was called "pubCrawl".

136 points by krat0sprakhar 10y ago

FWIW, I had previously bookmarked these related pages: http://smallshire.org.uk/sufficientlysmall/2010/04/11/a-hindley-milner-type-inference-implementation-in-python/ http://smallshire.org.uk/sufficientlysmall/2010/04/11/a-hind... https://github.com/tomprimozic/type-systems https://github.com/tomprimozic/type-systems

kragen 10y ago

This is cool! It's nice to have a bite-sized runnable illustration of HM. Maybe I will finally be able to understand it — both the code and the linked lecture notes (http://www.cs.cornell.edu/courses/cs3110/2011sp/lectures/lec26-type-inference/type-inference.htm http://www.cs.cornell.edu/courses/cs3110/2011sp/lectures/lec...) look pretty informative. I don't think I can digest it in time to comment before it scrolls off the HN front page. It's a little unfortunate that this version doesn't include let-polymorphism, since that's necessary for parametrically polymorphic functions to be actually polymorphic, and it's not a recent addition — it's in the original Damas-Milner paper. All the other stuff about tuples, lists, sum types, and whatnot can be emulated with functions, but not let-polymorphism, not without a potentially exponential blowup in the program size.

krat0sprakhar 10y ago
Thanks for the feedback! This is actually a smaller part of a much bigger full-blown type-inferred programming language[0], we've been working on as a part of course in school. Our plan was to directly add type-inference in the language but after reading through Stephen Diehl's tutorial[1] we were intimidated and wanted to have a working version on a bite-sized language. I'm assuming a lot developers like me would be keen to understand how HM works, so I was considering writing a detailed tutorial of the unification algorithm step-by-step. Would you be interested in something along those lines? [0] - http://www.cs.columbia.edu/~sedwards/classes/2016/4115-spring/proposals/JSJS.pdf http://www.cs.columbia.edu/~sedwards/classes/2016/4115-sprin... [1] - http://dev.stephendiehl.com/fun/006_hindley_milner.html http://dev.stephendiehl.com/fun/006_hindley_milner.html
- BhavdeepSethi 10y ago
  No link to Columbia's PLT lectures? :)
  - edmob 10y ago
    Link to the PLT course home page: http://www.cs.columbia.edu/~sedwards/classes/2016/4115-spring/ http://www.cs.columbia.edu/~sedwards/classes/2016/4115-sprin...
- kragen 10y ago
  I don't know if I understand unification well or not; I feel like the control flow in Algorithm W is still a bit of a mystery to me, but I suspect that this is more a function of the effort I've put into understanding it than of the adequacy of the explanations I've found. http://canonical.org/~kragen/sw/dev3/term-rewriting.scm http://canonical.org/~kragen/sw/dev3/term-rewriting.scm was the last time I implemented unification, in August, and sort of represented my understanding of unification at the time — but looking at it now, I see that it only does pattern-matching, which is really only kind of half of unification. I think I did a more general first-order vaguely unificationy thing for queries on triple stores some years back, but the details are now fuzzy in this thing of mine that I flatter by calling it a mind. So, yes! I'd love a detailed tutorial of unification step-by-step (or perhaps recursive function by recursive function, if that turns out to be simpler). Maybe it already exists somewhere, perhaps in a textbook, and I just haven't found it. Or maybe I got intimidated and need to calm down and work some exercises instead of going off to read Facebook and HN.
  - igravious 10y ago
    I second that. But I would also love to know why type inference and unification are so closely related. I mean, I learnt about Prolog (and thus unification) years ago. Like a decade or more later I'm learning about type systems (properly I mean, via type theory) and type inferencing and unification shows up. I kind of get that intensional typing schemes define typing relations and that logic programming is synonymous with relational programming but is that all there is to it? The second thing I would like to say. And I've said this before. Languages like Ocaml and Haskell (never mind Agda, Coq, what have you) already have too much typing 'smarts' built into them. I would like to see -- hint, I'm probably going to have to get my hands dirty! -- an implementation in either a dynamically typed language like Ruby/Python/Perl/PHP/Javascript/… or a non-functional language like C/C++/Obj-C/… What think ye?
Peaker 10y ago
Another really helpful resource to understand algorithm W inferring types for HM is Algorithm-W-Step-by-Step at [1]. [1]. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7733&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65....

catnaroek 10y ago

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

willtim 10y ago

The paper "Typing Haskell in Haskell" is also very readable and informative.

bsaul 10y ago

I remember doing this in a practical exercice session with a teacher at university. We coded the algorithm, and i kept saying to myself that what i was coding didn't make any sense. I only understood many years later what i did that day, and how important it was.

mbrock 10y ago

When I was in 9th grade, I frequented an IRC channel full of misfits and rejects from all over the world. One of them was a notorious drunkard whose inebriated jokes were all over the top of the quote tracker. He was studying computer science at the University of Illinois, and at one point he asked me in private message if I was interested in OCaml. I said sure, I've been playing around with it. Then he said he was on a bender and asked if I wanted to do his homework for him... due in a few days... The assignment was to implement the Hindley-Milner type inference algorithm in OCaml. And that's how I got started with learning about type theory and language implementation. Thanks, guy, whereever you are. Last I heard you were in the military.

auggierose 10y ago

The nicest and clearest presentation of first-order unification I know of is in this book: https://www21.in.tum.de/~nipkow/TRaAT/ https://www21.in.tum.de/~nipkow/TRaAT/ From there it is a simple means to form and solve the type equations needed for Hindley Milner.

mattydoincode 10y ago

I actually did a school project that was very similar for a compilers class! It was also Hindley-Minler in Ocaml and we tried to basically stuff any random features of a programming language we could into one language, and just compile it to java (because you can do anything with java). Here is the paper we did: http://www1.cs.columbia.edu/~sedwards/classes/2013/w4115-fall/reports/pubCrawl.pdf http://www1.cs.columbia.edu/~sedwards/classes/2013/w4115-fal... and the full information is available here: http://www1.cs.columbia.edu/~sedwards/classes/2013/w4115-fall/index.html http://www1.cs.columbia.edu/~sedwards/classes/2013/w4115-fal... our project was called "pubCrawl".