Errata for _Types and Programming Languages_. (Many thanks to Eijiro Sumii and Gary Klimowicz for helping curate these!) Errata are organized by page, naively sorted within the page. Text in square brackets lists the source, and an indicator of the severity of the error: no mark denotes VERY trivial errors * marks denote trivial errors ** marks denote less trivial errors :-) __________ p. xxi [Pierce 1st ed. *] Erik Hilsdale's name is spelled with a k Fermin Reig's name should be typeset Ferm\'{\i}n p. xxi, line 14 [Sumii] "Narciso Marti-Oliet" -> "Narciso Mart\'{\i}-Oliet" p. 7, "C#" [Sumii *] The # should not be superscript, and should be a "number sign" (not a "music sharp sign") according to the official language specification. p. 15 [Pierce 1st ed. *] The font used for (the set) T in 2.1.1 and 2.1.5 is inconsistent with the rest of the chapter. Ditto U in 2.1.5. p. 16, Definition 2.1.7, "The codomain or range of R" [Sumii **] This terminology is not standard. Usually, "codomain" means only T, while "range" means either T or {t \in T | \exists s. (s,t) \in R} (as defined here), depending on the literature. p. 19 [Pierce 1st ed. *] "P(0)" should be slanted in 2.4.1 p. 25 [Pierce 1st ed. *] "in under" --> "under" "is does not" --> "does not" The paragraph beginning "for brevity" would make more sense if it were moved just before the example higher on the page. p. 27 [Pierce 1st ed. *] concete --> concrete p. 28, 11th line from the bottom [Pierce 3rd ed.] S_i should be S_j (that is, it should read "t_1, t_2, t_3 are elements of S_j") p. 28, line -12 [Sumii] "by condition (2)" -> "by condition 2" p. 35, after the displayed program fragment [Pierce 3rd ed.] "using E-If" should be "using E-IfTrue" p. 40, Exercise 3.5.13 [Pierce 3rd ed.] The solution has an error; see p. 494, solution to exercise 3.5.13 [Pierce 3rd ed.] p. 40, Exercise 3.5.13 [Sumii] The solution has an error; see p. 494, Lemma A.1 [Sumii] p. 40, line -5 [Sumii] "containing" -> "satisfying" p. 41, definition 3.5.15 [Pierce 3rd ed.] the word "closed" is not needed here. p. 42, Exercise 3.5.16 [Pierce 3rd ed.] The solution has an error; see p. 496, solution to 3.5.16 [Pierce 3rd ed.] p. 42, Exercise 3.5.16 [Sumii] The solution has an error; see p. 496, line -7 [Sumii] p. 42, Exercise 3.5.16 [Pierce 1st ed. **] The solution has an error; see p. 497, subcase g1 = succ g1 [Pierce 1st ed. **] p. 42, Exercise 3.5.17 [Pierce 1st ed. **] The solution has an error; see p. 499, Lemma A.8, E-IfTrue and E-IfFalse cases [Pierce 1st ed. **] p. 42, Exercise 3.5.17 [Pierce 3rd ed.] The solution has an error; see p. 499, end of A.8 [Pierce 3rd ed.] p. 42, Exercise 3.5.17 [Sumii **] The solution has an error; see p. 499, Proof of Proposition A.9 [Sumii **] p. 45, line 8 [Sumii] "implementation sections" -> "implementation chapters" p. 47, near the middle [Sumii] "the result of the evaluation function yields no result" -> "the evaluation function yields no result" p. 49, Exercise 4.2.1 [Pierce 1st ed. **] The solution has an error; see p. 499, 4.2.1 [Pierce 1st ed. **] p. 53, footnote 2: [Pierce 3rd ed.] "the behaviors of some languages constructs" should be "the behaviors of some language constructs" p. 56 [Pierce 1st ed. *] the middle item in the first sample reduction sequence has an extra pair of parens p. 57 [Pierce 1st ed. *] all occurrences of "call by X" should be hyphenated (except, arguably, the first use of "call by need") p. 57, definition of call-by-value [Pierce 3rd ed.] "a term that is finished computing..." should be "a CLOSED term that is finished computing..." p. 57, definition of call-by-value [Sumii *] Like call-by-name, the call-by-value evaluation strategy also forbids reductions inside abstractions. By the way, the online errata (http://www.cis.upenn.edu/~bcpierce/tapl/errata.txt) adds "closed" to the (informal) definition of values here, but not all values are closed according to the formal definitions given in later chapters. p. 61, Exercise 5.2.4 [Pierce 1st ed. *] The solution has an error; see p. 500, solution 5.2.4 [Pierce 1st ed. *] p. 63, line 9 [Sumii] "Other common datatypes like lists, trees, arrays, and variant records" -> "Other common datatypes like lists, trees, arrays, variants, and records" p. 63, exercise 5.2.8 [Pierce 3rd ed.] fold_left should be fold_right p. 63, Exercise 5.2.8: [Sumii] "c x (c y (c z n)))" -> (remove the last closing parenthesis) "c x (c y (c z n))" p. 66, Exercise 5.2.11 [Pierce 3rd ed.] The solution has an error; see p. 501, solution to 5.2.11 [Pierce 3rd ed.] p. 67, Figure 5-2 [Sumii] The last periods in lines 18, 21, and 28 should be removed. p. 67, figure 5-2 [Pierce 3rd ed.] the reduction from times c3 (fct (prd c3)) to times c3 (fct c2') is not valid in call-by-value semantics -- the application of times to c3 should be reduced first. p. 71, last line of display near top of page [Pierce 1st ed. **] There should be a close-paren after the second t1. p. 71, last line [Pierce 1st ed. *] the RHS should (arguably) be parenthesized to match the corresponding line at the top of the page p. 72, line 5 [Pierce 3rd ed.] "values can be arbitrary lambda-terms" should read "values can be arbitrary lambda-abstractions" p. 73, exercise 5.3.8 [Pierce 3rd ed.] 4.2.2 should be 3.5.17 p. 73, Exercise 5.3.8 [Pierce 1st ed. **] The solution has an error; see p. 503, solution 5.3.8 [Pierce 1st ed. **] p. 76, exercise 6.1.1 [Pierce 3rd ed.] the combinator called "plus" does not implement the addition function (the solution in the back is correct, though) p. 78, Exercise 6.1.5 [Pierce 3rd ed.] The solution has an error; see p. 503, solution to 6.1.5 [Pierce 3rd ed.] p. 78, line 2 [Sumii] Add a "," before "x1". p. 78, second line of 6.2 [Pierce 3rd ed.] "To to" -> "To do" p. 79, exercise 6.2.3 [Pierce 3rd ed.] The statement to be shown is not quite true for d < 0. To be true for n>=0 and any integral d, it should be "Show that, if t is an n-term and, if d < 0, the free variables of t are all at least |d|, then is a (max(n+d,0))-term." p. 80, line 6 [Sumii] "([j|->s]t1 [j|->s]t2)" -> "([j|->s]t1) ([j|->s]t2)" Also, all the parentheses on the left hand sides of this definition should be in typewriter (heavy) font. p. 87 [Pierce 3rd ed.] "As in chapter 3" should be "As in chapter 4" p. 96, second line of proof of 8.3.2 [Pierce 2nd ed. **] T-IsZero should be T-Zero This error does *not* appear in the first printing. :-( p. 96, second to last line of T-If case in proof of 8.3.2 [Pierce 1st ed. **] T-If should be E-If p. 97, T-If case in proof of 8.3.3 [Pierce 1st ed. **] E-True and E-False should be E-IfTrue and E-IfFalse p. 102, footnote 1: [Pierce 3rd ed.] "they will be sometimes be elided" should be "they will sometimes be elided" p. 104, Exercise 9.3.2 [Pierce 1st ed. **] The solution has an error; see p. 506 [Pierce 1st ed. **] p. 104, proof of Theorem 9.3.3 [Sumii *] The exercise would be [Recommended, ***]. p. 104, Exercise 9.3.3 [Sumii] The solution has an error; see p. 506, near the middle [Sumii] p. 106, proof of 9.3.8 [Pierce 3rd ed.] "By induction on a derivation" should be "By induction on the depth of a derivation" p. 107, end of first para [Pierce 1st ed. **] The annotation on y should be T2, not T1 p. 107, Preservation theorem (and other preservation theorems throughout [Pierce 3rd ed.] the text) The theorem is correct as stated, but we don't really need this powerful a version of it for present purposes. Since (a) we have chosen only to be interested in evaluating closed terms and (b) the evaluation strategy is call-by-value (so evaluating a closed term only involved evaluating closed sub-terms), there is no reason for Gamma ever to be non-empty. p. 108, Exercise 9.3.10 [Pierce 3rd ed.] The solution has an error; see p. 507, solution to 9.3.10 [Pierce 3rd ed.] p. 108, Exercise 9.4.1 [Pierce 1st ed. **] The solution has an error; see p. 505 [Pierce 1st ed. **] p. 110, part 2 of Theorem 9.5.2 [Pierce 3rd ed.] the first "typed" should be "untyped" p. 114, l -10 [Pierce 3rd ed.] "the variable type @'a@" should be "the type variable @'a@" p. 118, line 2 [Sumii *] "with variables and type variables" -> "with variables" p. 120, Theorem 11.3.1 [Pierce 3rd ed.] The first part of the Theorem doesn't hold, for a couple of reasons. First, the statement in the "if" direction should read: if e(t) -> u, then there is a lambda-E term t' such that u = e(t') and t -> t' Second, the E-SeqNext rule should be changed to read v1; t2 -> t2 (with v1 in place of unit), to match the semantics of E-AppAbs. p. 121, Exercise 11.3.2 [Pierce 1st ed. **] The solution has an error; see p. 507, solution to 11.3.2 [Pierce 1st ed. **] p. 123, Exercise 11.4.1 [Pierce 3rd ed.] The solution has an error; see p. 508, solution to 11.4.1 [Pierce 3rd ed.] p. 123, Exercise 11.4.1 [(a student of) Sumii] The solution has an error; see p. 508, solution to 11.4.1, last line [(a student of) Sumii] p. 126, Figure 11-5, E-PairBeta1 and E-PairBeta2 [Sumii] The "1" and "2" after "." should be in typewriter (heavy) font. p. 129, line 2 [Sumii] "t'j" -> "tj'" p. 130, line 2 [Sumii] "both tuples and products" -> "both tuples and records" p. 130, second paragraph, second sentence [Pierce 3rd ed.] "affect" should be "effect" p. 130, Exercise 11.8.2 [Pierce 3rd ed.] The solution has an error; see p. 510, top of page [Pierce 3rd ed.] p. 130, Exercise 11.8.2 [Sumii *] The solution has an error; see p. 510, near the middle [Sumii *] p. 131, Figure 11-8 [Sumii] "Matching rules:" -> "Matching rules" p. 136, figure 11-11: [Pierce 3rd ed.] the value syntax for variants is missing. It should read: v ::= ... as T also, "field labels" would be better called "variant labels" here. p. 137, paragraph 3 [Pierce 3rd ed.] "finite mappings" should be "partial mappings" p. 142 [Pierce 1st ed. *] top line is garbled (some latex markup for index entries got into the text instead) p. 142, line 4 [Sumii] A space should be removed before |. p. 144, line 4 [Pierce 3rd ed.] T should be T1 p. 146 [Pierce 3rd ed.] Lists are not implemented in the fullsimple checker. p. 146 [Pierce 1st ed. **] footnote 9 is redundant with Exercise 11.12.2. p. 151, Lemma 12.1.5 [Sumii] "v1...,vn" -> "v1,...,vn" p. 152, line 1 [Pierce 3rd ed.] The first heavy open paren should be dropped. p. 152, line 3 [Pierce 3rd ed.] The first close paren should be in typewriter (heavy) font. p. 152, Exercise 12.1.7 [Pierce 3rd ed.] "Figure 3-1" should be "Figure 8-1" p. 152, Exercise 12.1.7 [Sumii *] The solution has an error; see p. 512, Solution 12.1.7 [Sumii *] p. 152, Exercise 12.1.7 [Sumii] The solution has an error; see p. 513, line 1 [Sumii] p. 152, Exercise 12.1.7 [Sumii] The solution has an error; see p. 513, line 5 [Sumii] p. 152, Exercise 12.1.7 [Sumii] The solution has an error; see p. 513, line 6 [Sumii] p. 152, Exercise 12.1.7 [Sumii] The solution has an error; see p. 513, line 12, "Let vi be" [Sumii] p. 152, "Tait's strong normalization proof corresponds exactly [Sumii **] to an algorithm for evaluating simply typed terms, known as normalization by evaluation or type-directed partial evaluation" Actually, normalization by evaluation (or type-directed partial evaluation) corresponds to _weak_ normalization; see http://www.cse.chalmers.se/~peterd/slides/Leicester.pdf for example. p. 155, first line [Pierce 1st ed. *] missing "of" between "result" and "the" p. 162, 166 [Pierce 3rd ed.] The notation for extending stores with new mappings is a little inconsistent ("[l |-> v2]\mu" in some places and "\mu, l |-> v1" in others). Note, though, that "[l |-> v2]\mu" assumes l \in \dom(\mu) while "\mu, l |-> v1" assumes the converse (so perhaps having two notations is useful). p. 162, Exercise 13.3.1 [Pierce 3rd ed.] The solution has an error; see p. 515, solution to 13.3.1 [Pierce 3rd ed.] p. 162, line -3 [Sumii] "l2" should be in math style. p. 163 [Pierce 3rd ed.] The last l_1 on the pge should be l_2 p. 166 [Pierce 3rd ed.] In the syntax of stores, = should be \mapsto p. 167, definition 13.5.1 (and following material) [Pierce 3rd ed.] It would be better to fix an empty context here rather than allowing an arbitrary one. (See the comment above for p. 107.) p. 168, near the middle [Sumii] "on the values of all the old locations" -> "on the types of all the old locations" p. 168, para 3, line 5 [Pierce 1st ed. **] \mu should be \Sigma in "or else it is exactly ..." also, in line 7 of the paragraph below Thm 13.5.3 (\mu, l \mapsto v_1) should be [l \mapsto v_1]\mu p. 169, Exercise 13.5.8 [Sumii *] The solution has an error; see p. 516, line 1-2 [Sumii *] p. 176, line 10 [Sumii] "In T-Raise we demand" -> "In T-Exn we demand" p. 177, l 8 [Pierce 3rd ed.] "l_n:t_n" -> "l_n:T_n" p. 177, line -15, "it falls through to the else clause" [Sumii] Perhaps "the wildcard clause" may be more accurate. p. 184 [Pierce 3rd ed.] In "most variants of Abadi and Cardelli's object calculus omit width subtyping", "width" should be replaced by "depth." p. 188, Exercise 15.3.1 [Pierce 3rd ed.] The solution has an error; see p. 519, top two displays [Pierce 3rd ed.] p. 189, proof of 15.3.4 [Pierce 3rd ed.] "By induction on typing derivations" should be "By induction on the depth of the given typing derivation". p. 190, Lemma 15.3.6, part 2 [Pierce 3rd ed.] {k_j=v_j ^ {a \in 1..m}} should be {k_a=v_a ^ {a \in 1..m}} p. 191, near the middle [Sumii *] "{ka=vj a \in 1..m}" -> "{ka=va a \in 1..m}" "with |-vj:Ti for each li=kj" -> "with |-va:Ti for each li=ka" p. 203 [Pierce 3rd ed.] in the last rule, S-RcdPerm, the part below the vertical line, instead of {l_i:S_i ...} <: {l_i:T_i ...} it should say: {k_j:S_j ...} <: {l_i:T_i ...} p. 203, right-hand side of definition of [[ ]] for (S-RcdPerm) [Sumii *] "kj:[[Si]]" -> "kj:[[Sj]]" p. 204, second equation in definition of [[ - ]] [Pierce 3rd ed.] \x:T1 should be \x:T1.t2 p. 206, first sentence of third para [Pierce 3rd ed.] In "The inhabitants of the intersection type T_1 /\ T_2 are terms belonging to both S and T", S and T should be T_1 and T_2. p. 206, S-Inter4 [Sumii] It may perhaps be better to add parentheses like: (S->T1) /\ (S->T2) <: S->(T1/\T2) p. 208, chapter quote [Pierce 1st ed. **] Mannasse should be Manasse p. 211, Figure 16-1 [Sumii] The symbols on the top left should be a little larger. p. 215, near the middle [Sumii **] "the left-hand subderivation has been pushed up" -> "the right-hand subderivation of the original instance of T-App has been pushed up" p. 220, (TA-If) [Sumii] All the turnstyles "|-" should be "|->". p. 220, exercise 16.3.4 [Pierce 1st ed. *] 15-5 should be 15.5 p. 220, Exercise 16.4.1 [Pierce 3rd ed.] The solution has an error; see p. 526, solution to 16.4.1 [Pierce 3rd ed.] p. 226, footnote 1: [Pierce 1st ed. **] "Other languages, such as and , ...". The words "Java" and "C++" are missing p. 232, line -3 [Pierce 3rd ed.] "C++ and ," should be "C++ and Java," p. 237, line -7 [Sumii *] "E-Fix" -> "E-FixBeta" p. 243, line 3 [Pierce 3rd ed.] Ref InstrCounter <: Ref SetCounter should be Source InstrCounter <: Source SetCounter p. 248, line -1 [Sumii *] It is unknown what "enumerations" mean here. p. 255, line -8 [Sumii] "this.f1=f1;...;this.fn=fn;" -> "this.f1=f1;...this.fn=fn;" p. 256, line -3, "the <: relation is antisymmetric" [Sumii *] (Cf. p. 257, Exercise 19.4.1 and p. 530, Solution 19.4.1) In addition, C should not be equal to D in any class declaration class C extends D {...}. p. 261, line -6 [Sumii *] "cannot perform a downcast" -> "cannot perform a cast" p. 263, line -9 [Sumii *] "the original used a nondeterministic beta-reduction relation" -> "the original used a nondeterministic reduction relation" p. 268, picture [Pierce 1st ed. **] the braces in "{nil: , cons: }" should look like "" p. 273, line 4 [Sumii] "fixed-point constructor" -> "fixed-point combinator" (This may be intentional, for avoiding repetition.) p. 273, first paragraph [Pierce 3rd ed.] the erasure of the fix combinator defined here is not quite the same as the fix defined on p. 65: this one is missing the abstractions on y (which are needed to make it work in the call-by-value setting). p. 273, sentence immediately below definition of diverge function [Pierce 3rd ed.] repeated "can" p. 274, definition of fixD [Pierce 3rd ed.] This is actually an implementation of the call by name fixed point combinator (Y), not the call by value one defined on page 65 (that one can also be encoded using recursive types, though). p. 278, line 3 [Sumii] "every datatype definition implicitly introduces a recursive type" -> "every datatype definition may implicitly introduce a recursive type" (The former is an overstatement: there _are_ non-recursive datatype definitions such as 'a option, of course.) p. 279, Section 20.4 [Sumii] "Basic syntactic and semantic properties (without subtyping) are collected in Cardone and Coppo (1991)." and "Basic syntactic and semantic properties of recursive types without subtyping were established in early papers by Huet (1976) and MacQueen, Plotkin, and Sethi (1986)." -> "Basic syntactic and semantic properties of recursive types without subtyping were established in early papers by Huet (1976) and MacQueen, Plotkin, and Sethi (1986), and are collected in Cardone and Coppo (1991)." p. 280 [Pierce 2nd ed. **] The citations for early papers on syntactic properties of recursive types (without subtyping) should also mention an paper by Claude Pair, published in Algol Bulletin n. 31, March 1970, which contains what appears to be the first proof of the decidability of equality for equi-recursive types. A scanned copy of the paper has kindly been made available by Pierre Lescanne, at the following URL: http://www.ens-lyon.fr/~plescann/PUBLICATIONS/RecursiveTypes/ p. 284, Exercise 21.1.9 [Pierce 1st ed. **] The solution has an error; see p. 538, lines 1 and 8 [Pierce 1st ed. **] p. 286, line 5 in the first paragraph of Section 21.3 [Sumii] "their fixed points" -> "its fixed points" p. 287, Exercise 21.3.4 [Pierce 3rd ed.] The solution has an error; see p. 539, solution to 21.3.4 [Pierce 3rd ed.] p. 291, Exercise 21.5.2, "subtyping relations" [Sumii] Here (and in a few other places throughout the book), a "subtyping relation" is a synonym of a "subtype relation" (Section 15.2). Note that there is also an "algorithmic subtyping relation" (Definition 16.1.4), which is different. p. 292, line -10 [Sumii] "consistent" -> "F-consistent" p. 299, proof of 21.7.4 [Pierce 3rd ed.] "Observe that reachable_{S_r}(S, T) \subseteq subtrees(S) * subtrees(T)" does't take into account contravariance in the function subtyping rule, such that the line should be changed to: "Observe that reachable_{S_r}(S, T) \subseteq (subtrees(S) * subtrees(T)) U (subtrees(T) * subtrees(S))." p. 301 [Pierce 1st ed. *] 'An sample' -> 'A sample' p. 302, Exercise 21.8.5 [Pierce 1st ed. **] The solution has an error; see p. 541, proof sketch of Lemma A.17 [Pierce 1st ed. **] p. 303, line 13 [Pierce 1st ed. *] "Q \in T \times T" should be "Q \subseteq T \times T" p. 303, line -8 [Pierce 1st ed. *] "we claim that R={...}" -> "we claim that R={...} is such a set" p. 308, line 6 [Sumii *] "S = [X<=Q]T" -> "S <= [X<=Q]T" p. 308, last line [Pierce 3rd ed.] In "Take S' = [Y -> \mu Y.S']S_2 ...", the last S' should be T'. p. 320, Example 22.2.2 [Pierce 1st ed. **] The last solution is wrong. Correct alternatives include: ( [ X |-> Nat -> Nat -> Nat, Y |-> Nat ], Nat -> Nat ) or ( [ X |-> Nat -> Nat, Y |-> Nat ], Nat ) p. 321, para 1, 3rd to last line [Pierce 1st ed. **] t_1 should be T_1 p. 322, Figure 22-1, CT-App [Sumii *] "X \not\in X_1, X_2, T_1, T_2, C_1, C_2, \Gamma, t_1, or t_2" -> "X not mentioned in X_1, X_2, T_1, T_2, C_1, or C_2" (see also the erratum for Corollary 22.3.8; note that the side condition "X \not\in \Gamma, t_1, or t_2" is never used in the proofs) p. 324, line 3 [Pierce 1st ed. **] "Is a solution for (Gamma, t2, S2, C)" should be "Is a solution for ((Gamma,x:T1), t2, S2, C)" p. 325, lines 3 and 4 [Pierce 1st ed. **] T2 should be S2 in the third line and T1 should be S1 in the fourth line. p. 325, Corollary 22.3.8 [Sumii *] "Suppose \Gamma \vdash t : S | C." -> "Suppose \Gamma \vdash t : S |_X C where X \cap FV(\Gamma, t) = \emptyset." (for instance, consider t = if true then (\lambda y:Y.0)true else (\lambda z:Nat.0)0 when (\lambda z:Nat.0)0 is given the type Y by the original CT-App) p. 325, Exercise 22.3.9 [Pierce 3rd ed.] The solution has an error; see p. 542, solution to 22.3.9 [Pierce 3rd ed.] p. 333, line 10 [Sumii] "Ct-AbsInf" -> "CT-AbsInf" p. 334, para 1, line 1 [Pierce 1st ed. *] "One caveat is here that" should be "One caveat here is that" p. 334, line 1-2 [Sumii] "variables T1" -> "variables in T1" p. 334, last full paragraph [Pierce 1st ed. *] "in the right-hand sides of other lets---rather than in their bodies, where nesting of lets is common---" should be cut (in Mairson's example, each let is nested in the previous one's body) p. 334, near the bottom [Sumii **] This example is not appropriate - it is slow in OCaml only because of the particular implementation of occurs checks (try "-rectypes") and printing types (insert "ignore"). A better example, due to Jacques Garrigue, is: let l0 = ([], [], [], []) in let l1 = (l0, l0, l0, l0) in let l2 = (l1, l1, l1, l1) in ...(snip)... let l9 = (l8, l8, l8, l8) in ignore (l9) p. 335, line 8, "(r:=(\lambda x:Nat. succ x); (!r)true);" [Sumii] Insert a line break after ";" (because the main text that follows talks about "the third line"). p. 336, line 11 [Sumii *] "X->X" -> "Ref(X->X)" "\forall X. X->X" -> "\forall X. Ref(X->X)" p. 337, line 3 [Sumii] "Algorithm W (Damas and Milner) of Damas and Milner" -> "Algorithm W of Damas and Milner" p. 337, line -7 [Sumii] "Remy" -> "R\'emy" p. 338, para 4, 2nd to last line [Pierce 1st ed. *] "e.g. using by" should be "e.g. by using" p. 339, second sentence below the definition of multiple doubling functions [Pierce 3rd ed.] "If we want apply" should be "If we want to apply". p. 342, line -7 [Sumii *] "for t" -> "for t2" p. 342, near bottom [Pierce 3rd ed.] In addition to We continue the convention (5.3.4) that the names of (term or type) variables should be chosen so as to be different from all the names already bound by $\Gamma$, ... we should add the restriction that a context of the form $\Gamma, x : T$ is well-formed only if every type variable free in $T$ is bound by $\Gamma$. p. 349, Exercise 23.4.6 [Sumii] "iszero" -> "iszro" p. 349, Exercise 23.4.6 [Pierce 3rd ed.] The solution has an error; see p. 546, solution to 23.4.6 [Pierce 3rd ed.] p. 350, Exercise 23.4.9 [Sumii] "function pred" -> "function prd" p. 354, second para [Pierce 3rd ed.] "A term M" should be "A term m" p. 354, definition of partial type erasure [Pierce 3rd ed.] The definition of Pfenning's partial erasure function is not quite right. The correct definition (with slightly different syntax) appears here: http://www.cs.cmu.edu/~fp/papers/CMU-CS-92-105.pdf p. 354, Theorem 23.6.2 [Pierce 2nd ed. **] The cited articles by Boehm (85 and 89) actually prove a slight variant of the stated result. Other variants (closer to the stated one) can be found in Pfenning (1993a). Surprisingly, though, the decidability of precisely this partial type inference problem appears still to be open. p. 356, exercise 23.6.3 [Pierce 3rd ed.] We part (1) is not actually useful later; it can be dropped (except for the definition of exposed). (2) should be used instead of (1) in the proof of (4). Also, the first occurrences of A and B in part (4) should have overbars. p. 356, Exercise 23.6.3 [Sumii *] The solution has an error; see p. 550, near the middle [Sumii *] p. 359, line 23 [Sumii **] "Kfoury and Wells (1999) gave the first correct" -> "Kfoury and Wells (1994) gave the first direct" where "Kfoury and Wells (1994)" is: http://dx.doi.org/10.1145/182590.182456 p. 371, line 1 [Pierce 3rd ed.] ATD should be ADT p. 371, Exercise 24.2.1 [Sumii *] "Use the List type introduced in Exercise 23.4.3" -> "Use the List type introduced in Section 23.4" p. 382, Exercise 25.2.1 [Sumii *] The solution has an error; see p. 554, Solution 25.2.1, last line [Sumii *] p. 394 [Pierce 1st ed. **] In the rule S-All, the premise "Gamma |- U1 :: K1" should be omitted. p. 398, line 6 [Sumii] "l : L" -> "l \in L" p. 401, Lemma 26.4.1 [Sumii *] In this chapter, "well-formed" means "well-scoped" (pp. 393-394). p. 402, line 11, "only in the part of the environment" [Sumii] Again, a "type environment" is a synonym of a typing context. p. 402, Proof of 26.4.8 [Pierce 3rd ed.] In the case for S-TVar, if Y=X, then [X -> P]S = P (not Q), which requires G |- P <: Q (from the premise) to reach the desired result. p. 403, line 2 [Sumii *] "[X|->P]T" -> "[X|->P]S" p. 404, proof of 26.4.13 [Pierce 3rd ed.] In the second subcase of the argument for T-TApp, the reference to 26.4.6 should instead be to 26.4.9. p. 405, proof of 26.4.14 (near the end) [Pierce 3rd ed.] The -> in \forall X<:T_1 -> S_2 should be a dot. p. 405, proof of 26.4.15 [Pierce 3rd ed.] The E-TApp1 should be E-TApp. p. 408, line -6 [Sumii] "Curien and Ghelli (1992, Ghelli, 1990)" -> "Curien and Ghelli (1992; Ghelli, 1990)" p. 409, line 2 [Sumii] "Bruce (Bruce, 1991)" -> "Bruce (1991)" p. 411 [Pierce 3rd ed.] The whole of chapter 27 is not very convincing. The purpose in using Fsub is supposedly to enable us to create the method table just once per class, rather than once per object. The code indeed manages to have it create something just once for each class, but that something is a *function* that creates the method table *at every open self recursive call*! (See the "(!self r)" calls that happen during a method invocation.) In other words, the final efficiency is worse than what we ended up at the end of Chapter 18. Many thanks to John Tang Boyland for pointing this out! John also proposes a different case study, using f-omega-sub in the style of chapter 32 to implement objects in an imperative style. A sketch of the main constructions can be found here: http://www.cis.upenn.edu/~bcpierce/tapl/boyland-object-encoding.txt Some code implementing the idea is here: http://www.cs.uwm.edu/classes/cs790/types-f2003/Chapter27-replacement.txt http://www.cs.uwm.edu/classes/cs790/types-f2003/fullfomsubref.tar.gz p. 411, line 12 [Sumii] "SetCounterRep" -> "CounterRep" p. 412, near the middle [Sumii] "be able coerce" -> "be able to coerce" p. 412, footnote [Pierce 3rd ed.] The description of method lookup in real-world OO languages is misleadingly simplistic: real implementations do things that are much fancier and more efficient than this. p. 418, throughout Section 28.1 [Sumii] "|-" should be "|->" in exposures. p. 422, line 5-7 [Sumii] "algorithmic typing statements" -> "algorithmic subtyping statements" "original typing statements" -> "original subtyping statements" p. 423, definition 28.3.4 [Pierce 3rd ed.] The weight of a subtyping statement should be defined as the *sum* (not the max) of the weights of S and T. Also, it would help to note explicitly that the weight function is well defined because the total size of all the types in Gamma plus the size of the type whose weight is being defined always decreases. p. 425, lemma 28.4.1, case 1: [Pierce 1st ed. **] ``Suppose that $\Gamma$ is a'' should be ``Suppose that $\Delta$ is a'' p. 426, line 4 [Sumii] "\Gamma |- S <: Top" -> "\Gamma |-> S <: Top" p. 426, line 10 [Sumii] "\Gamma |- U <: Q" -> "\Gamma |-> U <: Q" p. 429, line 10, "equivalent to \neg S \/ T" [Sumii] Insert "(in classical logic)". p. 431, line 4 [Sumii] Here, a "subtype statement" means a "subtyping statement". p. 433, l -4 [Pierce 1st ed. *] \Gamma U \/ T = J. should be replaced with \Gamma |-> U <: V. By the induction hypothesis, \Gamma |- U \/ T = J for some J with \Gamma |- J <: V. By the third clause in the definition, \Gamma |- S \/ T = J. p. 436, line 11 [Sumii *] "supertypes T" -> "supertypes of T" p. 436, Exercise 28.7.2 [Sumii **] The solution has an error; see p. 559, line -6 [Sumii **] and p. 559, line -6 [Sumii] p. 439, para 3, line 2 [Pierce 1st ed. *] "type constructorstype operators" should be just "type constructors" p. 441, line -3 [Sumii] The left parenthesis should be in typewriter (heavy) font. p. 444, Exercise 29.1.1 [Sumii] The solution has an error; see p. 560, Figure A-2, left, line 2 [Sumii] p. 444, line -1 [Sumii] The last ";" should be dropped. p. 444, footnote [Pierce 1st ed. *] wrong font for ' p. 445, line 1 [Sumii] ";" should be dropped. p. 455, Exercise 30.3.8 [Sumii *] The solution has an error; see p. 561, near the middle [Sumii *] p. 457, proof of Lemma 30.3.13 [Sumii *] "Lemma 30.3.12(1) gives us" -> "Corollary 30.3.11 and Lemma 30.3.12(1) give us" p. 459, Definition 30.3.18 [Sumii *] "and \Gamma |- T :: *" -> "and \Gamma1 |- T :: *" p. 461 [Pierce 3rd ed.] The type operator "Class" is not actually used in Chapter 32. p. 462, para 2 [Pierce 3rd ed.] "abstraction \x:T.t_2 is a family of terms [x <- s]t_1" should end "[x <- s]t_2" p. 462, near the middle [Sumii] "family of types indexed by types." -> "family of types indexed by types" p. 468, line -7 [Sumii] "If we let Top[*] = Top and define(maximal elements of higher kinds)" -> "If we let Top[*] = Top and define" p. 469, exericse 31.2.1 [Pierce 3rd ed.] The exercise is correct as stated, but it would have been more interesting if instead of (or in addition to) "FB <: FB" it had asked whether "FA <: FB" holds. Also, in the second and third parts from the bottom, it would have been clearer to use G instead of F. p. 471, figure 31-1 [Pierce **] The S-App rule as stated does not ensure that the two types are well kinded. Two extra premises (Gamma |- S1 U :: K and \Gamma |- T1 U :: K) should be added. (The second might be redundant.) p. 484, Figure 32-1 [Sumii **] The following congruence rules should be added: t1 ---> t1' ---------------------------- t1<-li=t2 ---> t1'<-li=t2 t2 ---> t2' -------------------------- v<-li=t2 ---> v<-li=t2' p. 486, first line of Section 32.9 [Sumii *] "In 18.9" -> "In 18.11" p. 488, first sentence of 32.10 [Pierce 1st ed. *] it introduced => it was introduced p. 494, solution to exercise 3.5.13 [Pierce 3rd ed.] the diamond lemma as stated is false: In the case where r->s by E-IfFalse and r->t by E-Funny2, we have t->s, rather than s->u and t->u for any u. It should be restated as follows: LEMMA: If r->s and r->t, then either s->t or t->s or there is some u such that s->u and t->u. The argument in the diagram chase below must now be slightly refined to take the modified lemma into account. p. 494, Lemma A.1 [Sumii] The correct statement would be: If r->s and r->t, with s \neq t, then either s->t or t->s or there is some term u such that s->u and t->u. (The online errata lacks "with s \neq t".) p. 496, line -7 [Sumii] "Theorem 3.5.14" -> "The property in Exercise 3.5.14" p. 496, solution to 3.5.16 [Pierce 3rd ed.] To fully capture the informal claim that "the original and new semantics agree," Proposition A.2 should be augmented with another (almost obvious) property: PROPOSITION: g --o-->* v iff g --w-->* v, for all original terms g. p. 497, subcase g1 = succ g1 [Pierce 1st ed. **] The argument for this subcase should conclude "From this derivation, w we construct a derivation of g -->* if wrong then g2 else g3, which w after a final instance of E-If-Wrong yields g -->* wrong p. 499, 4.2.1 [Pierce 1st ed. **] the constructor 'Some' was incorrectly typeset (twice) as \exists p. 499, Lemma A.8, E-IfTrue and E-IfFalse cases [Pierce 1st ed. **] the second t_2 should be t_3 p. 499, end of A.8 [Pierce 3rd ed.] both occurrences (in cases E-IfTrue and E-IfFalse) of "then t2 else t2" should be "then t2 else t3" p. 499, Proof of Proposition A.9 [Sumii **] The induction does not work in the case t = succ t1, because the number of evaluation steps is _the same_ for t and t1. A correct proof can be done by induction on the structure of t (though it does not extend to more sophisticated calculi like lambda-calculus), or by proving another lemma like if t --> t' and t' ==> v, then t ==> v by induction on the derivation of t --> t'. p. 500, solution 5.2.4 [Pierce 1st ed. *] the names of the arguments m and n should be exchanged p. 501, solution to 5.2.11 [Pierce 3rd ed.] in the second to last line of the solution, sumlist should be sumlist' p. 503, solution 5.3.8 [Pierce 1st ed. **] t' should be called v p. 503, solution to 6.1.5 [Pierce 3rd ed.] the subscripts in the third and sixth clauses should be just "Gamma", not "Gamma,x" p. 505 [Pierce 1st ed. **] exercise 9.4.1 is misfiled (it can be found between 9.2.3 and 9.3.2) p. 506 [Pierce 1st ed. **] ".... But this means that size(T1) is strictly greater than size(T1 -> T2), ..." should read "... size(T1) is equal to size(T1 -> T2) ..." [It is impossible because all types in this system have finite size.] Also, there is no formal definition of the "size" of a type. This can be taken to be the number of nodes in its tree representation. p. 506, near the middle [Sumii] Remove the "(" before "\Gamma". p. 507, solution to 9.3.10 [Pierce 3rd ed.] The term given doesn't actually reduce under the call-by-value rules. A better example would be: (\x:Bool->Bool. \y:Bool. y) (\z:Bool. true true) p. 507, solution to 11.3.2 [Pierce 1st ed. **] The conclusion in T-Wildcard should read Gamma |- \_:T1.t2 : T1->T2 not Gamma |- \_.t2 : T2 p. 508, solution to 11.4.1 [Pierce 3rd ed.] The third "x" on the second line should be deleted. p. 508, solution to 11.4.1, last line [(a student of) Sumii] "\rightarrow^*" -> "\rightarrow_I^*" p. 510, top of page [Pierce 3rd ed.] The "\in" in the conclusion of rule P-Rcd' should be ":" p. 510, near the middle [Sumii *] "C-Let" -> "T-Let" (twice) p. 512, Solution 12.1.7 [Sumii *] Apply the online errata (for the 1st printing) but replace t1, t2, and t3 with \sigma t1, \sigma t2, and \sigma t3, respectively. p. 513, line 1 [Sumii] "R_T2 \sigma t" -> "R_T2(\sigma t)" p. 513, line 5 [Sumii] "R_{T1->T2} v2" -> "R_{T1->T2}(v2)" p. 513, line 6 [Sumii] "R_{T1->T2} v3" -> "R_{T1->T2}(v3)" p. 513, line 12, "Let vi be" [Sumii] The variable vi is already used in the statement of Lemma 12.1.5. Here, it should perhaps be renamed to, say, wi. p. 515, solution to 13.3.1 [Pierce 3rd ed.] The restriction to finite memories is not absolutely necessary -- we can also talk about garbage collecting an infinite memory. But it makes part 5b more interesting E-RefV should be modified to add that the new location l must be in L. The text in part 5 is a little mangled. In 5a, what is meant is that, if evaluation is possible with GC, then the same evaluation is possible *in an infinite store* without GC, but this is not what is written. Similarly in part b. (We might also be interested in comparing runs of the same program with respect to a *finite* store, with and without the GC rule. For example, if the program runs to completion without GC, it should reach the same result with GC, though perhaps with renamed labels.) Also, note that progress and preservation depend on a store typing, and in the current statement of preservation the store typing only increases. With gc, we need to be able to "gc the store typing" too. p. 516, line 1-2 [Sumii *] "strongly normalizing" -> "normalizing" (This language is not even confluent!) p. 519, top two displays [Pierce 3rd ed.] the derivations should say "\Gamma |- t : S" and "\Gamma |- t : U" rather than "\Gamma |- t \in S" and "\Gamma |- t \in U" p. 526, solution to 16.4.1 [Pierce 3rd ed.] The 'if' typing rule (+ alternative) uses normal turnstiles; it should use algorithmic turnstiles. p. 538, lines 1 and 8 [Pierce 1st ed. **] $X \subseteq P$ implies $F(X) \subseteq P$ should be $F(P) \subseteq P$ (Fixed in later printings?) p. 539, solution to 21.3.4 [Pierce 3rd ed.] "the set pairs R = {(T(pi),T(pi)) | pi in {1,2}*}" should be "the set of pairs R = {(Q,Q) | Q a subtree of T}" It is not quite true that (mu S) only relates finite types: every type (even an infinite one) is a subtype of Top. A more complex argument is needed here. In the second paragraph, "follow" should be "can" and "byu induction on the size T" should be "by induction on the sum of the sizes of S and T." p. 541, proof sketch of Lemma A.17 [Pierce 1st ed. **] The first sentence should read "By induction on k = mu-height(S)." p. 542, solution to 22.3.9 [Pierce 3rd ed.] The end of the proposed lemma should read "... then every type variable mentioned in T or C is mentioned in Gamma, t, or F\F'." p. 546, solution to 23.4.6 [Pierce 3rd ed.] false and true should be fls and tru p. 550, near the middle [Sumii *] "R-Beta2" -> "R-TappTabs" p. 554, Solution 25.2.1, last line [Sumii *] \uparrow_0^d(T) and \uparrow^d(T) should be swapped. p. 559, line -6 [Sumii **] "\neg S = \forall X<:S.X" -> "\neg S = S->Top" (We are not supposed to use \forall here! In fact, it suffices to define \neg so that it is just contravariant.) p. 559, line -6 [Sumii] "[[X1<:T1,,...,Xn<:Tn]]" -> "[[X1<:T1,...,Xn<:Tn]]" p. 560, Figure A-2, left, line 2 [Sumii] "if X \not\in FVS" -> "if X \not\in FV(S)" p. 561, near the middle [Sumii *] "T12'" -> "T12" "T2'" -> "T2" p. 566, line -3 [Sumii *] "T1 x T2" -> "T11 x T12" p. 568, Abramsky, Samson, Radha Jagadeesan, and Pasquale Malacaria [Sumii] "Full abstraction for pcf" -> "Full abstraction for PCF" p. 571, Brandt, Michael and Fritz Henglein [Sumii] "Proc. 3d Int'l Conf. on" -> "Proc. 3rd Int'l Conf. on" (In fact, the actual title of the volume is: "Typed Lambda Calculi and Applications, Third International Conference on Typed Lambda Calculi and Applications, TLCA '97, Nancy, France, April 2-4, 1997, Proceedings") p. 572 [Sumii] "Canning, Peter, William Cook, Walt Hill, and Walter Olthoff" -> "Canning, Peter, William Cook, Walter Hill, and Walter Olthoff" p. 572, Canning, Peter, Walt Hill, and Walter Olthoff [Sumii] Although the original technical report is unavailable, its correct title (according to references from other papers including the authors') seems to be: "Towards a kernel language for object-oriented programming". p. 572, Canning, Peter, William Cook, Walter Hill, Walter Olthoff, and [Sumii] John Mitchell "F-bounded quantification for object-oriented programming" -> "F-bounded polymorphism for object-oriented programming" p. 577, Drossopoulou, Sophia, Susan Eisenbach, and Sarfraz Khurshid [Sumii] "7(1):3-24" -> "5(1):3-24" Also, since this is a paper (not a book), the title here should perhaps be (un)capitalized like: "Is the Java type system sound?" p. 579, lines -7 and -4 [Sumii] "Garrigue, Jaques" -> "Garrigue, Jacques" p. 580, Grattan-Guinness, Ivor [Sumii] Since this is a book (not a paper), the title should be in the headline style: "The Search for Mathematical Roots, 1870-1940: Logics, Set Theories and the Foundations of Mathematics from Cantor through Russell to Goedel". p. 582, Hennessy, Matthew [Sumii] "A Semantics of" -> "The Semantics of" An online copy of this book is currently available from: https://www.scss.tcd.ie/Matthew.Hennessy/slexternal/resources/sembookWiley.pdf p. 584, line 3 [Sumii] "1,2, ...,\omega" -> "1,2,...,\omega" p. 586, line 9 [Sumii] "DEXPTIME" should be in regular (not small) capital letters. p. 589, McKinna, James and Robert Pollack [Sumii] "Pure Type Sytems formalized" -> "Pure Type Systems formalized" p. 595, Plasmeijer, Marinus J. [Sumii] "CLEAN: a programming environment" -> "CLEAN: A programming environment" p. 596, Remy, Didier and Jerome Vouillon [Sumii] "Theory And Practice of Object Systems" -> "Theory and Practice of Object Systems" Even though it is often abbreviated as "TAPOS", this seems to be the official name of the journal: http://onlinelibrary.wiley.com/journal/10.1002/(ISSN)1096-9942 p. 599, Studer, Thomas [Sumii] "featherweight java" -> "Featherweight Java" p. 600, line 7 [Sumii] "TIL : A type-directed" -> "TIL: A type-directed" p. 603, Yelick, Kathy, ... [Sumii] "Titanium: a high-performance" -> "Titanium: A high-performance" p. 608, right [Sumii] The item "equi-recursive types" appears twice; it should be unified. p. 610, left, "garbage collection" [Sumii] "158-165" -> "158" p. 615, under "references" [Sumii] The subitems "and subtyping" and "subtyping" should be unified.