What is "n" in RankNTypes

Question

I understand how forall enables us to write polymorphic function.

According to this chapter, the normal function which we generally write are Rank 1 types. And this function is of Rank 2 type:

foo :: (forall a. a -> a) -> (Char,Bool)
foo f = (f 'c', f True)

It explains like this:

In general, a rank-n type is a function that has at least one rank-(n-1) argument but no arguments of even higher rank.

What does it actually mean by rank argument ?

Can somebody give an example of Rank 3 type which is similar to the above foo function.

Hazel

Answer 1

Rank is defined inductively on the structure of types:

rank (forall a. T) = max 1 (rank T)
rank (T -> U)      = max (if rank T = 0 then 0 else rank T + 1) (rank U)
rank (a)           = 0

Note how it increases by one on the left-hand side of an arrow. So:

Rank 0: Int
Rank 1: forall a. a -> Int
Rank 2: (forall a. a -> Int) -> Int
Rank 3: ((forall a. a -> Int) -> Int) -> Int

and so on.

Cracking

I don't think this is quite right: e.g. fix :: (a -> a) -> a sure is rank-1, not rank-2. – Cassilda

Also why wouldn't a function that returns a polymorphic function be rank 2? That is why would the rank increase for a forall on the left side of the ->, but not the right? Why wouldn't Int -> (forall a. a -> a) be a rank 2 type? – Martine

@leftaroundabout, you are right, I fixed the definition. – Cracking

@sepp2k, that's how the definition goes. The deeper reason is that the left of an arrow has negative polarity, the right is positive. (It's similar to the definition of order.) – Cracking

@sepp2k: if you return a polymorphic function, it's the same as if your entire multi-argument function is (rank-1) polymorphic but the type variable just happens to turn not up in the first argument. – Cassilda

@Cassilda and Andreas: You're right, I did not think that through. – Martine

Answer 2

n is the level at which the forall(s) is/are nested. So if you have forall a. ((a -> a) -> Bla) (which is simply a more verbose way of writing (a -> a) -> Bla), then the forall is on the outside and applies to the whole function, so it's rank 1. With (forall a. a -> a) -> Bla the forall only applies to the inner function (i.e. the one you take as an argument) and is thus rank 2.

If the function that you take as an argument would itself take another function as an argument and that function would have a forall in its type, then that would be rank 3. And so on.

Martine

More precisely, n is the level at which the foralls are nested on the left of arrows (cf. the comments on Andreas Rossberg's answer). – Goldy

Answer 3

foo has one argument that includes a universal quantor, that what kicks in the need for RankN. But this argument's type itself, a -> a, is rank-1, it's the only argument, so foo has rank n with n − 1 = 1, i.e. foo is rank-2.

Now consider

bar :: ((forall a. a -> a) -> (Char,Bool)) -> Int

This has an argument of foo's type, which as we said has Rank 2. So that's the highest rank in bar's arguments; bar is thus a rank-3 function.

Cassilda

Answer 4

In Robert Harper's Practical Foundations of Programming Languages (first edition), the definition of the types of rank k is illustrated via inference rules. With this definition, if a type is of rank k, then it is also of rank k+1. So a type is associated with many different ranks k, k+1, k+2..., which means we can use relations instead of functions for formalization. Let Type be the set of all types, N be the set of natural numbers, and S be the desired subset of Cartesian product of Type and N. That is, an element of S is a tuple (T, n) saying "type T is of rank n". The following rules define ranks of a type.

1. (a, 0) is in S
2. (T -> U, 0) is in S, if both (T, 0) and (U, 0) are in S
3. (T -> U, k+1) is in S, if both (T, k) and (U, k+1) are in S
4. (T, k+1) is in S, if (T, k) is in S
5. (forall a. T, k+1) is in S, if (T, k+1) is in S given (a, k) is in S

By the definition above, the type of id and foo in your question is of rank 1, 2, 3... and 2, 3, 4... respectively.

Endymion