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

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

Date found Description
27 Oct 2022

Page 382: 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.)
27 Oct 2022 Page S222: The type of the continuation given to >>=+ is misstated as 'a -> b error. It should be 'a -> 'b error. (Found by Norman Ramsey.)
1 Nov 2022 Page 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.)
3 Nov 2022

Page S410: 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.)
14 Nov 2022

Page 322: 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.)
17 Nov 2022 Page 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.)
26 Nov 2022 Page 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.)
3 Dec 2022 Page 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.)
16 Mar 2023 Page 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.)
22 Mar 2023 Page 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.)
24 Mar 2023 Page 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.)
24 Mar 2023 Page 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.)
20 Apr 2023 Page 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.)
24 Apr 2023 Page 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.)
30 Sep 2023 Page 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.)
4 Nov 2023

Page 439: 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.)
15 Feb 2024 Page 491: The evaluation judgment has the wrong form. See erratum for page 492. (Found by Roger Burtonpatel.)
15 Feb 2024

Page 492: 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.)
13 Mar 2024

Page S407: 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.)
25 Apr 2024

Page 214: 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.)