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

Question

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.

1. An atomic type constant of degree $n$ is an atomic proper type function of degree $n$ and rank $0$.

2. 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$.

3. 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$.

4. 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 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?

Answer 1

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$.

Answer 2

The degree of a type function is its arity, i.e. the number of parameters that it takes. This is the simple concept that you're familiar with, independent of what kind of objects the function manipulates. Rank-0 types are types of base objects like integers, strings, and more complex data structures. The atomic type constants of degree $0$ would be things like int, char, bool, string, etc. Atomic type constants of higher degree are type constructors like list (degree $1$; list int (the type of lists of integers) has rank $0$ and degree $1-1=0$), map (degree $2$, fmap string int (the type of finite maps from strings to integers) has rank $0$ and degree $(1-1)-1=0$), etc.

The rank of a type function conveys what kind of objects it works on. Type functions of rank $1$ are the types of functions that act on base types. For example, if $\sigma$ and $\tau$ are two atomic types of degree $0$, then¹ $\sigma \to \tau$ is the type of functions from $\sigma$ to $\tau$, and has rank $0+0+1=1$. For example, int -> int has degree $0$ (it isn't “missing” a parameter) and rank $1$ (it's the type of a function acting on base values). The type of curried functions of two arguments int -> int -> int = int -> (int -> int) has rank $0+(0+0+1)+1=2$and degree $0$. Functions that take a function as argument have a higher-rank type, e.g. (int -> int) -> int has rank $(0+0+1)+0+1 = 2$.

Intuitively, the rank of a type is the number of times you have to apply an object of this type or a part of that type to get to a base object. This can be more than the number of abstractions that you need to perform to construct an object of that type, which would be the arity of the object itself, as is shown by the example of (int->int)->int — it's the type of a function of arity $1$, but getting to a base object also involves applying the argument to an integer.

¹ _{$\sigma \to \tau$ a notation shortcut for $\Pi x:\sigma. \tau$ used when $x$ does not appear free in $\tau$, i.e. when the dependent product is actually not dependent, but just an ordinary function type.}