Is higher-rank parametric polymorphism useful?

Question

I'm pretty sure everyone is familiar with generic methods of the form:

T DoSomething<T>(T item)

This function is also called parametrically polymorphic (PP), specifically rank-1 PP.

Let's say this method can be represented using a function object of the form:

<T> : T -> T

That is, <T> means it takes one type parameter, and T -> T means that it takes one parameter of type T and returns a value of the same type.

Then the following would be a rank-2 PP function:

(<T> : T -> T) -> int 

The function takes no type parameters itself, but takes a function which takes a type parameter. You can continue this iteratively, making the nesting deeper and deeper, getting PP of higher and higher rank.

This feature is really rare among programming languages. Even Haskell doesn't allow it by default.

Is it useful? Can it describe behaviors that are difficult to describe otherwise?

Also, what does it mean for something to be impredicative? (in this context)

Answer 1

In general, you use higher-rank polymorphism when you want the callee to be able to select the value of a type parameter, rather than the caller. For example:

f :: (forall a. Show a => a -> Int) -> (Int, Int)
f g = (g "one", g 2)

Any function g that I pass to this f must be able to give me an Int from a value of some type, where the only thing g knows about that type is that it has an instance of Show. So these are kosher:

f (length . show)
f (const 42)

But these are not:

f length
f succ

One particularly useful application is in using the scoping of types to enforce the scoping of values. Suppose we have an object of type Action<T>, representing an action we can run to produce a result of type T, such as a future or callback.

T runAction<T>(Action<T>)

runAction :: forall a. Action a -> a

Now, suppose that we also have an Action that can allocate Resource<T> objects:

Action<Resource<T>> newResource<T>(T)

newResource :: forall a. a -> Action (Resource a)

We want to enforce that those resources are only used inside the Action where they were created, and not shared between different actions or different runs of the same action, so that actions are deterministic and repeatable.

We can use higher-ranked types to accomplish this by adding a parameter S to the Resource and Action types, which is totally abstract—it represents the “scope” of the Action. Now our signatures are:

T run<T>(<S> Action<S, T>)
Action<S, Resource<S, T>> newResource<T>(T)

runAction :: forall a. (forall s. Action s a) -> a
newResource :: forall s a. a -> Action s (Resource s a)

Now when we give runAction an Action<S, T>, we are assured that because the “scope” parameter S is fully polymorphic, it cannot escape the body of runAction—so any value of a type that uses S such as Resource<S, int> likewise cannot escape!

(In Haskell, this is known as the ST monad, where runAction is called runST, Resource is called STRef, and newResource is called newSTRef.)

Answer 2

Higher rank polymorphism is extremely useful. In System F (the core language of typed FP languages you're familiar with), this is essential for admitting "typed Church encodings" which is actually how System F does programming. Without these, system F is completely useless.

In System F, we define numbers as

Nat = forall c. (c -> c) -> c -> c

Addition has the type

plus : Nat -> Nat -> Nat
plus l r = Λ t. λ (s : t -> t). λ (z : t). l s (r s z)

which is a higher rank type (the forall c. appears inside those arrows).

This comes up in other places too. For example, if you want to indicate that a computation is a proper continuation passing style (google "codensity haskell") then you'd right this as

type CPSed A = forall c. (A -> c) -> c

Even talking about an uninhabited type in System F requires higher rank polymorphism

type Void = forall a. a 

The long and short of this, writing a function in a pure type system (System F, CoC) requires higher rank polymorphism if we want to deal with any interesting data.

In System F in particular, these encodings need to be "impredicative". This means that a forall a. quantifies over absolutely all types. This critically includes the very type we're defining. In forall a. a that a could actually stand for forall a. a again! In languages like ML this isn't the case, they're said to be "predicative" since a type variable quantifies only over the set of types without quantifiers (called monotypes). Our definition of plus required impredicativity as well because we instantiated the c in l : Nat to be Nat!

Finally, I'd like to mention one last reason where you'd like both impredicativity and higher rank polymorphism even in a language with arbitrarily recursive types (unlike System F). In Haskell, there's a monad for effects called the "state thread monad". The idea is that the state thread monad lets you mutate things but requires to escape it that your result not depend on anything mutable. This means that ST computations are observably pure. To enforce this requirement we use higher rank polymorphism

runST :: forall a. (forall s. ST s a) -> a

Here by ensuring that a is bound outside the scope where we introduce s, we know that a stands for a wellformed type which doesn't rely on s. We use s to parameritize all the mutable things in that particular state thread so we know that a is independent of mutable things and thus that nothing escapes the scope of that ST computation! A wonderful example of using types to rule out ill-formed programs.

By the way, if you're interested in learning about type theory I'd suggest investing in a good book or two. It's hard to learn this stuff in bits and pieces. I'd suggest one of Pierce or Harper's books on PL theory in general (and some elements of type theory). The book "Advanced topics in types and programming languages" also covers a good amount of type theory. Finally "Programming in Martin Lof's type theory" is a very good exposition into the intensional type theory Martin Lof outlined.