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

August 01, 2026

Polymorphism is a pretty simple concept at first, but it gets surprisingly subtle when polymorphic types can be nested. I strive to keep the type system simple, but maybe this feature is too useful to leave out.

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. You can think of the type signature as a contract, and 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 on its head. The caller can be required to treat a type like a blackbox. Take this function:

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

I’m using the forall keyword above because the square bracket syntax doesn’t scale to nested expressions. Note that B is bound one level deeper than A, inside the type scope created by the outer quantifier (the brackets). Using ∀ notation, foo has type ∀A. (∀B. List[B]) -> A.

Now consider these calls:

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 inside the callee. This is an important point. Polymorphic types are polymorphic to someone, not everyone.

Higher-rank types

A higher-rank type is a polymorphic type in which another 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 types simply means types with rank greater than 1.

The quantifier in front of B only applies to the parameter, not the whole function; And since the argument is provided by the caller, the obligation to uphold the polymorphic contract falls on it. It is foo that is allowed to “fill in” B with anything, not the caller.

Also note that the inner type scope ends before the arrow, so foo cannot return B values. I mention this because it mirrors the runST function, which I will discuss next.

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 runST function in Haskell. It lets us confine a mutable reference to part of the call graph and uses higher-rank types to prevent it from leaking out.

This is attractive because it gives users the ability to treat mutation as a private implementation detail. A function can use mutation internally and still appear referentially transparent to callers, since they cannot observe the effect. This can enable concurrency and other good things.

This extended notion of scope is sufficient for most common uses of mutation, such as constructing a list by appending to it iteratively. By contrast, limiting the right to mutate an object to its lexical scope would be too restrictive, since append is defined in another scope.

I won’t go into full detail about runST, but its type signature prevents two things:

Passing in arguments that are used elsewhere
Returning confined values to callers in other “regions”

Since Haskell doesn’t have global variables, this is sufficient to encapsulate and confine the mutable reference to runST and other functions called by it.

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.

In Haskell, mutability is encoded using the MutVar type constructor, that packs a mutable reference with a type variable. You can think of the type variable as representing the region the reference is confined to. In Newton syntax, a mutable list could have type MutVar[List[Int], R], for instance. To use the value you just extract it from the reference, which is not difficult. The issue is the number of abstract concepts you have to learn to understand what’s going on.

For Newton I think it may be better to use a type qualifier instead of a constructor. A qualifier such as mut or const can be explained without bringing up higher-rank types, regardless of how the effect is acheived.

Foot notes

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

Stefan