Errata for Programming Languages: Build, Prove, and Compare (by page)

There is an error in Table 3.4 (lowering rules for control operators). The try-catch rule is written as

(try‑catch e1 L e2)
⇝
(let ([h e2])
    (long‑label L
        (let ([x e1]) (lambda (_) x))) h)

whereas it should be

(try‑catch e1 L e2)
⇝
(let ([h e2])
    ((long‑label L
        (let ([x e1]) (lambda (_) x))) h))

In other words, the result of the long-label expression is applied to the handler h.

In Exercise 2a, the type of newLambda is given as

name list * exp -> name list * { varargs : bool } * exp

but the correct type is name list * exp -> exp.

When applied to an empty list, primitives car and cdr claim to have been applied to a “non-list.” The error message should say “applied to the empty list.” And if truly applied to a non-list, they should raise BugInTypeChecking, not RuntimeError.

The corrected code reads as follows:

("car",  unaryOp  (fn (PAIR (car, _)) => car 
                    | NIL => raise RuntimeError "car applied to empty list"
                    | v => raise BugInTypeChecking "car applied to non-list"
      ,  FORALL (["'a"], FUNTY ([listtype tvA], tvA))) ::
("cdr",  unaryOp  (fn (PAIR (_, cdr)) => cdr 
                    | NIL => raise RuntimeError "cdr applied to empty list"
                    | v => raise BugInTypeChecking "cdr applied to non-list"
      ,  FORALL (["'a"], FUNTY ([listtype tvA], listtype tvA))) ::

As noted in the text, the code doesn’t check the condition θΓ = Γ. A second, similar shortcut could have been taken by not passing ftv(Γ) to generalize. I chose not to take the second shortcut, because I want the code to resemble the rules as much as possible. But not if it required adding another judgment form (equality of environments) and associated code to table 7.3 on page 432. I also want not to make the total cost of type checking quadratic in the number of definitions.

FAQ: One could ask why those rules mess with Γ at all, given that we know a top-level Γ is empty. The side conditions and the parameter are needed to ensure soundness of each rule using purely local reasoning. The fact that a top-level Γ has these other properties is an emergent property of the rules system as a whole, the proof of which warrants a homework exercise (Exercise 10). And an emergent property is something we prefer not to rely on in a soundness proof. (The analogy with the LET rules doesn’t hurt either; if the VAL and VALREC rules were not consistent with LET, that would need explaining.)

The operational semantics of μML (Chapter 8) uses the same evaluation judgment as μScheme (Chapter 2): ⟨e,ρ,σ⟩⇓v. But μML does not have mutable variables, so by rights it should use the same evaluation judgment as nano-ML (Chapter 5): ⟨e,ρ⟩⇓v. The judgment forms used in rules CaseScrutinee, CaseMatch, and CaseFail should be updated to use the correct judgment form. And the second premise of CaseMatch should read

⟨e₁,ρ+ρ’⟩⇓v’.

Nothing else needs to change.

(The error was caused by using the wrong definition for the LaTeX macro \eval.)

In Typed μScheme, as a result of a copy/paste error, the predefined function cadr is given an unnecessarily restricted type. It is possible for the function to have type (forall ['a] ((list 'a) -> 'a)), as per this definition:

(val [cadr : (forall ['a] ((list 'a) ->'a))]
  (type-lambda ['a]
    (lambda ([xs : (list 'a)])
       ((@ car 'a) ((@ cdr 'a) xs))))

In Typed uScheme, function expString formatted the typed formal parameters incorrectly.

The corrected code reads as follows:

    fun sqbracket s = "[" ^ s ^ "]"
    val sqSpace = sqbracket o spaceSep
    fun formal (x, tau) = sqSpace [x, ":", typeString tau]