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. 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, Exercise 22.3.9 [Pierce 3rd ed.]
The solution has an error; see p. 542, solution to 22.3.9 [Pierce 3rd ed.]
p. 332, Figure 22-1, CT-App [Sumii *]
"X \not\in X1, X2, T1, T2, C1, C2, \Gamma, t1, or t2"
->
"X not mentioned in X1, X2, T1, T2, C1, C2, \Gamma, t1, or t2"
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.