Jim's
Tutorials

Chapter 31: Symbols

31.1

Add a new form eq{t.τ}(e; e'; e_1; e_2). The statics are:

Γ |-_Σ e   : sym(ρ)    Γ |-_Σ e'  : sym(ρ')
Γ |-_Σ e_1 : [ρ/t]τ    Γ |-_Σ e_2 : [ρ'/t]τ
-------------------------------------------
 Γ |-_Σ eq{t.τ}(e; e'; e_1; e_2) : [ρ'/t]τ

The dynamics are:

--------------------------------------------------------
eq{t.τ}(quote[a]; quote[a]; e_1; e_2) |->_{Σ, a ~ ρ} e_1

                              a ≠ a'
------------------------------------------------------------------
eq{t.τ}(quote[a]; quote[a']; e_1; e_2) |->_{Σ, a ~ ρ, a' ~ ρ'} e_2

                       e |->_Σ e_0
---------------------------------------------------------
eq{t.τ}(e; e'; e_1; e_2) |->_Σ eq{t.τ}(e_0; e'; e_1; e_2)

                 e val_Σ    e' |->_Σ e'_0
---------------------------------------------------------
eq{t.τ}(e; e'; e_1; e_2) |->_Σ eq{t.τ}(e; e'_0; e_1; e_2)

An alternative dynamics would be for an eq form to reduce to an is form once the first argument normalizes.

31.2

lookup : (τ sym × τ) list -> τ sym -> τ opt
lookup := fix self : (τ sym × τ) list -> τ sym -> τ opt is
    λ (assoc : (τ sym × τ) list) λ (key : τ sym)
    case assoc {nil -> null | cons(p; assoc') ->
        eq{t.τ}(key; p·l; p·r; self(assoc')(key))}

31.3

The dynamics for checking a given linear ordering on symbols cannot respect alpha conversion. Suppose that we have a form cmp(r_1; e_2) that checks whether the symbol referred to by e_1 is ≤ the symbol referred to by e_2, resulting in 0 if so and 1 if not. Then if a < b, we must have that cmp(quote[a]; quote[b]) |->_{a, b} 0, but cmp(quote[b]; quote[a]) |->_{a, b} 1, even though these are alpha-variants.

Chapter 32: Fluid Binding

32.1

First, stack states must now be indexed by collections of active symbols. This is a scope-free dynamics for symbols rather than the scoped one used in the chapter, but it suits the stack dynamics better. We must also add two new kinds of stack frames: put[a](-; e_2), and put[a](e_1; -). Before defining the dynamics for the new constructs and frames, we first define the dynamics for an auxiliary “search” state k ≥ k' ? a as described in the exercise statement.

---------------------
k ≥_Σ ϵ ? a |-> k ◀_Σ

-----------------------------------------
k ≥_Σ k';put[a](e_1; -) ? a |-> k ◁_Σ e_1

       f ≠ put[a](e_1; -)
-------------------------------
k ≥_Σ k';f ? a |-> k ≥_Σ k' ? a

We can now define the dynamics for the new constructs and frames.

--------------------------------------
k ▷_Σ new{ρ}(a.e) |-> k ▷_{Σ, a ~ ρ} e

---------------------------------------------------------------------
k ▷_{Σ, a ~ τ} put[a](e_1; e_2) |-> k;put[a](-; e_2) ▷_{Σ, a ~ τ} e_1

------------------------------------------------------------------------
k;put[a](-; e_2) ◁_{Σ, a ~ τ} e_1 |-> k;put[a](e_1; -) ▷_{Σ, a ~ τ}Σ e_2

--------------------------------------------------------
k;put[a](e_1; -) ◁_{Σ, a ~ τ} e_2 |-> k ◁_{Σ, a ~ τ} e_2

----------------------------------------------
k ▷_{Σ, a ~ τ} get[a] |-> k ≥_{Σ, a ~ τ} k ? a

An attempt to evaluate get[a] in a context where a is not bound will result in the execution of the ≤ state bubbling all the way up to the top of the stack and then returning back from the context of the get with an error.

32.2

We use the same put[a](-; e_2) frames as in Exercise 32.1, but we replace the other type of put frame with one of the simpler form put[a]. This is because we no longer need to keep track of the bound value in a frame, since it is now stored directly in μ. We do, however, still need to keep some kind of frame around, so that we know when to let go of the current binding for a. We no longer need the type of symbol-indexing used there, though, since that data is now present in μ. The interesting parts of the new dynamics are:

--------------------------------------------
k || μ ▷ new{ρ}(a.e) |-> k || μ ⊗ a -> ϵ ▷ e

---------------------------------------------------------------------------
k || μ ⊗ a -> _ ▷ put[a](e_1; e_2) |-> k;put[a](-; e_2) || μ ⊗ a -> _ ▷ e_1

---------------------------------------------------------------------------
k;put[a](-; e_2) || μ ⊗ a -> b ◁ e_1 |-> k;put[a] || μ ⊗ a -> b;e_1 ▷ e_2

----------------------------------------------------------
k;put[a] || μ ⊗ a -> b;e_1 ◁ e_2 |-> k || μ ⊗ a -> b ◁ e_2

----------------------------------------------------------
k || μ ⊗ a -> b;e_1 ▷ get[a] |-> k || μ ⊗ a -> b;e_1 ◁ e_1

----------------------------------------------
k || μ ⊗ a -> ϵ ▷ get[a] |-> k || μ ⊗ a -> ϵ ◀

32.3

raise is easy to implement:

raise(e) := throw e to get[hdlr]

The typing rule for raise is then admissible in any environment with hdlr ~ τ_exn cont. try is harder:

try(e_1; x.e_2) := letcc ret_try in
    (λ (x : τ_exn) e_2)
    (letcc hdlr_cont in put hdlr_cont for hdlr in
     throw e_1 to ret_try)

Let’s unpack this. We first assume that the evaluation of e_1 will produce an exception, so for our result, we evaluate e_2 applied to an expression that will evaluate to the thrown exception value. But we will need to be able to jump out of this application if e_1 actually finishes in a result without throwing an exception, so we first take hold of the continuation surrounding the overall try expression for this purpose. Now the argument to the lambda is precisely the continuation that we want to throw to from a raise in e_1, so we take the current continuation there and bind it to hdlr for when we evaluate e_1. Finally, we evaluate e_1 in this context, and if it does finish without an exception, we throw the result back to ret_try to bypass the evaluation of e_2.

This definition makes the typing rule for try admissible as long as hdlr ~ τ_exn cont.

Note that since hdlr_cont is (necessarily) taken hold of before the binding of hdlr is changed, its stack will still contain the prior binding of the exception handler, so that the old handler is restored as soon as an exception is thrown within e_1. This ensures that if an exception is thrown while evaluating e_2, it will be sent to the enclosing handler rather than back to e_2.

Chapter 33: Dynamic Classification

33.1

exception a of τ in e is just new a ~ τ in e. raise a with e is just raise(a·e). Both of these easily make the corresponding rules in the exercise admissible. try can be implemented using a combination of the original try from Chapter 29 and nested class matches:

try e ow a_1(x_1) -> e_1 | ... | a_n(x_n) -> e_n | x -> e' :=
    try e ow exn -> (match exn as a_1·x_1 -> e_2 ow
        (... (match exn as a_n·x_n -> e_n ow [exn/x]e')))

This also produces the right typing rule, although it takes a little bit more (still easy) work.