In B. Pierce's book "Types and Programming Languages", he talks about the size of types (see pictures below).

I searched the book for a definition but could not find one. I only found a definition for the size of terms, but not for the size of types.

Could someone please explain what Pierce means by the expression "$size(T_1)$" (marked by yellow in the image below) ?

enter image description here enter image description here


A term in logic and rewriting theory is anything defined by a tree structure that's supposed to represent the syntax of something. It can be a term of a programming language, a type, a kind, a module, etc.

The size of a term is the size of the tree: it's 1 for a leaf, and $\mathit{size}(t) = \mathit{size}(t_1) + \dots + \mathit{size}(t_n)$ for a tree $t = C(t_1,\dots,t_n)$. The exact definition is often not terribly important: what matters is that the size of a term is strictly larger than the size of any term that appears as a part of it.

In programming language literature, some authors use term in this sense, and some authors use term for a term of the programming language itself as opposed to types, kinds, modules, etc. The former authors use expression for the narrow sense of a term of the programming language itself. Pierce uses term in the narrow sense.

The definition of the size follows the same principle no matter what syntactic category the term (in the broader sense) represents. Thus the size of a type is defined as $\mathit{size}(\mathsf{Nat}) = \mathit{size}(\mathsf{Bool}) = 1$, $\mathit{size}(\mathsf{T}_1 \mathord\rightarrow \mathsf{T}_2) = 1 + \mathit{size}(\mathsf{T}_1) + \mathit{size}(\mathsf{T}_2)$, etc.

When there are multiple syntactic categories, whether terms of another category count depends on the definition chosen by the author. For example, the size of $\lambda x:T. M$ could be defined as $1 + \mathit{size}(M)$, or as $1 + \mathit{size}(T) + \mathit{size}(M)$, or even as $1 + \mathit{size}(x) + \mathit{size}(T) + \mathit{size}(M)$ depending on what is convenient for the matters at hand.

  • $\begingroup$ Thank you for the answer. Following your answer, would $T_1 \rightarrow T_2=T_1$ not mean that their size is equal, i.e. $size(T_1)=size(T_1 \rightarrow T_2)$ ? If yes, then why is Pierce writing that this equality means that $size(T_1)>size(T_1 \rightarrow T_2)$ ? Is this a typo in the book maybe? $\endgroup$
    – jhegedus
    Dec 15 '14 at 13:36
  • $\begingroup$ @jhegedus Since $T_1 \rightarrow T_2 = T_1$, $size(T_1) = size(T_1 \rightarrow T_2) = size(T_1) + size(T_2) + 1 > size(T_1)$. One line of reasoning shows that the sizes are equal and another line of reasoning shows that the sizes are different, therefore there is a contradiction. $\endgroup$ Dec 15 '14 at 13:39

It seems to be a typo:

p 506 solution to 9.3.2

".... But this means that size(T1) is strictly greater than size(T1 -> T2), ..." should read "... size(T1) is equal to size(T1 -> T2) ..."

[It is impossible because all types in this system have finite size.]

Also, there is no formal definition of the "size" of a type. This can be taken to be the number of nodes in its tree representation.


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.