Errata for TYPES AND PROGRAMMING LANGUAGES  (3rd printing)
==========================================================

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 <shift t up
    by d above cutoff c> 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 ::= ...
             <l=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 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 "<nil: , cons: >"

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