Near pg. 184 of Lambda Calculus and Combinators, the author is discussing the theory of dependent types. In particular, we are extending the lambda calculus to look at terms of form
$$ \Pi x : \sigma . \tau (x) $$
Now terms of this form denote type functions with degree and ranks, unless I am mistaken.
2 Textbook Passage on Degrees vs. Ranks
Here is what the textbook states:
The definition assumes that we are given a set (possibly infinite) of atomic type constants, $\theta^n_i$, each with a degree $n$. Each atomic type constant with degree $n$ will represent a type function intended to take $n$ arguments, the value of which is a type.
and then later:
Definition 13.7 (Type functions and types) Type functions of given degrees and ranks are defined in terms of proper type functions, which are defined as follows.
An atomic type constant of degree $n$ is an atomic proper type function of degree $n$ and rank $0$.
If $\sigma$ is a proper type function of degree $m > 0$ and rank $k$ and $M$ is any term, then $\sigma M$ is a proper type function of degree $m - 1$ and rank $k$.
If $\sigma$ is a proper type function of degree $m$ and rank $k$, then $\lambda x . \sigma$ is a proper type function of degree $m+1$ and rank $k$.
If $\sigma$ and $\tau$ are proper type functions of degree $0$ and ranks $k$ and $l$ respectively, and if $x \notin FV(\sigma)$, then $(\Pi x : \sigma . \tau)$ is a proper type function of degree $0$ and rank $1 + k + l$.
A type function of degree $m$ represents a function of $m$ arguments which accepts types as inputs and produces types as outputs. THe rank of a type function measures the number of occurrences of $\Pi$ in the normal form of the term representing it.
Question: I am totally confused between the notion of a type function's degree versus its rank.
The book states that the rank of a term is the number of $\Pi$'s in its (normal) form. But doesn't the number of such $\Pi$'s correspond exactly to the number of arguments it takes? That is, if a type function takes $n$ arguments, then doesn't that just mean there must be $n$ $\Pi$ symbols to capture those $n$ arguments?