What is the purpose of erasing a type application to a term-application in parametric polymorphism?

From Types and Programming Languages by Pierce

23 Polymorphism

23.7 Erasure and Evaluation Order

in a full-blown programming language, which may include side- eﬀecting features such as mutable reference cells or exceptions, the type- erasure function needs to be deﬁned a little more delicately than the full era- sure function in §23.6. For example, if we extend System F with an exception- raising 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.

What this shows is that type abstractions do play a signiﬁcant semantic role, since they stop evaluation under a call-by-value evaluation strategy and hence can postpone or prevent the evaluation of side-eﬀecting 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:T 1 . t 2 ) = λx. erasev (t 2 )
erasev (t 1 t 2 ) = erasev (t 1 ) erasev (t 2 )
erasev (λX. t 2 ) = λ_. erasev (t 2 )
erasev (t 1 [T 2 ]) = erasev (t 1 ) dummyv


where dummyv is some arbitrary untyped value, such as unit.

• Is the purpose of "erase a type abstraction to a term-abstraction" to prevent the body of a type abstraction from being evaluated?

• What is the purpose of erasing a type application to a term-application by adding dummyv?

• What is the evaluation rule for an application when the argument is unit? (I can't find it in the section for type Unit.)

Thanks.

Q1

• Is the purpose of "erase a type abstraction to a term-abstraction" to prevent the body of a type abstraction from being evaluated?

Yes.

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

Q2

• What is the purpose of erasing a type application to a term-application by adding dummyv?

The erasure introduces a term-abstraction into a type-abstraction:

eraseᵥ(λX. t₂) = λ_. eraseᵥ(t₂)


So the erasure needs a term-application instead of a type-application. An argument of the term-application can be any untyped value because it will be discarded, so for example unit.

Q3

• What is the evaluation rule for an application when the argument is unit? (I can't find it in the section for type Unit.)

The unit value unit is a value. Therefore we can use (E-APPABS) for an application.

(λx:T₁₁. t₁₂) v₂ ⟶ [x ↦ v₂] t₁₂    (E-APPABS)