What's the difference between the rank and the degree of a type function?

1 Context

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.

3 Question

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

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?

Nope. Let $\sigma, \tau$ be types (i.e., type functions with degree=rank=$0$). The type
$$
\prod_{x:\sigma} \tau
$$
is the type of functions $\sigma \to \tau$, which do not take type arguments -- they take value arguments (of type $\sigma$). So, the degree is $0$ (not $1$), while the rank is $1$.

StackExchange Computer Science Q#69367, answer score: 5