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)