Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What is "n" in RankNTypes

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.

like image 567
Sibi Avatar asked Mar 12 '14 19:03

Sibi


2 Answers

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.

like image 170
Andreas Rossberg Avatar answered Oct 30 '22 14:10

Andreas Rossberg


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.

like image 30
sepp2k Avatar answered Oct 30 '22 15:10

sepp2k