Jim's
Tutorials

Chapter 36: Lazy Evaluation

I have some issues with the dynamics presented in this chapter.

1. Some of the rules, like (36.7b), simply materialize types for introduced suspensions out of thin air. The rules as written, if interpreted at face value, would allow transition to states where the symbol context includes incorrect types associated to symbols. This is an issue that has already showed up in a few other places before this chapter, if I recall correctly. Really, this seems like part of a larger issue of including types in the dynamics—is that standard anywhere else? I should look into that!

2. The rules that replace arguments to introduction forms with cell references, like (36.3c) and (36.7c), apply even when the arguments to the form are already cell references! This technically makes the dynamics nondeterministic, albeit not in a very interesting or important way. More to the point, it means that we have possible reduction sequences like

   ν {s(z) || Ø} |->
   ν a ~ nat {s(@a) || a -> z} |->
   ν a ~ nat, b ~ nat {s(@b) || a -> z ⊗ b -> @a} |->
   ν a ~ nat, b ~ nat, c ~ nat {s(@c) || a -> z ⊗ b -> @a ⊗ c -> @b} |->
   ...
   

3. Similarly to the previous complaint, rule (36.3h) for β-reduction always allocates a new cell no matter what the argument is, which means that passing an argument along directly, as in λ (x : nat) foo(x)(3), will create an unnecessary chain of cells.
4. Similarly to both of the previous two complaints, introducing a cell when the argument to an introduction form or a function is already a value only creates overhead—nothing is gained, for example, by stepping ν Σ {(λ (x : nat) e)(3) || μ} |->* ν Σ, a ~ nat {[@a/x]e || μ ⊗ a -> 3} rather than simply ν Σ {(λ (x : nat) e)(3) || μ} |-> ν Σ {[3/x]e || μ}. (Actually, 3 isn’t a value in these dynamics, since s(e) is only a value if e is a cell, and 2 is not a cell… Hmm.) The same phenomenon takes place in rules for elimination forms like (36.3f) and (36.7e); although they do not directly allocate cells, they still require it to happen before they can be applied.

It seems like (2)-(4) could all be fixed by introducing a judgment like “would benefit from being replaced with a cell” that excludes values and cells, and then modifying the dynamics to make use of this judgment. For the rules complained about in (2), we could add a premise that the argument should be replaced. For the one complained about in (3), we could split it into (a) ordinary β-rule but with a premise that the argument shouldn’t need to be replaced, and (b) a version of the current rule with a premise that the argument should be replaced. For the rules complained about at the end of (4), we could replace the requirement that the relevant subterm be a cell with the requirement that the relevant subterm would not benefit from being replaced with a cell.

36.1

Suppose we eliminate on ω, like ifz ω {z -> e_0 | s(x) -> e_1}.

Under the by-name interpretation discussed previously, we first reduce ω in-place until it is a value. This takes one step: ω |-> s(ω), so ifz ω {z -> e_0 | s(x) -> e_1} |-> ifz s(ω) {z -> e_0 | s(x) -> e_1. Then ifz s(ω) {z -> e_0 | s(x) -> e_1} |-> [ω/x]e_1. Anywhere we make use of x in e_1 will re-do the simplification of ω.

Under the by-need interpretation, we have ν Σ {ω || μ} |-> ν Σ, a ~ nat {@a || μ ⊗ a -> s(@a)}, and hence

ν Σ {ifz ω {z -> e_0 | s(x) -> e_1} || μ} |->
ν Σ, a ~ nat {ifz @a {z -> e_0 | s(x) -> e_1} || μ ⊗ a -> s(@a)}.

Then,

ν Σ, a ~ nat {ifz @a {z -> e_0 | s(x) -> e_1} || μ ⊗ a -> s(@a)} |->
ν Σ, a ~ nat {ifz s(@a) {z -> e_0 | s(x) -> e_1} || μ ⊗ a -> s(@a)} |->
ν Σ, a ~ nat {[@a/x]e_1 || μ ⊗ a -> s(@a)}.

All instances of x in e_1 now use @a to refer to the shared unrolling of ω.

In this particular case, this saves essentially no work, but if the body of ω had involved nontrivial computation before settling on being s(ω), there would be significant savings.

36.2

(fix count_up : nat -> list is λ (n : nat) cons·(n, count_up(s(n))))(0)

36.3

I’ll follow the book’s lead, even though I have some concerns about some of how it presents the dynamics that I’ll voice elsewhere.

unit is very simple and needs no real change from ordinary FPC:

--------
<> val_Σ

void is almost as simple:

       ν Σ {e || μ} |-> ν Σ' {e' || μ'}
----------------------------------------------
ν Σ {abort(e) || μ} |-> ν Σ' {abort(e') || μ'}

Sums:

-------------------
l·@a val_{Σ, a ~ τ}

-------------------
r·@a val_{Σ, a ~ τ}

--------------------------------------------------
ν Σ {l·e || μ} |-> ν Σ, a ~ τ {l·@a || μ ⊗ a -> e}

--------------------------------------------------
ν Σ {r·e || μ} |-> ν Σ, a ~ τ {r·@a || μ ⊗ a -> e}

           ν Σ {e || μ} |-> ν Σ' {e' || μ'}
----------------------------------------------------
  ν Σ {case e {l·x_1 -> e_1 | r·x_2 -> e_2} || μ}
                        |->
ν Σ' {case e' {l·x_1 -> e_1 | r·x_2 -> e_2} || μ'}

                 ν Σ {e || μ} loops
-----------------------------------------------------
ν Σ {case e {l·x_1 -> e_1 | r·x_2 -> e_2} || μ} loops

---------------------------------------------------------
ν Σ, a ~ τ {case l·@a {l·x_1 -> e_1 | r·x_2 -> e_2} || μ}
                          |->
             ν Σ, a ~ τ {[@a/x_1]e_1 || μ}

---------------------------------------------------------
ν Σ, a ~ τ {case r·@a {l·x_1 -> e_1 | r·x_2 -> e_2} || μ}
                          |->
             ν Σ, a ~ τ {[@a/x_2]e_2 || μ}

Finally, recursive types:

-------------------
l·@a val_{Σ, a ~ τ}

-----------------------
fold(@a) val_{Σ, a ~ τ}

----------------------------------------------------------
ν Σ {fold(e) || μ} |-> ν Σ, a ~ τ {fold(@a) || μ ⊗ a -> e}

        ν Σ {e || μ} |-> ν Σ' {e' || μ'}
------------------------------------------------
ν Σ {unfold(e) || μ} |-> ν Σ' {unfold(e') || μ'}

    ν Σ {e || μ} loops
--------------------------
ν Σ {unfold(e) || μ} loops

-----------------------------------------------------------
ν Σ, a ~ τ {unfold(fold(@a)) || μ} |-> ν Σ, a ~ τ {@a || μ}

36.4

I’ll write <τ> for the interpretation of the LFPC type τ into SFPC, since it’s not clear to me how to use Unicode to typeset a hat like in the book.

1. unit has one value in LFPC, so its translation should also be unit, the SFPC type with one value.
2. An LFPC value of τ_1 × τ_2 is a pair of unevaluated subexpressions, so the SFPC type with the appropriate values is <τ_1> susp × <τ_2> susp.
3. There are no LFPC values for void, so we set <void> := void.
4. For similar reasons to (2), we set τ_1 + τ_2 := <τ_1> susp + <τ_2> susp.
5. This one is slightly subtler because of the self-reference. The lazy dynamics for recursive types given in Chapter 20 says that a value of rec t is τ is any expression of the form fold(e), where e is an unevaluated expression of type [rec t is τ/t]τ. Thus, we would like an SFPC value of <rec t is τ> to be of the form fold(e), where e is a suspension of a <[rec t is τ/t]τ>. The appropriate type is simply rec t is <τ> susp—the SFPC values of this type are of the form fold(e), where e is a suspension of a [<rec t is τ>/t]<τ>. Then because of how <_> is defined, this is equal to <[rec t is τ/t]τ>.