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:

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.

In one of Rich Hickey’s excellent presentations introducing Clojure, he mentions in passing that Scala “isn’t really a functional language”.  He says that Java and Scala are both cut from the same mold, and because Scala doesn’t force immutability it really shouldn’t qualify.  These viewpoint is something I’ve been hearing a lot of from various sources, people talking about how F# is really the only mainstream functional language, or how once Erlang takes off it will leave Scala in the dust.

When I first heard this sentiment voiced by Rich, I brushed it off as a little odd and only slightly self-serving (after all, if you don’t use Scala, there’s a better chance you will use Clojure).  Rich has his own opinions about a lot of things, but I have found with most that I can still understand his rationale, even if I don’t agree.  So, realizing that many of his other kooky ideas seemed to have some basis in reality, I decided to come back to his opinion on Scala and give it some deeper consideration.

The core of the argument made by Rich (and others) against Scala as a functional language goes something like this:

• Mutable variables as first-class citizens of the language
• Uncontrolled side-effects (ties in with the first point)
• Mutable collections and other imperative libraries exist on equal footing
• Object-oriented structures (class inheritance, overloading, etc)
• Verbosity

Comparative Type Inference

If you’re coming from Java-land, the final point may have caught you a bit by surprise.  After all, Scala is vastly more concise than Java, so how could anyone possibly claim that it is “too verbose”?  Well, to answer that question, you have to compare Scala with the other side of the language jungle: the functional languages.  Here’s an explicitly-recursive function which sums a list of integers:

def sum(ls: List[Int]): Int = ls match {
  case hd :: tail => hd + sum(tail)
  case Nil => 0
}

That’s not too bad.  The use of pattern matching eliminates an entire class of runtime errors (selecting a non-existent element) and makes the code a lot cleaner than the equivalent Java.  However, compare this with the same function ported directly to SML (a functional language:

fun sum nil = 0
  | sum (hd :: tail) = hd + sum tail

One thing you’ll notice here is the complete lack of any type annotations.  Like most static functional languages, ML (and derivatives) has a form of type inference called “Hindley - Milner” (sometimes called “global type inference”).  Rather than just looking at a single expression to infer a type (like Scala), Hindley - Milner looks at the entire function and derives the most general (least restrictive) type which satisfies all expressions.  This means that everything can be statically type-checked with almost no need to declare types explicitly.

“Now, wait!” (you say), “You would never write a function just to sum a list; you should be using a fold.”  That’s true.  So let’s see how well these two languages do when the problem is solved in a more realistic fashion.  Once again, Scala first:

def sum(ls: List[Int]) = ls.foldLeft(0) { _ + _ }

Let’s see ML top that!

fun sum ls = foldl (op+) 0 ls

Then again, maybe we’ll just quit while we’re behind…

The fact is that Scala requires significantly more ceremony to accomplish some things which are trivial in pure-functional languages like ML and Haskell.  So while Scala may be a huge step up from Java and C++, it’s still a far cry from being the quickest and most readable way of expressing things in a functional style.

One obvious solution to this would be to just add Hindley - Milner type inference to Scala.  Well, this may be the “obvious” solution, but it doesn’t work.  Scala has an extremely powerful and complex type system, one with a number of properties which Hindley - Milner just can’t handle.  A full object-oriented inheritance hierarchy causes some serious problems with the “most general” inference of Hindley - Milner: just about everything becomes type Any (or close to it).  Also, method overloading can lead to ambiguities in the inferred types.  This is actually a problem even in the venerable Haskell, which imposes hard limitations on what functions can be in scope at any given point in time (so as to avoid two functions with the same name).

Simply put, Scala’s design forbids any type inference (that I know of) more sophisticated than local expression-level.  Don’t get me wrong, it’s still better than nothing, but a language with local type inference alone will never be as generally concise as a language with Hindley - Milner.

Side Effects

One big ticket item in the litany of complaints against Scala is the admission of uncontrolled side effects.  It’s not hard to find an example which demonstrates this property:

val name = readLine
println("Hello, " + name)

This example alone shows how fundamental side-effects are within the Scala language.  All we have done here is made two function calls, one of them passing a String and receiving nothing as a result.  From a mathematical standpoint, this code snippet is virtually a no-op.  However, we all know that the println function has an additional side effect which involves sending text to standard out.  Coming from Java, this makes perfect sense and it’s probably hard to see why this would be considered a problem.  However, coming from Haskell, what we just wrote was a complete abomination.

You see, Haskell says that no function should ever have side effects unless they are explicitly declared using a special type constructor.  In fact, this is one of the areas where monads have had a huge impact on Haskell’s design.  Consider the following Haskell equivalent:

main :: IO ()
main = do
         name <- getLine
         putStrLn ("Hello, " ++ name)

Even if you don’t know Haskell, the above should be pretty readable.  The first line is the type declaration for the main “function” (it’s actually a value, but why quibble).  Haskell does have Hindley - Milner type inference, but I wanted to be extra-explicit.  You’ll notice that main is not of type void or Unit or anything similar, it is actually of type IO parameterized with Haskell’s form of Unit: ().  This is an extremely important point: IO is a monad which represents an action with side-effects returning a value which matches its type parameter (in this case, ()).  The little dance we perform using do-notation is just a bit of syntax sugar allowing us to compose two other IO values together in a specific order.  The getLine “function” is of type IO String, meaning that it somehow reads a String value by using side effects (in this case, reading from standard in).  Similarly, putStrLn is a function of type String -> IO ().  This means that it takes a String as a parameter and uses it to perform some side effects, from which it obtains no result value.  The do-notation takes these two monadic values and composes them together, forming one big value of type IO ().

Now, this may seem horribly over-complicated, especially when compared to the nice clean side effects that we have in Scala, but it’s actually quite mathematically elegant.  You see, the IO monad is how we represent actions with side effects.  In fact, the only (safe) way to have side effects in Haskell is to wrap them up inside monad instantiations like these.  Haskell’s type system allows you to actually identify and control side effects so that they remain contained within discrete sections of your code base.

This may not sound so compelling, but remember that functional programming is all about eliminating side effects.  You compute your result, you don’t just accidentally find yourself with a magic value at the end of a long run.  The ability to work with side effects as packaged values just like any other constant is extremely powerful.  More importantly, it is far closer to the “true” definition of functional programming than what we have in Scala.

Conclusion

I hate to say it, but Rich Hickey and the others are quite right: Scala isn’t a terribly functional language.  Variables, mutable data structures, side effects and constant type declarations all seem to conspire to remove that crown from Scala’s proverbial brow.  But let’s not forget one thing: Scala wasn’t designed to be a functional language.

That may sound like heresy, but it’s true.  Scala was created primarily as an experiment in language design, specifically focusing on type systems.  This is the one area where I think Scala excels far beyond the rest of the field.  Scala makes it possible to model many problems in an abstract way and then leverage the type system to prove correctness at compile time.  This is approach is both revolutionary and an extremely natural way to solve problems.  The experience of using the type system in this fashion is a little difficult to describe (I’m still on the lookout for good examples), but trust me, you’ll like it when you see it.

Scala’s not really a functional language, and as Cedric Beaust has pointed out, it’s not really the best object-oriented language either; so what is it good for?  Scala sits in a strange middle ground between the two worlds of functional and object-oriented programming.  While this does have some disadvantages like being forced to take second place in terms of type inference, it also lets you do some really interesting stuff like build a mutable ListBuffer with constant time conversion to an immutable List, or sometimes recognize the fact that fold is not the universal solution.  It’s an experiment to be sure, but one which I think has yielded some very powerful, very useful results…just not many of a purely functional nature.