Chapter 11: Simple Extensions

---

The simply typed lambda-calculus has enough structure to make its theoretical properties interesting, but it is not yet much of a programming language. In this chapter, we begin to close the gap with more familiar languages by introducing a number of familiar features that have straightforward treatments at the level of typing. An important theme throughout the chapter is the concept of derived forms.

11.1 Base Types

Every programming language provides a variety of base types—sets of simple, unstructured values such as numbers, booleans, or characters—plus appropriate primitive operations for manipulating these values. We have already examined natural numbers and booleans in detail; as many other base types as the language designer wants can be added in exactly the same way.

Besides Bool and Nat, we will occasionally use the base types String (with elements like "hello") and Float (with elements like 3.14159) to spice up the examples in the rest of the book.

For theoretical purposes, it is often useful to abstract away from the details of particular base types and their operations, and instead simply suppose that our language comes equipped with some set A of uninterpreted or unknown base types, with no primitive operations on them at all. This is accomplished simply by including the elements of A (ranged over by the metavariable A) in the set of types, as shown in Figure 11-1. We use the letter A for base types, rather than B, to avoid confusion with the symbol , which we have used to indicate the presence of booleans in a given system. A can be thought of as standing for atomic types—another name that is often used for base types, because they have no internal structure as far as the type system ^[1]

Figure 11-1: Uninterpreted Base Types

is concerned. We will use A, B, C, etc. as the names of base types. Note that, as we did before with variables and type variables, we are using A both as a base type and as a metavariable ranging over base types, relying on context to tell us which is intended in a particular instance.

Is an uninterpreted type useless? Not at all. Although we have no way of naming its elements directly, we can still bind variables that range over the elements of a base type. For example, the function^[2]

   λx:A. x; ▸ <fun> : A → A 

is the identity function on the elements of A, whatever these may be. Likewise,

   λx:B. x; ▸ <fun> : B → B 

is the identity function on B, while

   λf:A→A. λx:A. f(f(x)); ▸ <fun> : (A→A) → A → A 

is a function that repeats two times the behavior of some given function f on an argument x.

^[1]The systems studied in this chapter are various extensions of the pure typed lambda-calculus (Figure 9-1). The associated OCaml implementation, fullsimple, includes all the extensions.

^[2]From now on, we will save space by eliding the bodies of λ-abstractions—writing them as just <fun>—when we display the results of evaluation.

---