Jim's
Tutorials

Chapter 29: Exceptions

29.1

The theorem is imprecisely stated; the ok judgment is never defined for XPCF. However, a natural definition would be to first extend the K machine’s ~> judgment to raise and try frames in the obvious way and then extend its ok judgment by a rule

k ◁: τ    e : τ_exn    e val
----------------------------
          k ◀ e ok

Note that the τ in k ◁: τ does not occur in the conclusion; we only care that it holds for some τ—i.e., that k is well-typed.

1. All of the rules inherited from the original K machine can be proven safe in the same way as before. This leaves rules (29.5) to be accounted for.
   1. This follows immediately from inversion on the premise that the old state is ok (and subsequent inversion on the resulting typing judgments), followed by application of ~>’s extension to raise frames.
   2. Inversion on ok, plus the extension of ok to ◀ states.
   3. Inversion on ok, plus the extension of ~> to try frames.
   4. Ditto.
   5. Ditto, plus the substitution property of typing.
   6. Inversion on ok, plus the extension of ok to ◀ states.

2. We first consider states k ▷ e. As for the K machine, such a state can always take a step using the unique rule applicable to e’s form. We next consider states k ◁ e. If k does not end in a raise or try frame, then the same arguments used in progress for K apply, and if it does end in one of these, then one of rules (29.5b) and (29.5d) applies. We lastly consider states k ◀ e. If k is empty, then this is a final state. If k ends in a non-try frame, then rule (29.5f) applies. Finally, if k ends in a try frame, then rule (29.5c) applies.

These proofs do not rely on any properties of τ_exn.

29.2

We can extend an evaluation dynamics for ordinary PCF with some more rules. We start with the basic rules for raise and try:

    e ⇓ v
------------
raise(e) ⇑ v

      e_1 ⇓ v_1
---------------------
try(e_1; x.e_2) ⇓ v_1

e_1 ⇑ v_1    [v_1/x]e_2 ⇓ v_2
-----------------------------
    try(e_1; x.e_2) ⇓ v_2

We must then add rules for propagating exceptions upward when subexpressions produce them. For each rule other than the second one above, we need to add propagation rules corresponding to each ⇓ premise. The second rule above is excluded because it is precisely the case when an exception shouldn’t propagate upward. Here are a few example propagation rules; the rest are very similar.

For the rule

e_1 ⇓ lam{τ_2}(x.e)    [e_2/x]e ⇓ v
-----------------------------------
        ap(e_1; e_2) ⇓ v

we must add two propagation rules:

     e_1 ⇑ v_1
------------------
ap(e_1; e_2) ⇑ v_1

e_1 ⇓ lam{τ_2}(x.e)    [e_2/x]e ⇑ v
-----------------------------------
        ap(e_1; e_2) ⇑ v

For the rule

   e ⇓ v
-----------
s(e) ⇓ s(v)

we must add one propagation rule:

 e ⇑ v
--------
s(e) ⇑ v

29.3

The val judgment should be the same as in ordinary PCF; neither a try term nor a raise term is a legitimate value. The transition rules include all rules of strict call-by-value PCF. We add rules for evaluating under raise and for capturing try’s behavior:

       e |-> e'
----------------------
raise(e) |-> raise(e')

            e_1 |-> e_1'
------------------------------------
try(e_1; x.e_2) |-> try(e_1', x.e_2)

        e_1 val
-----------------------
try(e_1; x.e_2) |-> e_1

              e val
---------------------------------
try(raise(e); x.e_2) |-> [e/x]e_2

Then, as before, we must add propagation rules. Typical examples include:

          e val
-----------------------
s(raise(e)) |-> raise(e)

                e val
--------------------------------------
ifz{e_0; x.e_1}(raise(e)) |-> raise(e)

           e val
----------------------------
raise(raise(e)) |-> raise(e)

Chapter 30: Continuations

30.1

1. Preservation goes through identically for all of the old K machine rules, so we just need to show it for the new rules (30.5). These go through with reasoning extremely similar to that in Exercise 28.1 part 1; the only interesting things to note are the specifics in (30.5b) and (30.5e).

   For (30.5b), the key observations are that if x.e is the body of a well-typed letcc, then e expects to be supplied with a continuation accepting a value of e’s own result type, and that if k ▷ letcc{τ}(x.e) ok, k must be expecting e’s result type. Then cont(k) is exactly the right type to supply e with.

   For (30.5e), the key observation is that if k; throw{τ}(e; -) ◁ cont(k') ok, then k' must expect a value of e’s type, so it is safe to transition to k' ◁ e (the e val condition is already supplied by the premise of (30.5e)).

   It is worth noting that there is an additional important preservation property not directly mentioned in the chapter. First, extend the ~> judgment to full stacks instead of just frames by the following rules, so that k : τ ~> τ' when k transforms values of type τ to values of type τ':

   ----------
   ϵ : τ ~> τ
   
   k : τ' ~> τ''    f : τ ~> τ'
   ----------------------------
           k;f : τ ~> τ''
   

   Now for s = k ▷ e or s = k ◁ e, say s : ρ if e : τ, k : τ ~> ρ, and for every subterm of the form cont(k') occurring in s, we have k' : τ' ~> ρ for some τ' specific to k'. We can show that s : ρ is preserved by transition. Then for a term e : ρ with no subterms of the form cont(k), we have ϵ ▷ e : ρ, so if ϵ ▷ e |->* ϵ ◁ e', we have ϵ ◁ e' : ρ, and by inversion this means e' : ρ. This establishes that if a well-typed term without cont(k)s reduces to a value, it in particular reduces to a value of its type—for example, if e : nat contains no cont(k)s, then e evaluates to a nat (if it terminates), and not, say, a nat -> nat. This is important, and it does not follow simply from the preservation theorem (30.2)(1).

2. Progress, like preservation, goes through almost identically to the outline in Exercise 28.1. The only parts specific to KPCF are cases for when s = k; throw{τ}(-; e_2) ◁ e_1 or s = k; throw{τ}(e_1; -) ◁ e_2. In the former case, inverting s ok shows that e_1 val, so rule (30.5d) applies and we can take a step. In the latter case, inverting s ok (and its premises and their premises for a few steps) shows that e_1 val, e_2 val, and e_2 : cont(τ) for some τ. These last two imply that e_2 = cont(k') for some k', which along with e_1 val implies that (30.5e) applies and we can take a step.

30.2

Technically, every type τ is inhabited by the expression fix{τ}(x.x), but that’s clearly not in the spirit of the exercise.

1. letcc k in r·compose(L)(k), where L = λ (x : τ) l·x and compose is as defined on page 267.
2. λ (k : τ cont cont) letcc h in throw h to k
3. λ (f : τ_2 cont -> τ_1 cont) λ (x : τ_1) letcc h in throw x to f(h)
4. λ (k : (τ_1 + τ_2) cont) (compose(L)(k), compose(R)(k)), where L = λ (x : τ) l·x, R = λ (x : τ) r·x, and compose is as defined on page 267.

30.3

TODO