23.7 Erasure and Evaluation Order

---

23.7 Erasure and Evaluation Order

The operational semantics given to System F in Figure 23-1 is a type-passing semantics: when a polymorphic function meets a type argument, the type is actually substituted into the body of the function. The ML implementation of System F in Chapter 25 does exactly this.

In a more realistic interpreter or compiler for a programming language based on System F, this manipulation of types at run time could impose a significant cost. Moreover, it is easy to see that type annotations play no significant role at run time, in the sense that no run-time decisions are made on the basis of types: we can take a well-typed program, rewrite its type annotations in an arbitrary way, and obtain a program that behaves just the same. For these reasons, many polymorphic languages instead adopt a type-erasure semantics, where, after the typechecking phase, all the types are erased and the resulting untyped terms are interpreted or compiled to machine code.^[4]

However, in a full-blown programming language, which may include side-effecting features such as mutable reference cells or exceptions, the type-erasure function needs to be defined a little more delicately than the full erasure function in §23.6. For example, if we extend System F with an exceptionraising primitive error (§14.1), then the term

   let f = (λX.error) in 0; 

evaluates to 0 because λX.error is a syntactic value and the error in its body is never evaluated, while its erasure

   let f = error in 0; 

raises an exception when evaluated.^[5] What this shows is that type abstractions do play a significant semantic role, since they stop evaluation under a call-by-value evaluation strategy and hence can postpone or prevent the evaluation of side-effecting primitives.

We can repair this discrepancy by introducing a new form of erasure appropriate for call-by-value evaluation, in which we erase a type abstraction to a term-abstraction

•  

  erasev(x)	=	x
  erasev(λx:T1 . t2)	=	λx. erasev(t2)
  erasev(t1 t2)	=	erasev(t1) erasev(t2)
  erasev(λX. t2)	=	λ_. erasev(t2)
  erasev(t1 [T2])	=	erasev(t1) dummyv

where dummyv is some arbitrary untyped value, such as unit.^[6] The appropriateness of this new erasure function is expressed by the observation that it "commutes" with untyped evaluation, in the sense that erasure and evaluation can be performed in either order:

23.7.1 Exercise [⋆⋆]

Translate the unsound example on page 335 into System F extended with references (Figure 13-1).

23.7.2 Theorem

If erase_v(t) = u, then either (1) both t and u are normal forms according to their respective evaluation relations, or (2) t → t′ and u → u′, with erase_v(t′) = u′.

^[4]In some languages, the presence of features like casts (§15.5) forces a type-passing implementation. High-performance implementations of these languages typically attempt to maintain only a vestigial form of type information at run time, e.g., passing types only to polymorphic functions where they may actually be used.

^[5]This is related to the problem we saw with the unsound combination of references and ML-style let-polymorphism in §22.7. The generalization of the let-body in that example corresponds to the explicit type abstraction here.

^[6]In contrast, the value restriction that we imposed in order to recover soundness of ML-style type reconstruction in the presence of side effects in §22.7 does erase type-abstractions—generalizing a type variable is essentially the opposite of erasing a type abstraction—but ensures soundness by permitting such generalizations only when the inferred type abstraction would occur immediately adjacent to a term abstraction or other syntactic value-constructor, since these also stop evaluation.

---