The Hindley-Milner type system is very powerful: it allows you to express functions with complex type signatures in an elegant, readable way. For example, consider this function in Haskell:
combine :: (Show a, Show b) => a -> b -> String
combine x y = show x ++ show y
This function takes two values which can be converted to strings (i.e., are instances of the Haskell Show typeclass) and concatenates them after conversion. Note here that we haven't specified anything about the types except that they obey the showable constraint; therefore, we can plug in strings, integers, chars or user-defined showable types and always get the expected result, all without having to write a separate function for each combination of input types. Which is all just to say that combine is polymorphic in both of its arguments.
But now suppose we want the ability to customize how the values are converted to strings with a higher-order function. The obvious way to do this would be to enhance combine with a new polymorphic function parameter. So our new function would like this:
customCombine :: (Show a, Show b, Show c) =>
(c -> String) -> a -> b -> String
customCombine f x y = f x ++ f y
The idea here is that we can recover the original combine function via combine = customCombine show. But if instead we wanted to, say, add exclamation marks to the input values, we could write something like this:
combineWithExclamation = customCombine exclaim
where exclaim :: (Show a) => a -> String
exclaim x = show x ++ "!"
Sadly, the code for customCombine above will fail to compile in the Haskell 98 standard. The reason is that Haskell 98 is based on the Hindley-Milner type system - and while Hindley-Milner allows us to write polymorphic functions, it doesn't allow us to write functions which take polymorphic functions as arguments.
This seems peculiar, though. Didn't the fact that the type signature of customCombine defined the first parameter as being of type (c -> String), where c belongs to Show, ensure the function parameter could take any showable argument? The problem is that by using different type variables for the different arguments to customCombine, the type checker refuses to unify them, i.e., to allow them to be treated as referring to identical, concrete types. In particular, if we've specified in the type signature that f is of type c -> String and x is of type a, our type checker won't allow us to apply f to x, because it can't prove that c represents the same type as a. One way to try to get around this would be to simply directly unify a and c in the type signature by treating them as a single variable:
customCombine :: (Show a, Show b) => (a -> String) -> a -> b -> String
customCombine f x y = f x ++ f y
Here the problem is that f now takes the a value with the type of customCombine's second parameter, but by writing f y, we're also plugging in a value of the type of the third parameter. Again, we wanted to ensure that f was polymorphic over its own parameter (that is, that it accepts any showable value whatsoever and spits back a string), whereas with this implementation it can only operate on a single type within the scope of the function.
Type theorists and programming language implementers have thought hard about this problem and have arrived at a solution known as higher-ranked types. (In Haskell, this can be enabled via the RankNTypes language extension). Practically speaking, enabling higher-ranked types lets us introduce new variable scopes inside of type signatures. Here's the implementation we want:
{-# LANGUAGE RankNTypes #-}
customCombine :: (Show a, Show b) =>
(forall c. Show c => c -> String) -> a -> b -> String
customCombine f x y = f x ++ f y
By declaring that the first parameter of the function is of type (forall c . Show c => c -> String), we've specified that it accepts values of all showable types within the scope of the same function. The forall introduces a new type variable scope; by creating the type variable c within that scope, the type checker no longer attempts to unify it with any type variables that occur outside of that scope. In fact, we could've written the function signature this way:
{-# LANGUAGE RankNTypes #-}
customCombine :: (Show a, Show b) =>
(forall a . Show a => a -> String) -> a -> b -> String
customCombine f x y = f x ++ f y
Here, even though we've used the type variable a twice, the type checker understands that the instance inside of the forall scope is different from the one outside it. The only thing the compiler needs to verify about the input of f is that it belongs to the Show typeclass. In the implementation of customCombine, we've stated this explicitly by declaring the two parameters we're plugging into f to be showable.
(Interesting as all of this is, as an aside, one may still wonder about the somewhat cryptic syntax that Haskell is adopting here. Why introduce a new type variable scope through the "forall" keyword? The key idea is that of substitution. In first-order logic, we can take a universally quantified statement like "for all x, if x is a man, then x is mortal" and then substitute any actual value for "x" and drop the universal quantification: for instance, we could obtain "if Socrates is a man, then Socrates is mortal." A function parameter f with type (forall x . Show x => x -> String) is saying, "for all showable types x, if you hand me an x, then I will produce a string." We can then substitute any particular showable type for the type variable x. Hence by calling f with an Int-typed argument, as in f 1, we're implicitly instantiating f into a new function of type Int -> String and then plugging 1 in to that.)
To summarize, higher-ranked types allow us to write richer higher-order functions by letting their function parameters be polymorphic. In our case, we've used higher-ranked types to refactor our combine function into a more general function with a parameter that controls what happens to the values we're converting into strings. We were ultimately able to accomplish this feat by augmenting the old Hindley-Milner type system (plus typeclasses) with the ability to create new type variable scopes anywhere inside a type signature, thereby telling the compiler that all type variables declared outside the scope (and which meet the correct typeclass constraints) can be freely substituted for any type variable declared inside of it.
Co-written with Michael Baker.