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

Errata are sorted by page number. You can also find them sorted by date or by finder.

The most recent erratum on this page is dated 2024-04-25.

Page Description
12 Immediately following code chunk 12a, the colon between “interpreter’s response” and the reference mark of footnote 1 should be replaced with a period. (Found by Raghavendra Nyshadham on November 17, 2022.)
23 In code chunk 23a, the interpreter’s response after (val x 4) has been elided. This is the first of many elided responses, but it should have been signposted. (Found by Raghavendra Nyshadham on November 26, 2022.)
28 In the line following code chunk 28, strike the second “this”: in “This description is worth comparing this with the description of …” (Found by Raghavendra Nyshadham on December 3, 2022.)
164 Just before the section head for 2.13.3, the second equation for desugaring cond is missing a closing bracket.
The left-hand side should read “(cond [eqea] ).” (Found by Norman Ramsey on September 30, 2023.)

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.

(Found by Mike Vanier on April 25, 2024.)

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.

(Found by Alex Bai on November 14, 2022.)
356 In the penultimate paragraph on page 356, the math-style type of the instance (@ length bool) is mistakenly given as bool list → bool. The correct math-style type is bool list → int. The Typed μScheme type, which is shown as ((list bool) ‐> int), is correct. (Found by Bao Zhiyuan on March 22, 2023.)
366 “Has the form of a lambda” is meant to be a syntactic restriction, not a premise in the typing rule. (Found by Richard Townsend on March 16, 2023.)

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))) ::
(Found by Daniel Scherzer on October 27, 2022.)

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.)

(Found by Richard Townsend and Milod Kazerounian on November 4, 2023.)
458 The definition of null? shown on page 458 swaps #t and #f. The faulty definition is actually overwritten by a second definition on page 475 (chunk 475a), which is correct. (Found by Mert Erden on November 1, 2022.)
471 At the bottom of the page: “…, the number of variables under the forall must be equal the to number of type parameters T is expecting.” “be equal the to number” should be “be equal to the number”. (Found by Bao Zhiyuan on April 24, 2023.)
476 In the first paragraph of Section 8.3, which says “But unlike μScheme, μMLhas…”, there should be a space between “μML” and “has.” (Found by Bao Zhiyuan on April 20, 2023.)
491 The evaluation judgment has the wrong form. See erratum for page 492. (Found by Roger Burtonpatel on February 15, 2024.)

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


Nothing else needs to change.

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

(Found by Roger Burtonpatel on February 15, 2024.)
S222 The type of the continuation given to >>=+ is misstated as 'a -> b error. It should be 'a -> 'b error. (Found by Norman Ramsey on October 27, 2022.)

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))))
(Found by Andrew Fisher and Milod Kazerounian on March 13, 2024.)

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]
(Found by Norman Ramsey on November 3, 2022.)
S572 In μSmalltalk, when check-expect test fails, the error message says that two values are not “similar.” The message should say that they do not test as “=.” (Found by Matthew Fluet on March 24, 2023.)
S573 When a μSmalltalk expression is printed, say as part of an error message, a nullary block is incorrectly rendered as […]. It should be rendered as {…}. (Found by Matthew Fluet on March 24, 2023.)