Errata for TYPES AND PROGRAMMING LANGUAGES (3rd printing)
==========================================================
NOTE: This file has been superceded by a new errata list compiled by Eijiro
Sumii and his collaborators while making the Japanese translation of TAPL.
It can be found here:
https://www.dropbox.com/s/9dkguftad519x0s/errata-trans.txt
___________________________________________________________________________
The first section of this file lists all the errors that I'm aware of in
the third printing of TAPL (errata for earlier printings are below). If
you find one that's not listed here, please let me know!
---------
in the source code for the checkers: In the TmTimesFloat case of the "pr"
function in syntax.ml in most of the checkers, the first occurrence of
"printtm_ATerm false ctx t2" should be "printtm_ATerm false ctx t1".
in the source code for checkers involving exceptions: The eval1 function is
missing cases for reducting "try" statements. Something like this should be
added:
| TmTry(fi,v1,t2) when isval ctx v1 ->
v1
| TmTry(fi,TmError(_),t2) ->
t2
| TmTry(fi,t1,t2) ->
let t1' = eval1 ctx t1 in
TmTry(fi, t1', t2)
in the source code for checkers involving subtyping and polymorphism: The
TyAll case of the join function is wrong. It reads:
| (TyAll(tyX,tyS1,tyS2),TyAll(_,tyT1,tyT2)) ->
if not(subtype ctx tyS1 tyT1 && subtype ctx tyT1 tyS1) then TyTop
else
let ctx' = addbinding ctx tyX (TyVarBind(tyT1)) in
TyAll(tyX,tyS1,join ctx' tyT1 tyT2)
The last line should read: TyAll(tyX,tyS1,join ctx' tyS2 tyT2).
-----------
p 28, 11th line from the bottom
S_i should be S_j (that is, it should read "t_1, t_2, t_3 are elements
of S_j")
p 35, after the displayed program fragment
"using E-If" should be "using E-IfTrue"
p 41, definition 3.5.15
the word "closed" is not needed here.
p. 53, footnote 2:
"the behaviors of some languages constructs"
should be
"the behaviors of some language constructs"
p 57, definition of call-by-value
"a term that is finished computing..." should be "a CLOSED term that is
finished computing..."
p 63, exercise 5.2.8
fold_left should be fold_right
p 67, figure 5-2
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 72, line 5
"values can be arbitrary lambda-terms" should read "values can be
arbitrary lambda-abstractions"
p. 73, exercise 5.3.8
4.2.2 should be 3.5.17
p. 76, exercise 6.1.1
the combinator called "plus" does not implement the addition function
(the solution in the back is correct, though)
p 78, second line of 6.2
"To to" -> "To do"
p 79, exercise 6.2.3
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. 87
"As in chapter 3" should be "As in chapter 4"
p 102, footnote 1:
"they will be sometimes be elided"
should be
"they will sometimes be elided"
p 106, proof of 9.3.8
"By induction on a derivation" should be "By induction on the depth
of a derivation"
p 107, Preservation theorem (and other preservation theorems throughout
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 110, part 2 of Theorem 9.5.2
the first "typed" should be "untyped"
p 114, l -10
"the variable type @'a@" should be "the type variable @'a@"
p 120, Theorem 11.3.1
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 130, second paragraph, second sentence
"affect" should be "effect"
p 136, figure 11-11:
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
"finite mappings" should be "partial mappings"
p 144, line 4
T should be T1
p 146
Lists are not implemented in the fullsimple checker.
p 152, line 1
The first heavy open paren should be dropped.
p 152, line 3
The first close paren should be in typewriter (heavy) font.
p 152, Exercise 12.1.7
"Figure 3-1" should be "Figure 8-1"
p 162, 166
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 163
The last l_1 on the pge should be l_2
p 166
In the syntax of stores, = should be \mapsto
p 167, definition 13.5.1 (and following material)
It would be better to fix an empty context here rather than allowing an
arbitrary one. (See the comment above for p. 107.)
p 177, l 8
"l_n:t_n" -> "l_n:T_n"
p 184
In "most variants of Abadi and Cardelli's object calculus omit width
subtyping", "width" should be replaced by "depth."
p 189, proof of 15.3.4
"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
{k_j=v_j ^ {a \in 1..m}} should be {k_a=v_a ^ {a \in 1..m}}
p. 203:
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 204, second equation in definition of [[ - ]]
\x:T1 should be \x:T1.t2
p 206, first sentence of third para
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 232, line -3
"C++ and ," should be "C++ and Java,"
p 243, line 3
Ref InstrCounter <: Ref SetCounter
should be
Source InstrCounter <: Source SetCounter
p 273, first paragraph
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
repeated "can"
p 274, definition of fixD
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 299, proof of 21.7.4
"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 308, last line
In "Take S' = [Y -> \mu Y.S']S_2 ...", the last S' should be T'.
p 339, second sentence below the definition of multiple doubling functions
"If we want apply"
should be
"If we want to apply".
p 342, near bottom
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 354, second para
"A term M" should be "A term m"
p 354, definition of partial type erasure
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 356, exercise 23.6.3
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 371, line 1
ATD should be ADT
p 402: Proof of 26.4.8
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 404, proof of 26.4.13
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)
The -> in \forall X<:T_1 -> S_2 should be a dot.
p 405, proof of 26.4.15
The E-TApp1 should be E-TApp.
p 411-416 (chapter 27)
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 412, footnote
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 423, definition 28.3.4
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 461
The type operator "Class" is not actually used in Chapter 32.
p 462, para 2
"abstraction \x:T.t_2 is a family of terms [x <- s]t_1"
should end "[x <- s]t_2"
p 469: exericse 31.2.1
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 494, solution to exercise 3.5.13
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 496, solution to 3.5.16
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 499, end of A.8
both occurrences (in cases E-IfTrue and E-IfFalse) of "then t2 else t2"
should be "then t2 else t3"
p 501, solution to 5.2.11
in the second to last line of the solution, sumlist should be sumlist'
p 503, solution to 6.1.5
the subscripts in the third and sixth clauses should be just "Gamma",
not "Gamma,x"
p 507, solution to 9.3.10
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. 508, solution to 11.4.1
The third "x" on the second line should be deleted.
p. 510, top of page
The "\in" in the conclusion of rule P-Rcd' should be ":"
p 515, solution to 13.3.1
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. 519, top two displays
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
The 'if' typing rule (+ alternative) uses normal turnstiles; it should
use algorithmic turnstiles.
p 539, solution to 21.3.4
"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 542, solution to 22.3.9
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
false and true should be fls and tru
p 562, solution to 30.5.1
FloatList should be just List
###########################################################################
###########################################################################
###########################################################################
Errata for TYPES AND PROGRAMMING LANGUAGES (2nd printing)
==========================================================
This section lists all the errors that I'm aware of in the second
printing of TAPL (not counting the errors listed above). They should be
corrected in the third printing.
SUBSTANTIVE ERRORS
------------------
p 96, second line of proof of 8.3.2
T-IsZero should be T-Zero
This error does *not* appear in the first printing. :-(
p 280:
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 354, Theorem 23.6.2
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 502, solution to 5.3.6
In the full beta-reduction rules, one is missing:
t1 -> t1'
--------------- (E-Abs)
\x.t1 -> \x.t1'
Also, na1' in rule E-App1 should be renamed t1'.
###########################################################################
###########################################################################
###########################################################################
Errata for TYPES AND PROGRAMMING LANGUAGES (1st printing)
==========================================================
The following errors appear only in the first printing -- they should all
be corrected in the second printing (Summer, 2002). The errors listed
above are also present in the first printing.
SUBSTANTIVE ERRORS
------------------
p xxi
Erik Hilsdale's name is spelled with a k
Fermin Reig's name should be typeset Ferm\'{\i}n
p 71, last line of display near top of page
There should be a close-paren after the second t1.
p 96, second to last line of T-If case in proof of 8.3.2
T-If should be E-If
p 97, T-If case in proof of 8.3.3
E-True and E-False should be E-IfTrue and E-IfFalse
p 107, end of first para
The annotation on y should be T2, not T1
p 146
footnote 9 is redundant with Exercise 11.12.2.
p 168, para 3, line 5
\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 208, chapter quote
Mannasse should be Manasse
p 226, footnote 1:
"Other languages, such as and , ...". The words "Java" and "C++"
are missing
p 268, picture
the braces in "{nil: , cons: }" should look like ""
p 320, Example 22.2.2
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
t_1 should be T_1
p 324, line 3
"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
T2 should be S2 in the third line and T1 should be S1 in the fourth
line.
p 394
In the rule S-All, the premise "Gamma |- U1 :: K1" should be omitted.
p 425, lemma 28.4.1, case 1:
``Suppose that $\Gamma$ is a'' should be ``Suppose that $\Delta$ is a''
p 497, subcase g1 = succ g1
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, Lemma A.8, E-IfTrue and E-IfFalse cases
the second t_2 should be t_3
p 499, 4.2.1
the constructor 'Some' was incorrectly typeset (twice) as \exists
p 503, solution 5.3.8
t' should be called v
p 505 to 507
exercise 9.4.1 is misfiled (it can be found between 9.2.3 and 9.3.2)
p 506 solution to 9.3.2
".... 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 507, solution to 11.3.2
The conclusion in T-Wildcard should read
Gamma |- \_:T1.t2 : T1->T2
not
Gamma |- \_.t2 : T2
p 538, lines 1 and 8
$X \subseteq P$ implies $F(X) \subseteq P$
should be
$F(P) \subseteq P$
(Fixed in later printings?)
p 541, proof sketch of Lemma A.17
The first sentence should read "By induction on k = mu-height(S)."
========================================================================
GRAMMATICAL / TYPOGRAPHICAL / COSMETIC ERRORS
---------------------------------------------
p 15
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 19
"P(0)" should be slanted in 2.4.1
p 25
"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
concete --> concrete
p 56
the middle item in the first sample reduction sequence has an extra
pair of parens
p 57
all occurrences of "call by X" should be hyphenated (except,
arguably, the first use of "call by need")
p 71, last line
the RHS should (arguably) be parenthesized to match the corresponding
line at the top of the page
p 142
top line is garbled (some latex markup for index entries got into the
text instead)
p 155, first line
missing "of" between "result" and "the"
p 220, exercise 16.3.4
15-5 should be 15.5
p 301
'An sample' -> 'A sample'
p 303, line 13
"Q \in T \times T" should be "Q \subseteq T \times T"
p 303, line -8
"we claim that R={...}" -> "we claim that R={...} is such a set"
p 334, para 1, line 1
"One caveat is here that" should be "One caveat here is that"
p 334, last full paragraph
"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 338, para 4, 2nd to last line
"e.g. using by" should be "e.g. by using"
p 433, l -4
\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 439, para 3, line 2
"type constructorstype operators" should be just "type constructors"
p 444, footnote
wrong font for '
p 488, first sentence of 32.10
it introduced => it was introduced
p 500, solution 5.2.4
the names of the arguments m and n should be exchanged
p 512, solution to exercise 12.1.7
The case for T-If proceeds by induction on T. This is more complicated
than necessary. By the induction, we know R bool t1, R T t2 and R T
t3. Since we know R bool t1, we know that t1 halts and is a bool. Hence,
the conditional will evaluate either to t2 or to t3. Then, by
preservation of R under evaluation, it suffices to show R T t2 or R T
t3, but they are immediate by induction. [Thanks to Edsko de Vries.]