4
$\begingroup$

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?

$\endgroup$
5
$\begingroup$

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

$\endgroup$
  • $\begingroup$ So , in general, does the rank correspond to the arity of the underlying (non type) function, while the degree corresponds to the arity of the type function? $\endgroup$ – George Jan 27 '17 at 0:55
  • 2
    $\begingroup$ @George Close, but not exactly. A function whose argument itself has a function type has a higher rank. $\endgroup$ – Gilles Jan 27 '17 at 9:18
  • $\begingroup$ @George You can have a unary function, whose argument is however a function-taking-function-taking-... . So, even if it is unary, its rank can be arbitrarily high. $\endgroup$ – chi Jan 27 '17 at 10:05
4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.