34 KiB

Raw Permalink Blame History

created_at

title

url

author

points

story_text

comment_text

num_comments

story_id

story_title

story_url

parent_id

created_at_i

_tags

objectID

year

2017-08-19T18:13:24.000Z

What is Hindley-Milner and why is it cool? (2008)

http://www.codecommit.com/blog/scala/what-is-hindley-milner-and-why-is-it-cool

jwdunne

185

1503166404

story

author_jwdunne

story_15054752

15054752

2008

Source

What is Hindley-Milner? (and why is it cool?) - Code Commit

What is Hindley-Milner? (and why is it cool?)

29
Dec
2008

Anyone who has taken even a cursory glance at the vast menagerie of programming languages should have at least heard the phrase “Hindley-Milner”. F#, one of the most promising languages ever to emerge from the forbidding depths of Microsoft Research, makes use of this mysterious algorithm, as do Haskell, OCaml and ML before it. There is even some research being undertaken to find a way to apply the power of HM to optimize dynamic languages like Ruby, JavaScript and Clojure.

However, despite widespread application of the idea, I have yet to see a decent layman’s-explanation for what the heck everyone is talking about. How does the magic actually work? Can you always trust the algorithm to infer the right types? Further, why is Hindley-Milner is better than (say) Java? So, while those of you who actually know what HM is are busy recovering from your recent aneurysm, the rest of us are going to try to figure this out.

Ground Zero

Functionally speaking, Hindley-Milner (or “Damas-Milner”) is an algorithm for inferring value types based on use. It literally formalizes the intuition that a type can be deduced by the functionality it supports. Consider the following bit of psuedo-Scala (not a flying toy):

| ----- | | |

def foo(s: String) = s.length
 
// note: no explicit types
def bar(x, y) = foo(x) + y

Just looking at the definition of bar, we can easily see that its type must be (String, Int)=>Int. As humans, this is an easy thing for us to intuit. We simply look at the body of the function and see the two uses of the x and y parameters. x is being passed to foo, which expects a String. Therefore, x must be of type String for this code to compile. Furthermore, foo will return a value of type Int. The + method on class Int expects an Int parameter; thus, y must be of type Int. Finally, we know that + returns a new value of type Int, so there we have the return type of bar.

This process is almost exactly what Hindley-Milner does: it looks through the body of a function and computes a constraint set based on how each value is used. This is what we were doing when we observed that foo expects a parameter of type String. Once it has the constraint set, the algorithm completes the type reconstruction by unifying the constraints. If the expression is well-typed, the constraints will yield an unambiguous type at the end of the line. If the expression is not well-typed, then one (or more) constraints will be contradictory or merely unsatisfiable given the available types.

Informal Algorithm

The easiest way to see how this process works is to walk it through ourselves. The first phase is to derive the constraint set. We start by assigning each value (x and y) a fresh type (meaning “non-existent”). If we were to annotate bar with these type variables, it would look something like this:

| ----- | | |

def bar(x: X, y: Y) = foo(x) + y

The type names are not significant, the important restriction is that they do not collide with any “real” type. Their purpose is to allow the algorithm to unambiguously reference the yet-unknown type of each value. Without this, the constraint set cannot be constructed.

Next, we drill down into the body of the function, looking specifically for operations which impose some sort of type constraint. This is a depth-first traversal of the AST, which means that we look at operations with higher-precedence first. Technically, it doesn’t matter what order we look; I just find it easier to think about the process in this way. The first operation we come across is the dispatch to the foo method. We know that foo is of type String=>Int, and this allows us to add the following constraint to our set:

X String

The next operation we see is +, involving the y value. Scala treats all operators as method dispatch, so this expression actually means “foo(x).+(y). We already know that foo(x) is an expression of type Int (from the type of foo), so we know that + is defined as a method on class Int with type Int=>Int (I’m actually being a bit hand-wavy here with regards to what we do and do not know, but that’s an unfortunate consequence of Scala’s object-oriented nature). This allows us to add another constraint to our set, resulting in the following:

X String

Y Int

The final phase of the type reconstruction is to unify all of these constraints to come up with real types to substitute for the X and Y type variables. Unification is literally the process of looking at each of the constraints and trying to find a single type which satisfies them all. Imagine I gave you the following facts:

Daniel is tall
Chris is tall
Daniel is red
Chris is blue

Now, consider the following constraints:

Person1 is tall

Person1 is red

Hmm, who do you suppose Person1 might be? This process of combining a constraint set with some given facts can be mathematically formalized in the guise of unification. In the case of type reconstruction, just substitute “types” for “facts” and you’re golden.

In our case, the unification of our set of type constraints is fairly trivial. We have exactly one constraint per value (x and y), and both of these constraints map to concrete types. All we have to do is substitute “String” for “X” and “Int” for “Y” and we’re done.

To really see the power of unification, we need to look at a slightly more complex example. Consider the following function:

| ----- | | |

def baz(a, b) = a(b) :: b

This snippet defines a function, baz, which takes a function and some other parameter, invoking this function passing the second parameter and then “cons-ing” the result onto the second parameter itself. We can easily derive a constraint set for this function. As before, we start by coming up with type variables for each value. Note that in this case, we not only annotate the parameters but also the return type. I sort of skipped over this part in the earlier example since it only sufficed to make things more verbose. Technically, this type is always inferred in this way.

| ----- | | |

def baz(a: X, b: Y): Z = a(b) :: b

The first constraint we should derive is that a must be a function which takes a value of type Y and returns some fresh type Y’ (pronounced like “why prime“). Further, we know that :: is a function on class List[A] which takes a new element A and produces a new List[A]. Thus, we know that Y and Z must both be List[Y']. Formalized in a constraint set, the result is as follows:

X (Y=>Y’ )

Y List[Y' ]

Z List[Y' ]

Now the unification is not so trivial. Critically, the X variable depends upon Y, which means that our unification will require at least one step:

X ( List[Y' ]``=>Y’ )

Y List[Y' ]

Z List[Y' ]

This is the same constraint set as before, except that we have substituted the known mapping for Y into the mapping for X. This substitution allows us to eliminate X, Y and Z from our inferred types, resulting in the following typing for the baz function:

| ----- | | |

def baz(a: List[Y']=>Y', b: List[Y']): List[Y'] = a(b) :: b

Of course, this still isn’t valid. Even assuming that Y' were valid Scala syntax, the type checker would complain that no such type can be found. This situation actually arises surprisingly often when working with Hindley-Milner type reconstruction. Somehow, at the end of all the constraint inference and unification, we have a type variable “left over” for which there are no known constraints.

The solution is to treat this unconstrained variable as a type parameter. After all, if the parameter has no constraints, then we can just as easily substitute any type, including a generic. Thus, the final revision of the baz function adds an unconstrained type parameter “A” and substitutes it for all instances of Y’ in the inferred types:

| ----- | | |

def baz[A](a: List[A]=>A, b: List[A]): List[A] = a(b) :: b

Conclusion

…and that’s all there is to it! Hindley-Milner is really no more complicated than all of that. One can easily imagine how such an algorithm could be used to perform far more complicated reconstructions than the trivial examples that we have shown.

Hopefully this article has given you a little more insight into how Hindley-Milner type reconstruction works under the surface. This variety of type inference can be of immense benefit, reducing the amount of syntax required for type safety down to the barest minimum. Our “bar” example actually started with (coincidentally) Ruby syntax and showed that it still had all the information we needed to verify type-safety. Just a bit of information you might want to keep around for the next time someone suggests that all statically typed languages are overly-verbose.

[Add to DZone][7] [Digg it][8] [Bookmark with Del.icio.us][9]

Comments

Do you know of anyone working on static typing for Clojure? I’d be very interested in a statically typed functional language on the JVM. (I like CAL — http://openquark.org very much, but it doesn’t have Clojure’s momentum at the moment).

[Tom Davies][10] Monday, December 29, 2008 at 5:25 am

This is probably approximentally what those IDEs do with ‘typeless’ scripting langauges and auto-complete etc..

I wish Java would do something like this at least for generics. For a dumbass example (that doesn’t even require HM) all Java folk wish that this:

ArrayList list = new ArrayList();

Could be this:

ArrayList list = new ArrayList();

But better would be more HM at deeper levels. For example, what about a “warning” for types that are less specific than they could be, e.g. returning Object when you could return String?

Also it would be interesting to do this at a data level for basic types. For example, you could do similar for “ranges of possible integer values” to declare what results are possible. As a simple example, String.length() would return [0,MAX_INT], not “integer.” Perhaps one could declare such a thing, or perhaps you could leave this at a compiler/IDE level. Wouldn’t it be cool if the IDE annotated your int and String types with extra information like possible range of values?

Or even just null/not-null? On this last point I have a patent pending for exactly this kind of data-movement analysis, so this is near-and-dear to my heart.

Anyway, I’ve lurked for a while and never posted a comment, so thanks for the interesting posts. I’m still not convinced about functional programming for normal commercial applications, but I’m continuing to read with an open mind!

(Yes I know the point of many of your posts is to show that Java is inadequate anyway… but still it’s fun for me to muse about how Java could be improved with some of the methods you suggest without throwing out the whole thing.)

[Jason Cohen][11] Monday, December 29, 2008 at 10:28 am

It’s worth mentioning that before HM is an inference algorithm, HM is a type system. It’s actually a fairly limited type system, but has the big plus that in every valid program every expression will have exactly one most general type which can always be inferred.

Critically for OO programmers, HM has no notion of subtyping. So F#, which must interact with the rest of .NET, must extend HM to the point where it can’t promise complete type inference.

Scala doesn’t even give the illusion of using an HM type system and uses a much more local type inference scheme. It would be interesting to see if Scala can borrow F#’s “I’ll infer most things but not everything” stance or if that’s just fundamentally out of reach for Scala.

[James Iry][12] Monday, December 29, 2008 at 10:44 am

Thanks for the run through on how Hindly-Milner works. I’ve often wondered how F# did it’s type inference. I’ve got to say though, it must also have to construct some kind of “type tree” so that interfaces and parent types get inferred before children.

[RickM][13] Monday, December 29, 2008 at 11:19 am

@Tom

Scala is a statically typed functional language on the JVM (sort of). It’s very much typed, but less “functional” than even Clojure. Regarding your question, it’s almost impossible to statically type a Lisp without losing what it means to be a Lisp. Specifically, macros pretty much fall apart.

The research I was referring to was some of the work going on in advanced JavaScript VMs (V8, Tracemonkey, etc). While not exactly Hindley-Milner, there is a lot of type inference going on behind the scenes to enable better optimization. There is also a suggestion in the wind to implement fastpath optimizations within Clojure functions when the argument types can be inferred. The inference itself would be a form of Hindley-Milner adapted to an object-oriented type system.

@Jason

I don’t think Java could ever implement full type inference without creating potential for unsoundness. I didn’t show it so much in these examples, but HM does not mix well with OO languages. Part of the reason for this is nominal-vs-structural typing, but subtyping and uncontrolled overloading are also a huge factor. Consider the following example:

    class Test {
    a;    // field
    b;    // another field

    testMethod(x) {
        a.doSomething(x);
    }

    testMethod(x) {
        b.doSomething(x);
    }
}

I ask you, what types would you infer here? Should “a” and “b” have the same type? Or should they be different types which both happen to implement doSomething(…)?

@James @RickM

I really have to take a closer look at F#. Even Odersky himself has mentioned that their type system is worthy of further attention. They’re really another language which has had to blend the functional and OO paradigms, but with a slightly different approach than Scala. You mentioned that their inference can cause unsoundness, is this something which is caught by an error or will your code just blindly execute until it runs into trouble?

[Daniel Spiewak][14] Monday, December 29, 2008 at 12:25 pm

Tom,

I doubt very much that anybody is working on a statically typed variant of Clojure. The only statically typed functional language for the JVM with any momentum is Scala. CAL is a distant second. Beyond that there is an effort to bring OCaml (ocaml-java) and I’ve read of various lurching efforts to bring Haskell to the JVM but I don’t think any of them are ready for prime time.

I’ve you’re curious about statically typed Lisps (not for the JVM) see Liskell, Qi, and Typed Scheme.

Jason,

Every useful statically typed language does some type inference. When you write in Java “int x = (a + b) * c” there’s an inference engine that determines the type of the expression (a + b) * c to make sure it’s assignable to int (perhaps with a coercion).

HM is a very specific type system and inference algorithm that is fundamentally incompatible with Java. But Java could do a heck of a lot more type inference than it currently does. See Scala and C# as examples.

RickM,

Type checking and type inference are related to logical unification. As such, “before” and “after” aren’t really thought of in the way that they are in imperative programming. In general, the ordering of logical unifications can be very hard to predict but should not affect the final outcome except when things don’t terminate and most type systems guarantee that type checking and inference will terminate.

[James Iry][12] Monday, December 29, 2008 at 12:37 pm

Daniel,

F#’s type system is not unsound as far as I know! I don’t know what I said to make you think that. But F#’s type system does prevent complete type inference. No, your code won’t run off a bridge if inference fails. You’ll just get a compiler error that the system couldn’t infer something.

[James Iry][12] Monday, December 29, 2008 at 12:46 pm

@James

Ah, excellent! It would be a little silly if they had implemented things the way I thought you were implying…

Incidentally, I’m not sure I know what you mean when you say that HM is a type system unto itself. As far as I know, HM is strictly just the algorithm for unifying type constraints. Constraint based typing has been around for much longer (I think Curry did it first, but it may have even been Church). There’s no restriction which says that languages with HM must have an ML-like type system. For example, Cat has Hindley-Milner type inference, and it is very different from ML (and family).

[Daniel Spiewak][14] Monday, December 29, 2008 at 1:01 pm

I should more correctly say that HM is a family of closely related type systems, sometimes called HM(X). Informally you can say it’s those type systems for which the algorithm can always find a principle type. Here’s a paper that generalizes the features found in that family: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.7215

The fact that the Cat language is different from the ML language doesn’t mean it doesn’t have an HM type system.

[James Iry][12] Monday, December 29, 2008 at 1:09 pm

Woah, Nelly.

I might really simply be a clueness and pedantic n00b, but I sorta threw up a little when I read “Int” in the first example instead of seeing something like “Num”.

http://www.zvon.org/other/haskell/Outputprelude/Num_c.html

Especially because of the stressing of “must” up there.

Raoul Duke Monday, December 29, 2008 at 3:14 pm

@Raoul

If this were type inference for Haskell, then yes, “Num a” would be the correct answer. However, this is Scala, and the foo method really does return Int. Therefore, because the Int#+(Int) method also returns Int, the final return value must itself be Int.

[Daniel Spiewak][14] Monday, December 29, 2008 at 3:48 pm

@Haskell vs. Scala

Ah, OK, I get it — thanks for the explanation.

(I guess then I think saying “Just looking at the definition of bar, we can easily see that its type must be (String, Int)=>Int. As humans, this is an easy thing for us to intuit.” before explaining it as only Scala would see it is sorta misleading: the way I “easily intuit” things is not how Scala does if it isn’t clear that I need to be thinking precisely how Scala would ![:-)][15]

Raoul Duke Monday, December 29, 2008 at 3:55 pm

Good post.

What I do not understand though, taking your example

testMethod(x) {
a.doSomething(x);
}

why OO languages can’t infer the type of a, but a functional language can (assuming this is then a function not a method)?

Peace
-stephan

[Stephan Schmidt][16] Monday, December 29, 2008 at 4:01 pm

@Stephen

A functional language would never allow the situation I demonstrated because functional languages do not support OO features. The closest we could get is something like this in OCaml:

    let fun a =
  let testMethod x = a#doSomething x

Off the top of my head, I’m not sure what type OCaml would infer here, but it would definately be structural. Probably something like:

    a : < doSomething 'a >
x : 'a    (* from enclosing scope *)

Object-oriented languages have a number of features which make HM more or less impossible. Subtyping is problematic, but not insurmountable. Overloading is real trouble, and nominal object typing is killer. If we allow for structural types and carefully existentialize overloading (probably using intersect types), we can make HM work in an OO language. However, the types inferred would be heinously long. You would end up with every class having dozens of type parameters; not the easiest thing to deal with in an error message! Furthermore, I don’t think that the inference on such a system would be decidable in every situation (for the same reason that System F is undecidable).

Someone more familiar with Hindley-Milner probably be able to answer your question more fully.

[Daniel Spiewak][14] Monday, December 29, 2008 at 4:22 pm

@jason cohen: i think a generic type in your comment got eaten by the blogging engine, probably due to angle brackets.

Aaron Davies Monday, December 29, 2008 at 6:27 pm

@Aaron

Yup, brackets got smoked.

@Daniel

Yes of course polymorphism screws things too. Simplest example is that of an interface — by definition there’s no code to infer from, therefore no types.

Still more support even at the IDE level in Java (or similar language) would be useful. Sure if you know nothing about the types (or data), fine, but when you do, how nice would it be for the IDE to tell you?

There’s still plenty of code that calls non-polymorphic other code where this inference could help.

Of course this could also help at the runtime-VM or JIT layer, and in fact they already do simple things like that for e.g. removing array-out-of-bounds or null-pointer checks when it’s clear that those errors are impossible. Still I wonder if it could be made smarter through more inter-functional logic like this.

[Jason Cohen][11] Tuesday, December 30, 2008 at 10:30 am

Thanks a lot for your explaination Daniel. Peace -stephan

[Stephan Schmidt][16] Tuesday, December 30, 2008 at 11:20 am

From the looks of it, it sure sounds like a simple Constraint Satisfaction Problem, solvable even with the most elementary artificial intelligence class. Naturally, I assume this algorithm in particular is highly optimized for use, but at least from what I read here, it sounds like the algorithm is expecting to find ONE type for each variable — highly unsatisfactory for generic functions such as those in Python or other such langauges.

QuacoreZX Wednesday, December 31, 2008 at 3:48 am

@QuacoreZX

You can get surprisingly far with simple let-polymorphism. Saying that HM is inferring one type implies that only a single nominal type will suffice, when really it is far more robust than that. If you extend the algorithm to encompass intersect and union types, you get even more power. Things aren’t quite as bleak as you think. ![:-)][15]

However, generally speaking you are correct. In any Turing Complete language, there will exist the possibility of code which is perfectly valid at runtime but not accepted by any type system, inference or no inference. Consider the following Clojure tidbit:

    (defn do-stuff [c x]
  (if c
    (:foo x)
    (:bar x)))

(do-stuff true (struct (create-struct :foo) 123))

Even using every trick in the type systems book (structural types, intersect types, etc), there is no way to successfully type this snippet: the struct we are passing does not define a :bar property, meaning that it is possible that evaluation may fail. Of course, at runtime, things work out just fine since the (:bar x) form is in a non-evaluated branch. The type system doesn’t know that though, and there is no way for it to reliably find out. Dynamic languages are permanently safe in this regard.

[Daniel Spiewak][14] Wednesday, December 31, 2008 at 4:07 am

@QuacoreZX,

Type systems are constraint logic programming, exactly. And as Daniel says, for every type system there are true things it can’t prove (see Godel). But when we say that HM always finds one principle type we don’t mean it will necessarily find a primitive type. In Haskell for instance

id x = x — A function that returns the value passed in unchanged

Gets inferred as
id :: forall t. t -> t

Meaning that the id function can take a value of any type and will return a value of that type.

Similarly
singletonList x = [x] — a function that boxes a single value into a list

Haskell infers
singletonList :: forall t. t -> [t]

Meaning if you pass in a value of any type ‘t’ the function gives back a value of type List of ‘t’.

Finally, a more complicated example using Haskell type classes

f x y z = x >>= y >>= z
f :: forall a, a1, b . (Monad m) => m a -> (a -> m a1) -> (a1 -> m b) -> m b

Which says that x must have a type “m a” where m is a special type constructor called a monad and “a” is some arbitrary type, y must have type “a -> m a1″ where a1 is some other arbitrary type, and z has type “a1 -> m b” where b is some arbitrary type. It will then return a value of type “m b”.

Hopefully this shows that principle types can be pretty sophisticated.

@Daniel,

Programs like what you wrote in Clojure above can be typed using dependent typing. However, afaik, there’s no way to infer dependent types.

[James Iry][12] Wednesday, December 31, 2008 at 8:42 am

@James

Good point; I hadn’t considered dependent types. With that said, I tend to consider dependent types to be flirting a little too closely with a full-blown meta-language. In fact, type systems with dependent types have a tendency toward intractability. That doesn’t make them any less valid, but it at least gives a better explanation for why I didn’t even consider them in my example. ![:-)][15]

Regarding inference, I’m pretty sure that it would be possible to infer the appropriate dependent type in examples as trivial as the one I gave. The trick would be to imbue the CT-If* rules with awareness of Boolean dependent types (required anyway to make the system work). However, in general, constraint-based inference for dependent types would certainly be undecidable. Shame…

[Daniel Spiewak][14] Wednesday, December 31, 2008 at 12:04 pm

@ Daniel Spiewak

This is an old argument but here it is anyway.

The problem with HM and OO is that this typing system does not have a property called principal typing. When a typing system has this property, and it is decidable, one can give the PT for the piece of code and any other typing for this piece can be obtained from this one. This allows you to have smart recompilation in your system. The lack of PT property has nothing to do with functional programming itself, but with the typing system used with the most popular ones.

There is a work going on with ML using intersection types instead of HM type system. Polymorphism by intersection is a promissing field, it list the multiple types instead of quantifying over it, as is done for HM.

Note that HM has principal TYPE property but no principal TYPING. The lack of modulatiry in the Dama/Milner algorithm can be notice that for “let N in M” program, one has to give a type for N and then for M. In a compositional type inference one can give type for N and M in parallel and check whether they can be related.

[anonymous][14] Wednesday, December 23, 2009 at 6:17 am

@Daniel: Strictly speaking, Hindley-Milner is the type system and Damas-Milner is the type inference algorithm, aka “Algorithm W”.

[Jon Harrop][17] Sunday, July 4, 2010 at 12:43 pm

@Jon

I am quite aware of that now. Unfortunately, I wasn’t too well versed in the distinction when I originally wrote this article. I’ve considered revising it, but the changes would be fairly extensive, and given the fact that it’s a minor semantic point, I thought it best to leave things as they are.

There is also the fact that most people aren’t going to make the distinction and so would be confused by the proliferation of terminology. Generally, when someone says “Hindley-Milner”, they actually mean the type inference algorithm. Should they use the term “Damas-Milner” instead? Absolutely. Is it worth quibbling? Probably not.

[Daniel Spiewak][14] Sunday, July 4, 2010 at 1:55 pm

You might be interested by the work of d.Nolen, author of CLojure core.logic who recently ttweeted :
if a Hindley-Milner type checker for Clojure ends up being more than 800-1000 lines of core.logic I’ll be very, very surprised.
https://twitter.com/#!/swannodette

see https://groups.google.com/group/clojure/browse_thread/thread/7d1a9ad2ff860f60

wolfgangK Friday, June 24, 2011 at 6:09 am

34 KiB

Raw Permalink Blame History

What is Hindley-Milner? (and why is it cool?) - Code Commit

What is Hindley-Milner? (and why is it cool?)

Ground Zero

Informal Algorithm

Conclusion

Comments

Post a Comment

Categories

34 KiB Raw Permalink Blame History Unescape Escape

What is Hindley-Milner? (and why is it cool?) - Code Commit

What is Hindley-Milner? (and why is it cool?)

Ground Zero

Informal Algorithm

Conclusion

Comments

Post a Comment

Categories

Related

34 KiB

Raw Permalink Blame History