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/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.
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?
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 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.
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/…
I can try to explain why HM type inference and unification are related.
If you take just the lambda calculus where you have:
1) Lambdas that bind variables
2) Usages of bound variables
3) Function applications
The inference rules for the first 2 are simple & straight-forward and require no unification.
For 1 (lambdas) - you create a fresh type variable (e.g: 'a') for the parameter type and infer the lambda body (e.g: 'T'), and the lambda's type is then 'a -> T'. While inferring the lambda body, you also pass the information that the parameter bound by the lambda has-type 'a'.
For 2 (variable usage), you just use the known type information that was passed down by the lambda inference.
For 3 (application), you need unification. Function application is between two subexpressions (e.g: 'f' and 'x'). You infer both of these recursively, and get 2 types (e.g: 'fType' and 'xType'). But you also know that 'fType' must look like: 'xType -> resType' because it's being applied to 'x'. You also know that 'resType' is the result of the entire application. So you have to unify 'fType' with 'xType -> resType'.
This is why inference relates to unification: You have 2 sources of information for 'fType' and 'xType' -- the recursive inference AND the fact they're being applied together.
This unification, by the way, is the only way that type information is learned for parameter types. If all parameter types are always specified (as in, e.g: C++) then formally, there's no type inference at all. So what C++ calls "local type inference" is formally just type checking.
> 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/…
I understand where you're coming from. I'm working on a mini-ML in Python as a learning exercise for myself and possibly as a tutorial for others; will open source it soon.
As such, I've come across a few good resources:
check out Robert Small's Hindley-Milner in Python[0], as well as alehander42's Hermetic language in Python[1].
I also just found out about Hask, an implementation of many Haskell language features in Python. Looking at the source code, it's well-commented and clear, so I suspect I'll learn a lot from it as well [2].
Finally, even though it's not in a dynamic or non-functional language like you request, I highly recommend Andrej Bauer's Programming Language Zoo[3], which contains very simple and easy-to-understand implementations of various type systems in OCaml. Very elucidating.
Edit: Oh, and one more resource that's been extremely helpful has been "Introduction to Functional Programming through Lambda Calculus" by Michaelson. Well worth the cost of the book.
Brilliant, I'm attempting something very similar in Ruby :)
Will check out those links.
When I have something workable, I'll post it to Github as well and then we can see about creating some kind of umbrella structure?
A related idea I have is that what is needed is some kind of grammar interchange format, or typing-relation interchange format -- kind of like JSON (or Amazon's ION) but for this sort of work. In some ways that is what S-expressions are, maybe there is no need to reinvent the wheel but my hunch is that a domain specific format is needed. Apologies if this is a bit vague, it's a hunch, and I'm going by intuition.
Check out RAML: https://github.com/raml-org/raml-spec Maybe it will fit the bill? It can even encode sum types. But I'm not sure if that's what you're looking for.
I'll ping you when I put my mini-ml in Python on Github.
That's not really what I mean. Take the file `parser.mly` from http://andrej.com/plzoo/html/miniml.html . See how it has it's own format for describing grammars. So does Yacc, so does X, Y, and Z. Is there an interchange format for parser generators?
There's BNF, and there's DFDL, and there's just plain lists of productions without the extra decorations in BNF, but basically no. The issue is that each parser generator in current wide use has its particular funky set of limitations that you have to hack around one way or another when you write the grammar for it: it can't handle left recursion, or right recursion, or ambiguity, except in certain special cases (maybe if it doesn't continue for more than one token, or two syntax-tree levels), or it can handle them but has potentially exponential runtime, or it just arbitrarily resolves them in a certain way which may be adequate for your needs or may require you to restructure the grammar, or whatever. And then there are lots of ways that our languages aren't quite context-free, and different parsing systems have different ways to shoehorn that into a basically context-free framework.
I think it's maybe a solvable problem, but I haven't seen anyone try to solve it.
Hermetic is amusing. Hask is very like what I'm aiming towards, not PLZoo. I'm starting with a PEG library (https://kschiess.github.io/parslet/) and working my way up. I'd prefer to start with a GLL parser which could handle mildly context-sensitive grammars and work my way up but I think creating a PEG version as a proof of concept is the way to go first.
> Would you be interested in something along those lines?
Yes! That would be very cool to read.
I've been working on an implementation of Mini-ML in Python using Robert Small's Hindley-Milner in Python [0] (and also eagerly awaiting the rest of Diehl's series on writing a Haskell).
I understand the fundamentals of the algorithm, but even now I don't think I could yet implement it from scratch. I'd love to read a detailed tutorial.
By the way, those Cornell lecture notes you referenced have also been very helpful to me.
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.
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
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.
> 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.
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.
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).
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).
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.
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.