11.4 Ascription

---

11.4 Ascription

Another simple feature that will frequently come in handy later is the ability to explicitly ascribe a particular type to a given term (i.e., to record in the text of the program an assertion that this term has this type). We write "t as T" for "the term t, to which we ascribe the type T." The typing rule T-ASCRIBE for this construct (cf. Figure 11-3) simply verifies that the ascribed type T is, indeed, the type of t. The evaluation rule E-ASCRIBE is equally straightforward: it just throws away the ascription, leaving t free to evaluate as usual.

Figure 11-3: Ascription

There are a number of situations where ascription can be useful in programming. One common one is documentation. It can sometimes become difficult for a reader to keep track of the types of the subexpressions of a large compound expression. Judicious use of ascription can make such programs much easier to follow. Similarly, in a particularly complex expression, it may not even be clear to the writer what the types of all the subexpressions are. Sprinkling in a few ascriptions is a good way of clarifying the programmer's thinking. Indeed, ascription is sometimes a valuable aid in pinpointing the source of puzzling type errors.

Another use of ascription is for controlling the printing of complex types. The typecheckers used to check the examples shown in this book—and the accompanying OCaml implementations whose names begin with the prefix full—provide a simple mechanism for introducing abbreviations for long or complex type expressions. (The abbreviation mechanism is omitted from the other implementations to make them easier to read and modify.) For example, the declaration

   UU = Unit→Unit; 

makes UU an abbreviation for Unit→Unit in what follows. Wherever UU is seen, Unit→Unit is understood. We can write, for example:

   (λf:UU. f unit) (λx:Unit. x); 

During type-checking, these abbreviations are expanded automatically as necessary. Conversely, the typecheckers attempt to collapse abbreviations whenever possible. (Specifically, each time they calculate the type of a subterm, they check whether this type exactly matches any of the currently defined abbreviations, and if so replace the type by the abbreviation.) This normally gives reasonable results, but occasionally we may want a type to print differently, either because the simple matching strategy causes the typechecker to miss an opportunity to collapse an abbreviation (for example, in systems where the fields of record types can be permuted, it will not recognize that {a:Bool,b:Nat} is interchangeable with {b:Nat,a:Bool}), or because we want the type to print differently for some other reason. For example, in

   λf:Unit→Unit. f; ▸ <fun> : (Unit→Unit) → UU 

the abbreviation UU is collapsed in the result of the function, but not in its argument. If we want the type to print as UU→UU, we can either change the type annotation on the abstraction

   λf:UU. f; ▸ <fun> : UU → UU 

or else add an ascription to the whole abstraction:

   (λf:Unit→Unit. f) as UU→UU; ▸ <fun> : UU → UU 

When the typechecker processes an ascription t as T, it expands any abbreviations in T while checking that t has type T, but then yields T itself, exactly as written, as the type of the ascription. This use of ascription to control the printing of types is somewhat particular to the way the implementations in this book have been engineered. In a full-blown programming language, mechanisms for abbreviation and type printing will either be unnecessary (as in Java, for example, where by construction all types are represented by short names—cf. Chapter 19) or else much more tightly integrated into the language (as in OCaml—cf. Rémy and Vouillon, 1998; Vouillon, 2000).

A final use of ascription that will be discussed in more detail in §15.5 is as a mechanism for abstraction. In systems where a given term t may have many different types (for example, systems with subtyping), ascription can be used to "hide" some of these types by telling the typechecker to treat t as if it had only a smaller set of types. The relation between ascription and casting is also discussed in §15.5.

11.4.1 Exercise [Recommended, ⋆⋆]

(1) Show how to formulate ascription as a derived form. Prove that the "official" typing and evaluation rules given here correspond to your definition in a suitable sense. (2) Suppose that, instead of the pair of evaluation rules E-ASCRIBE and E-ASCRIBE1, we had given an "eager" rule

that throws away an ascription as soon as it is reached. Can ascription still be considered as a derived form?

---