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.
(a, 0)
is in S
(T -> U, 0)
is in S
, if both (T, 0)
and (U, 0)
are in S
(T -> U, k+1)
is in S
, if both (T, k)
and (U, k+1)
are in S
(T, k+1)
is in S
, if (T, k)
is in S
(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.