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 t1 with t2

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:

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 variant type that allows exception values.

             𝒯⟦x⟧ = <ok=x>
         𝒯⟦λx. t⟧ = <ok=λx. 𝒯⟦t]>
         𝒯⟦t1 t2⟧ = case 𝒯⟦t1⟧ of
                        <err=e> ⇒ <err=e>,
                         <ok=f> ⇒ (case 𝒯⟦t2⟧ of
                                      <err=e> ⇒ <err=e>,
                                       <ok=v> ⇒ f v)

For clarity, we first show how to translate raise x and try t1 with x2:

       𝒯⟦raise x⟧ = <err=x>
       
𝒯⟦try t1 with x2⟧ = case 𝒯⟦t1⟧ of
                        <err=e> ⇒ x2 e,
                         <ok=v> ⇒ <ok=v>

The general case is more complicated because of the possibility of exceptions being raised during the evaluation of both of the above.

       𝒯⟦raise t⟧ = case 𝒯⟦t⟧ of
                        <err=e> ⇒ <err=e>,
                         <ok=x> ⇒ <err=x>

𝒯⟦try t1 with t2⟧ = case 𝒯⟦t1⟧ of
                        <err=e> ⇒ (case 𝒯⟦t2⟧ of
                                       <err=e'> ⇒ <err=e'>,
                                       <ok=h> ⇒ h e),
                        <ok=v> ⇒ <ok=v>