What is "n" in RankNTypes
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.
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.
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.