Chapter 8: Typed Arithmetic Expressions

---

In Chapter 3, we used a simple language of boolean and arithmetic expressions to introduce basic tools for the precise description of syntax and evaluation. We now return to this simple language and augment it with static types. Again, the type system itself is nearly trivial, but it provides a setting in which to introduce concepts that will recur throughout the book.

8.1 Types

Recall the syntax for arithmetic expressions:

•  

   t ::=        true        false        if t then t else t        0        succ t        pred t        iszero t 

  terms:

  constant true

  constant false

  conditional

  constant zero

  successor

  predecessor

  zero test

We saw in Chapter 3 that evaluating a term can either result in a value…

•  

   v ::=        true        false        nv nv ::=        0        succ nv 

  values:

  true value

  false value

  numeric value

  numeric values:

  zero value

  successor value

^[1]

or else get stuck at some stage, by reaching a term like pred false, for which no evaluation rule applies.

Stuck terms correspond to meaningless or erroneous programs. We would therefore like to be able to tell, without actually evaluating a term, that its evaluation will definitely not get stuck. To do this, we need to be able to distinguish between terms whose result will be a numeric value (since these are the only ones that should appear as arguments to pred, succ, and iszero) and terms whose result will be a boolean (since only these should appear as the guard of a conditional). We introduce two types, Nat and Bool, for classifying terms in this way. The metavariables S, T, U, etc. will be used throughout the book to range over types.

Saying that "a term t has type T" (or "t belongs to T," or "t is an element of T") means that t "obviously" evaluates to a value of the appropriate form-where by "obviously" we mean that we can see this statically, without doing any evaluation of t. For example, the term if true then false else true has type Bool, while pred (succ (pred (succ 0))) has type Nat. However, our analysis of the types of terms will be conservative, making use only of static information. This means that we will not be able to conclude that terms like if (iszero 0) then 0 else false or even if true then 0 else false have any type at all, even though their evaluation does not, in fact, get stuck.

^[1]The system studied in this chapter is the typed calculus of booleans and numbers (Figure 8-2). The corresponding OCaml implementation is tyarith.

---