0
$\begingroup$

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- effecting features such as mutable reference cells or exceptions, the type- erasure function needs to be defined 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 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: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.

$\endgroup$
1
$\begingroup$

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)
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.