From Types and Programming Languages by Pierce
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
dummyvis some arbitrary untyped value, such as
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
What is the evaluation rule for an application when the argument is
unit? (I can't find it in the section for type