What are higher-rank types and what are they good for?

Basic polymorphism is easy to learn, but it gets much more difficult once polymorphic types can be nested. The question is whether the language can do without this feature, or if it’s just too important to leave out.

Introduction

Just to set the scene, plain polymorphic functions give the caller the right to choose the type of a parameter. For example, the identity function can be given a single definition for all types:

def identity[T](arg: T):
    return arg

The square brackets should be read as “for all T”. In type theory we use the symbol ∀ to say “for all”, so in this notation the above function has type ∀T. T → T.

This is an example of a rank-1 type. I explain what that means further down.

A signature is a contract

The caller’s right to choose implies a restriction on the callee: It must refrain from making assumptions about the type so that it doesn’t contradict the caller’s choice. You can think of the type signature as a contract. To honor it, the function body has to treat T as a black box that cannot be used anywhere a specific type is required.

Higher-rank types let us turn the relationship around. The obligation to treat a parameter type like a blackbox can be moved from the callee to the caller.

But how is the caller supposed to provide a value of an unknown type?

One way is to wrap the unknown part in another type. An example will make it more concrete:

def foo[A](arg: forall B. List[B]) -> A:
    ..

Here B is polymorphic and wrapped in a List. I’m using the forall keyword above because the square bracket syntax doesn’t scale to nested expressions. Using ∀ notation, foo has type ∀A. (∀B. List[B]) -> A.

Now consider these calls to foo:

foo(list())
foo([1, 2, 3])

The first call is allowed, since nothing is assumed about the type of elements in the list. It’s just a List[alpha], where alpha is a fresh unification variable.

But the second call is passing a particular type of list, and the arg parameter is required to be polymorphic.

Higher-rank types

A higher-rank type is a polymorphic type in which a universal quantifier appears nested inside it. Here is the type of foo again as an example:

∀A. (∀B. List[B]) -> A

Rank refers to how deeply nested the innermost quantifier is, so the above function has rank 2. Higher rank simply means rank greater than 1. Rank 0 is not polymorphic at all.

Since foo has the above type, it follows that arg has type ∀B. List[B]. Consider what that means for each side, starting with the caller.

Let’s say the list() expression in the example has type List[alpha]. To match arg’s type, it must be generalized to ∀alpha. List[alpha]. That is possible here because alpha hasn’t unified with anything else, having no other use sites. Otherwise it wouldn’t be allowed. Neither can you generalize a specific type, such as in the second call. Because it’s applied to a parameter, the quantifier forces the caller to pass in a fresh, unused value.

Now let’s discuss the callee. It receives a polymorphic list ∀B. List[B]. Since the quantifier appears at the outermost level, it can be instantiated to List[beta], where beta is a unification variable. Foo gets to fill in beta with anything it likes, since there is no requirement that beta should generalize. For that constraint to arise, foo would have to pass the list along to another higher-rank function.

Also note that foo cannot return B values. It has to return an A, and what A means is decided by the caller. This actually means foo is impossible to implement, because it has no way of returning an A! It doesn’t receive an A, and it cannot create a new one since the type is unknown.

A type that is impossible to implement is pretty useless, but being able to prevent functions from returning certain values is not, as we shall see.

Regional mutation

Ok, so what is all this good for? In the foo example I used a List, but only because it’s something everyone is familiar with. The best real example I know of is the Haskell function runST. It lets us bottle up a mutable reference in a function and uses a higher-rank type to prevent it from leaking out.

This is very attractive because it gives users the ability to treat mutation as a private implementation detail. A function can use mutation to build up a result and still return it as immutable, since the ability to mutate the value can be guaranteed to end when the function returns. The immutable type can then enable concurrency and other good things.

Scoping the mutable reference to a function (and functions called by it) is sufficiently permissive for most use cases, such as constructing a list by appending to it iteratively. In contrast, limiting the right to mutate an object to its lexical scope would be too restrictive, since append is a different function defined elsewhere.

runST

I don’t want to spend too much time on runST, so this will be a bit brief. First, ST stands for “state thread”. It is called runST because it threads a piece of state through a sequence of function calls. It has the following type:

∀A. (∀S. ST[S, A]) -> A

As you can see it’s a function taking a single argument of type ∀S. ST[S, A]. The quantifier before S requires the argument to be fresh, as in the previous example.

Inside the region/thread the mutable value is wrapped in a MutVar[S, A]. It packs an S, representing the region, with a value of type A. For instance, a mutable list could have type MutVar[S, List[Int]]. S is a so-called phantom type that doesn’t correspond to a run time value.

The MutVar cannot be returned since the return type is another type. Together the restrictions are sufficient to encapsulate the stateful computation (or “thread”) and make it invisible to the rest of the program.

Quiet but capable

Now the question is: Should I add higher-rank types to Newton? I hesitate to make it too much like Haskell. I want the type system to stay in the background, but Haskell’s type system is flamboyant and demands attention. That’s not what I want for Newton. I want Newton’s type system to be capable, but low-key.

The issue is the number of abstract concepts you have to learn and pay attention to. For Newton I think it may be better to use type qualifiers instead of types. A qualifier such as mut or const can be explained without bringing up higher-rank types, regardless of how the compiler encodes it internally.

Foot notes

For details about runST, see Lazy Functional State Threads by John Launchbury and Simon Peyton Jones.

Stefan