Exceptions

TAPL builds up an exception mechanism in three steps: raising exceptions, handling exceptions, and exceptions returning values. Below are the semantics of these three mechanisms using evaluation contexts.

Raising exceptions

Syntax:

t ::= ...
      error

Evaluation:

E[error] ⟶ error          (E-ConError)  

Whereas the E-AppErr1 and E-AppErr2 rules in TAPL “unwinds” the evaluation context one layer at a time, this rule unwinds it all at once. (Actually, this rule is nondeterministic because it can unwind any part of the evaluation context. How would you modify the rules to make them deterministic?)

Handling exceptions

Syntax:

t ::= ...
      error
      try t with t

Now the evaluation rule for error should only unwind the evaluation context up to the nearest try, not all the way up to the top of the program as before. So we need two kinds of evaluation contexts. The first has the same definition as if we hadn’t added exceptions to the language:

F ::= [⋅]
      F t
      v F

The second can break through try:

E ::= F
      F[E]
      try E with t

Evaluation rules:

try v1 with t2 ⟶ v1        E-TryV
try F[error] with t2 ⟶ t2  E-TryConErr

Exceptions returning values

Syntax:

t ::= ...
      raise t
      try t with t

F ::= [·]
      F t
      v F
      raise F

E ::= F
      F[E]
      try E with t

Evaluation:

try v1 with t2 ⟶ v1                E-TryV
try F[raise v11] with t2 ⟶ t2 v11  E-TryConRaise

In pure lambda calculus

In “exception-passing style,” every term t is replaced with a sum. The inl values represent exceptions, and the inr values represent ordinary values.

A term that doesn’t raise an exception becomes an inr:

    𝒯⟦x⟧ = inr x
𝒯⟦λx. t⟧ = inr λx. 𝒯⟦t⟧

But a raise expression becomes an inl. As before, we define the translation just for variables:

𝒯⟦raise x⟧ = inl x

The translation of try is then:

𝒯⟦try t1 with t2⟧ = case 𝒯⟦t1⟧ of inl x ⇒ inr x,
                                  inr x ⇒ 𝒯⟦t2 x⟧
                                  

Application of one variable to another is easy, as before.

𝒯⟦x1 x2⟧ = x1 x2

The translation of let captures the fact that if t1 raises an exception, then t2 is bypassed.

𝒯⟦let x = t1 in t2⟧ = case 𝒯⟦t1⟧ of inr x ⇒ 𝒯⟦t2⟧, inl x ⇒ inl x

Now we can derive the more general rules for raise and applications.

𝒯⟦raise t⟧ = 𝒯⟦let x = t in raise x⟧
           = case 𝒯⟦t⟧ of inl x ⇒ inl x,
                          inr x ⇒ inl x
                                 
𝒯⟦t1 t2⟧ = 𝒯⟦let x1 = t1 in let x2 = t2 in x1 x2⟧
         = case 𝒯⟦t1⟧ of inl x ⇒ inl x,
                         inr x ⇒ (case 𝒯⟦t2⟧ of inl y ⇒ inl y, inr y ⇒ x y)