update the copyright

book.tex

@@ -26,7 +26,7 @@
 
 \def\racketEd{0}
 \def\pythonEd{1}
-\def\edition{1}
+\def\edition{0}
 
 % material that is specific to the Racket edition of the book
 \newcommand{\racket}[1]{{\if\edition\racketEd{#1}\fi}}
@@ -122,15 +122,35 @@ Cambridge, Massachusetts\\
 London, England}
 
 \begin{copyrightpage}
-  \textcopyright\ 2022 Jeremy G. Siek.  Available for free viewing
-  or personal downloading under the
-  \href{https://creativecommons.org/licenses/by-nc-nd/2.0/uk/}{CC-BY-NC-ND}
-  license.
+  \textcopyright\ 2022 Massachusetts Institute of Technology Press \\[2ex]
+  This work is subject to a Creative Commons CC-BY-ND-NC license. \\[2ex]
+  Subject to such license, all rights are reserved. \\[2ex]
+  \includegraphics{CCBY-logo}
+
+The MIT Press would like to thank the anonymous peer reviewers who
+provided comments on drafts of this book. The generous work of
+academic experts is essential for establishing the authority and
+quality of our publications. We acknowledge with gratitude the
+contributions of these otherwise uncredited readers.
+
+This book was set in Times LT Std Roman by the author. Printed and
+bound in the United States of America.
+
+Library of Congress Cataloging-in-Publication Data is available.
+
+ISBN:
+
+10 9 8 7 6 5 4 3 2 1
+
+  %% Jeremy G. Siek.  Available for free viewing
+  %% or personal downloading under the
+  %% \href{https://creativecommons.org/licenses/by-nc-nd/2.0/uk/}{CC-BY-NC-ND}
+  %% license.
   
-  Copyright in this monograph has been licensed exclusively to The MIT
-  Press, \url{http://mitpress.mit.edu}, which will be releasing the final
-  version to the public in 2022. All inquiries regarding rights should
-  be addressed to The MIT Press, Rights and Permissions Department.
+  %% Copyright in this monograph has been licensed exclusively to The MIT
+  %% Press, \url{http://mitpress.mit.edu}, which will be releasing the final
+  %% version to the public in 2022. All inquiries regarding rights should
+  %% be addressed to The MIT Press, Rights and Permissions Department.
 
 %% \textcopyright\ [YEAR] Massachusetts Institute of Technology
 
@@ -18674,11 +18694,11 @@ variables~\citep{Anderson:2002kd,Siek:2006bh}.
 The concrete syntax of \LangGrad{} is defined in
 Figure~\ref{fig:Lgrad-concrete-syntax} and its abstract syntax is
 defined in Figure~\ref{fig:Lgrad-syntax}. The main syntactic
-difference between \LangLam{} and \LangGrad{} is the additional
-\Param{} and \itm{ret} non-terminals that make type annotations
-optional. The type annotations are not optional in the abstract
-syntax; the parser fills in the \ANYTY{} type when a type annotation
-is absent.
+difference between \LangLam{} and \LangGrad{} is that type annotations
+optional, which is specified in the grammar using the \Param{} and
+\itm{ret} non-terminals. In the abstract syntax, type annotations are
+not optional but we use the \CANYTY{} type when a type annotation is
+absent.
 
 \newcommand{\LgradGrammarRacket}{
 \begin{array}{lcl}
@@ -18814,14 +18834,44 @@ is absent.
 \label{fig:Lgrad-syntax}
 \end{figure}
 
-
-
 Both the type checker and the interpreter for \LangGrad{} require some
 interesting changes to enable gradual typing, which we discuss in the
-next two sections in the context of the \code{map} example from
-Chapter~\ref{ch:Lfun}.  In Figure~\ref{fig:gradual-map} we revisit the
-\code{map} example, omitting the type annotations from the \code{inc}
-function.
+next two sections.
+
+% TODO: more road map -Jeremy
+
+%\clearpage
+
+\section{Type Checking \LangGrad{}}
+\label{sec:gradual-type-check}
+
+We begin by discussing the type checking of a partially-typed variant
+of the \code{map} example from Chapter~\ref{ch:Lfun}, shown in
+Figure~\ref{fig:gradual-map}.  The \code{map} function itself is
+statically typed, so there is nothing special happening there with
+respect to type checking. On the other hand, the \code{inc} function
+does not have type annotations, so parameter \code{x} is given the
+type \CANYTY{} and the return type of \code{inc} is \CANYTY{}.  Now
+consider the \code{+} operator inside \code{inc}. It expects both
+arguments to have type \INTTY{}, but its first argument \code{x}
+has type \CANYTY{}.  In a gradually typed language, such differences
+are allowed so long as the types are \emph{consistent}, that is, they
+are equal except in places where there is an \CANYTY{} type. That is,
+the type \CANYTY{} is consistent with every other type.
+Figure~\ref{fig:consistent} defines the
+\racket{\code{consistent?}}\python{\code{consistent}} method.
+%
+So the type checker allows the \code{+} operator to be applied
+to \code{x} because \CANYTY{} is consistent with \INTTY{}.
+%
+Next consider the call to the \code{map} function in
+Figure~\ref{fig:gradual-map} with the arguments \code{inc} and a
+tuple. The \code{inc} function has type
+\racket{\code{(Any -> Any)}}\python{\code{Callable[[Any],Any]}}
+but parameter \code{f} of \code{map} has type
+\racket{\code{(Integer -> Integer)}}\python{\code{Callable[[int],int]}}.
+The type checker for \LangGrad{} allows this because the two types are
+consistent.
 
 \begin{figure}[btp]
 % gradual_test_9.rkt
@@ -18856,28 +18906,6 @@ print(t[1])
 \label{fig:gradual-map}
 \end{figure}
 
-\section{Type Checking \LangGrad{}}
-\label{sec:gradual-type-check}
-
-The type checker for \LangGrad{} uses the \code{Any} type for missing
-parameter and return types. For example, the \code{x} parameter of
-\code{inc} in Figure~\ref{fig:gradual-map} is given the type
-\code{Any} and the return type of \code{inc} is \code{Any}. Next
-consider the \code{+} operator inside \code{inc}. It expects both
-arguments to have type \code{Integer}, but its first argument \code{x}
-has type \code{Any}.  In a gradually typed language, such differences
-are allowed so long as the types are \emph{consistent}, that is, they
-are equal except in places where there is an \code{Any} type. The type
-\code{Any} is consistent with every other type.
-Figure~\ref{fig:consistent} defines the
-\racket{\code{consistent?}}\python{\code{consistent}} method.
-Returning to the \code{map} example of
-Figure~\ref{fig:gradual-map}, the \code{inc} function has type
-\racket{\code{(Any -> Any)}}\python{\code{Callable[[Any],Any]}}
-but parameter \code{f} of \code{map} has type
-\racket{\code{(Integer -> Integer)}}\python{\code{Callable[[int],int]}}.
-The type checker for \LangGrad{} allows this
-because the two types are consistent.
 
 \begin{figure}[tbp]
   \begin{tcolorbox}[colback=white]
@@ -18921,17 +18949,17 @@ because the two types are consistent.
 \label{fig:consistent}
 \end{figure}
 
-
-Next consider a program with an error, such as applying \code{map} to
-a function that sometimes returns a Boolean, as shown in
-Figure~\ref{fig:map-maybe_inc}.  The type checker for \LangGrad{}
-accepts this program because the type of \code{maybe\_inc} is
-consistent with the type of parameter \code{f} of \code{map}, that is,
-\racket{\code{(Any -> Any)}}\python{\code{Callable[[Any],Any]}} is consistent
-with \racket{\code{(Integer -> Integer)}}\python{\code{Callable[[int],int]}}.
-One might say that a gradual type checker is optimistic
-in that it accepts programs that might execute without a runtime type
-error.
+It is also helpful to consider how gradual typing handles programs with an
+error, such as applying \code{map} to a function that sometimes
+returns a Boolean, as shown in Figure~\ref{fig:map-maybe_inc}.  The
+type checker for \LangGrad{} accepts this program because the type of
+\code{maybe\_inc} is consistent with the type of parameter \code{f} of
+\code{map}, that is,
+\racket{\code{(Any -> Any)}}\python{\code{Callable[[Any],Any]}}
+is consistent with
+\racket{\code{(Integer -> Integer)}}\python{\code{Callable[[int],int]}}.
+One might say that a gradual type checker is optimistic in that it
+accepts programs that might execute without a runtime type error.
 %
 The type checker for \LangGrad{} is defined in
 Figures~\ref{fig:type-check-Lgradual-1}, \ref{fig:type-check-Lgradual-2},
@@ -18999,23 +19027,28 @@ performs checking at runtime to ensure the integrity of the static
 types, such as the
 \racket{\code{(Integer -> Integer)}}\python{\code{Callable[[int],int]}}
 annotation on
-parameter \code{f} of \code{map}.  This runtime checking is carried
-out by a new \code{Cast} AST node that is generate in the
-new \code{cast\_insert} pass.  The output of the \code{cast\_insert}
-pass is a program in the \LangCast{} language, which adds \code{Cast}
-and \ANYTY{} to \LangLam{}.
+parameter \code{f} of \code{map}.
+Here we give a preview of how the runtime checking is accomplished;
+the following sections provide the details.
+
+The runtime checking is carried out by a new \code{Cast} AST node that
+is generate in a new pass named \code{cast\_insert}.  The output of
+\code{cast\_insert} is a program in the \LangCast{} language, which
+simply adds \code{Cast} and \CANYTY{} to \LangLam{}.
 %
 Figure~\ref{fig:map-cast} shows the output of \code{cast\_insert} for
 \code{map} and \code{maybe\_inc}.  The idea is that \code{Cast} is
 inserted every time the type checker sees two types that are
 consistent but not equal. In the \code{inc} function, \code{x} is
 cast to \INTTY{} and the result of the \code{+} is cast to
-\ANYTY{}.  In the call to \code{map}, the \code{inc} argument
+\CANYTY{}.  In the call to \code{map}, the \code{inc} argument
 is cast from
 \racket{\code{(Any -> Any)}}
 \python{\code{Callable[[Any], Any]}}
 to 
 \racket{\code{(Integer -> Integer)}}\python{\code{Callable[[int],int]}}.
+%
+In the next section we see how to interpret the \code{Cast} node.
 
 \begin{figure}[btp]
   \begin{tcolorbox}[colback=white]
@@ -19062,7 +19095,7 @@ print(t[1])
 {\if\edition\pythonEd        
 \begin{figure}[tbp]
 \begin{tcolorbox}[colback=white]  
-\begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
+\begin{lstlisting}[basicstyle=\ttfamily\footnotesize]
 class TypeCheckLgrad(TypeCheckLlambda):
   def type_check_exp(self, e, env):
     match e:
@@ -19074,16 +19107,12 @@ class TypeCheckLgrad(TypeCheckLlambda):
         return IntType()
       case Call(Name('input_int'), []):
         return IntType()
-      case BinOp(left, op, right) if op == Add() or op == Sub():
+      case BinOp(left, op, right):
         left_type = self.type_check_exp(left, env)
         self.check_consistent(left_type, IntType(), left)
         right_type = self.type_check_exp(right, env)
         self.check_consistent(right_type, IntType(), right)
         return IntType()
-      case UnaryOp(USub(), v):
-        ty = self.type_check_exp(v, env)
-        self.check_consistent(ty, IntType(), v)
-        return IntType()
       case IfExp(test, body, orelse):
         test_t = self.type_check_exp(test, env)
         self.check_consistent(test_t, BoolType(), test)
@@ -19091,36 +19120,6 @@ class TypeCheckLgrad(TypeCheckLlambda):
         orelse_t = self.type_check_exp(orelse, env)
         self.check_consistent(body_t, orelse_t, e)
         return self.join_types(body_t, orelse_t)
-      case UnaryOp(Not(), v):
-        ty = self.type_check_exp(v, env)
-        self.check_consistent(ty, BoolType(), v)
-        return BoolType()
-      case BoolOp(op, values):
-        left = values[0]; right = values[1]
-        left_type = self.type_check_exp(left, env)
-        self.check_consistent(left_type, BoolType(), left)
-        right_type = self.type_check_exp(right, env)
-        self.check_consistent(right_type, BoolType(), right)
-        return BoolType()
-      case Compare(left, [cmp], [right]) \
-          if isinstance(cmp, Eq) or isinstance(cmp, NotEq):
-        left_type = self.type_check_exp(left, env)
-        right_type = self.type_check_exp(right, env)
-        self.check_consistent(left_type, right_type, e)
-        return BoolType()
-      case Compare(left, [cmp], [right]) \
-          if isinstance(cmp, Lt()) or isinstance(cmp, LtE()) \
-             or isinstance(cmp, Gt()) or isinstance(cmp, GtE()):
-        left_type = self.type_check_exp(left, env)
-        self.check_consistent(left_type, IntType(), left)
-        right_type = self.type_check_exp(right, env)
-        self.check_consistent(right_type, IntType(), right)
-        return BoolType()
-      case Compare(left, [cmp], [right]) if isinstance(cmp, Is):
-        left_type = self.type_check_exp(left, env)
-        right_type = self.type_check_exp(right, env)
-        self.check_consistent(left_type, right_type, e)
-        return BoolType()
       case Call(func, args):
         func_t = self.type_check_exp(func, env)
         args_t = unzip([self.type_check_exp(arg, env) for arg in args])
@@ -19133,79 +19132,47 @@ class TypeCheckLgrad(TypeCheckLlambda):
             return AnyType()
           case _:
             raise Exception('type_check_exp: in call, unexpected ' + repr(func_t))
+      ...
       case _:
         raise Exception('type_check_exp: unexpected ' + repr(e))
 \end{lstlisting}
 \end{tcolorbox}
 
-\caption{Type checker for the \LangGrad{} language, part 1.}
+\caption{Type checking expressions in the \LangGrad{} language.}
 \label{fig:type-check-Lgradual-1}
 \end{figure}
 
 \begin{figure}[tbp]
 \begin{tcolorbox}[colback=white]  
-\begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
-      case Tuple(es, Load()):
-        ts = unzip([self.type_check_exp(e, env) for e in es])
-        return TupleType(ts)
-      case Subscript(tup, Constant(index), Load()) if isinstance(index,int)::
-        tup_ty = self.type_check_exp(tup, env)
-        match tup_ty:
-          case TupleType(ts):
-            return ts[index]
-          case AnyType():
-            return AnyType()
-          case _:
-            raise Exception('subscript expected a tuple, not ' + repr(tup_ty))
-      case Subscript(tup, index, Load()):
-        tup_ty = self.type_check_exp(tup, env)
-        index_ty = self.type_check_exp(index, env)
-        self.check_consistent(index_ty, IntType(), index)
-        match tup_ty:
-          case TupleType(ts):
-            return AnyType()
-          case AnyType():
-            return AnyType()
-          case _:
-            raise Exception('subscript a tuple, not ' + repr(tup_ty))
-      case Call(Name('len'), [tup]):
-        tup_t = self.type_check_exp(tup, env)
-        match tup_t:
-          case TupleType(ts):
-            return IntType()
-          case AnyType():
-            return IntType()
-          case _:
-            raise Exception('len expected a tuple, not ' + repr(tup_t))
-
-  def check_exp(self, e, ty, env):
+\begin{lstlisting}[basicstyle=\ttfamily\footnotesize]
+  def check_exp(self, e, expected_ty, env):
     match e:
       case Lambda(params, body):
-        match ty:
+        match expected_ty:
           case FunctionType(params_t, return_t):
             new_env = {x:t for (x,t) in env.items()}
             for (p,t) in zip(new_params, params_t):
                 new_env[p] = t
-            e.has_type = ty
+            e.has_type = expected_ty
           case AnyType():
             new_env = {x:t for (x,t) in env.items()}
             for p in new_params:
                 new_env[p] = AnyType()
             e.has_type = FunctionType([AnyType() for _ in new_params], AnyType())
           case _:
-            raise Exception('lambda does not have type ' + str(ty))
+            raise Exception('lambda does not have type ' + str(expected_ty))
       case _:
         e_ty = self.type_check_exp(e, env)
-        self.check_consistent(e_ty, ty, e)
+        self.check_consistent(e_ty, expected_ty, e)
 \end{lstlisting}
 \end{tcolorbox}
-\caption{Type checker for the \LangGrad{} language, part 2.}
+\caption{Checking expressions with respect to a type in the \LangGrad{} language.}
 \label{fig:type-check-Lgradual-2}
 \end{figure}
 
 \begin{figure}[tbp]
 \begin{tcolorbox}[colback=white]
-\begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
+\begin{lstlisting}[basicstyle=\ttfamily\footnotesize]
   def type_check_stmt(self, s, env, return_type):
     match s:
       case Assign([Name(id)], value):
@@ -19214,24 +19181,7 @@ class TypeCheckLgrad(TypeCheckLlambda):
           self.check_consistent(env[id], value_ty, value)
         else:
           env[id] = t
-      case Expr(Call(Name('print'), [arg])):
-        arg_ty = self.type_check_exp(arg, env)
-        self.check_type_equal(arg_ty, IntType(), arg)
-      case Expr(value):
-        value_ty = self.type_check_exp(value, env)
-      case If(test, body, orelse):
-        test_ty = self.type_check_exp(test, env)
-        self.check_consistent(BoolType(), test_ty, test)
-        body_ty = self.type_check_stmts(body, env)
-        orelse_ty = self.type_check_stmts(orelse, env)
-        self.check_consistent(body_ty, orelse_ty, ss[0])
-      case FunctionDef(name, params, body, dl, returns, comment):
-        new_env = {x: t for (x,t) in env.items()}
-        for (x,t) in params:
-            new_env[x] = t
-        self.type_check_stmts(body, new_env, returns)
-      case Return(value):
-        self.check_exp(value, return_type, env)
+      ...
       case _:
         raise Exception('type_check_stmts: unexpected ' + repr(ss))
 
@@ -19240,7 +19190,7 @@ class TypeCheckLgrad(TypeCheckLlambda):
       self.type_check_stmt(s, env, return_type)
 \end{lstlisting}
 \end{tcolorbox}
-\caption{Type checker for the \LangGrad{} language, part 3.}
+\caption{Type checking statements in the \LangGrad{} language.}
 \label{fig:type-check-Lgradual-3}
 \end{figure}
 
@@ -19537,37 +19487,37 @@ operator, that is, by checking the value's tag and either retrieving
 the underlying integer or signaling an error if it the tag is not the
 one for integers (Figure~\ref{fig:interp-Lany-aux}).
 %
-Things get more interesting casts involving function or tuple types,
-that is, casts involving higher-order types.
+Things get more interesting casts involving function, tuple, or array
+types, that is, casts involving higher-order types.
 
 Consider the cast of the function \code{maybe\_inc} from
 \racket{\code{(Any -> Any)}}\python{\code{Callable[[Any], Any]}}
 to
-\racket{\code{(Integer -> Integer)}}\python{\code{Callable[[int], int]}}.
-When a function flows through
-this cast at runtime, we can't know in general whether the function
-will always return an integer. After all, predicting the return value of
-a function is equivalent to the halting problem, which is
-undecidable.  The \LangCast{} interpreter therefore delays the checking
+\racket{\code{(Integer -> Integer)}}\python{\code{Callable[[int], int]}}
+in Figure~\ref{fig:map-maybe_inc}.
+When the \code{maybe\_inc} function flows through
+this cast at runtime, we don't know whether it will return
+an integer, as that depends on the input from the user.
+The \LangCast{} interpreter therefore delays the checking
 of the cast until the function is applied. This is accomplished by
 wrapping \code{maybe\_inc} in a new function that casts its parameter
 from \INTTY{} to \CANYTY{}, applies \code{maybe\_inc}, and then
-casts the return value from \CANYTY{} to \code{Integer}.
+casts the return value from \CANYTY{} to \INTTY{}.
 
 
 {\if\edition\pythonEd
 %
-Casts that involve mutable data require special care. So to
-demonstrate these issues, we use the \code{list} type introduced in
+There are further complicatons regarding casts on mutable data
+such as the \code{list} type introduced in
 the challenge assignment of Section~\ref{sec:arrays}.
 %
 \fi}
 %
-Turning our attention to casts involving \racket{tuple}\python{list}
-types, we consider the example in Figure~\ref{fig:map-bang} that
+Consider the example in Figure~\ref{fig:map-bang} that
 defines a partially-typed version of \code{map} whose parameter
-\code{v} has type \racket{\code{(Vector Any
-    Any)}}\python{\code{list[Any]}} and that updates \code{v} in place
+\code{v} has type
+\racket{\code{(Vector Any Any)}}\python{\code{list[Any]}}
+and that updates \code{v} in place
 instead of returning a new tuple. So we name this function
 \code{map\_inplace}. We apply \code{map\_inplace} to a
 \racket{tuple}\python{list} of integers, so the type checker inserts a
@@ -19636,9 +19586,9 @@ cast to the resulting value.  On a write, the proxy casts the argument
 value and then performs the write to the underlying tuple.
 \racket{
 For the first \code{(vector-ref v 0)} in \code{map\_inplace}, the proxy casts
-\code{0} from \code{Integer} to \CANYTY{}.
+\code{0} from \INTTY{} to \CANYTY{}.
 For the first \code{vector-set!}, the proxy casts a tagged \code{1}
-from \CANYTY{} to \code{Integer}.
+from \CANYTY{} to \INTTY{}.
 }
 \python{
   For the subscript \code{v[i]} in \code{f([v[i])} of \code{map\_inplace},

defs.tex

@@ -275,6 +275,7 @@
 \newcommand{\CSUB}[2]{\LP\key{-}~#1~#2\RP}
 \newcommand{\CWHILE}[2]{\LP\key{while}~#1~#2\RP}
 \newcommand{\WHILE}[2]{\LP\key{WhileLoop}~#1~#2\RP}
+\newcommand{\MAKEVEC}[2]{\LP\key{make-vector}~#1~#2\RP}
 \newcommand{\CMAKEVEC}[2]{\LP\key{make-vector}~#1~#2\RP}
 \newcommand{\CSETBANG}[2]{\LP\key{set!}~#1~#2\RP}
 \newcommand{\SETBANG}[2]{\LP\key{SetBang}~#1~#2\RP}