11.2 The Unit Type

---

11.2 The Unit Type

Another useful base type, found especially in languages in the ML family, is the singleton type Unit described in Figure 11-2. In contrast to the uninterpreted base types of the previous section, this type is interpreted in the simplest possible way: we explicitly introduce a single element-the term constant unit (written with a small u)-and a typing rule making unit an element of Unit. We also add unit to the set of possible result values of computations-indeed, unit is the only possible result of evaluating an expression of type Unit.

Figure 11-2: Unit Type

Even in a purely functional language, the type Unit is not completely without interest,^[3] but its main application is in languages with side effects, such as assignments to reference cells-a topic we will return to in Chapter 13. In such languages, it is often the side effect, not the result, of an expression that we care about; Unit is an appropriate result type for such expressions.

This use of Unit is similar to the role of the void type in languages like C and Java. The name void suggests a connection with the empty type Bot (cf. §15.4), but the usage of void is actually closer to our Unit.

11.2.1 Exercise [⋆⋆⋆]

Is there a way of constructing a sequence of terms t₁, t₂, ..., in the simply typed lambda-calculus with only the base type Unit, such that, for each n, the term t_n has size at most O(n) but requires at least O(2ⁿ) steps of evaluation to reach a normal form?

^[3]The reader may enjoy the following little puzzle:

---