merged upstream

book.tex

@@ -8343,7 +8343,7 @@ then there is no need to generate a new label and entry in
   and 3) \code{els}, the code generated by
   explicate for the ``else'' branch.  The \code{explicate\_pred}
   function should match on \code{cnd} with a case for
-  every kind of expression that can have type \code{Boolean}.}
+  every kind of expression that can have type \BOOLTY{}.}
 %
 \python{The \code{explicate\_pred} function has four parameters: 1)
   the condition expression, 2) the generated statements for the
@@ -9985,7 +9985,7 @@ Figure~\ref{fig:type-check-Lwhile}.
 %
 The type checking of the \code{SetBang} expression requires the type
 of the variable and the right-hand-side to agree. The result type is
-\code{Void}. For \code{while}, the condition must be a \code{Boolean}
+\code{Void}. For \code{while}, the condition must be a \BOOLTY{}
 and the result type is \code{Void}.  For \code{Begin}, the result type
 is the type of its last subexpression.
 %
@@ -13256,8 +13256,7 @@ nested inside each other.
         &\MID& \key{FunctionType}\LP \Type^{*} \key{, } \Type \RP \\
     \Exp &::=& \CALL{\Exp}{\Exp^{*}}\\
     \Stmt &::=& \RETURN{\Exp} \\
-   \Params &::=&                  \LP\Var\key{,}\Type\RP^*
-    \\
+   \Params &::=&  \LP\Var\key{,}\Type\RP^* \\
    \Def &::=& \FUNDEF{\Var}{\Params}{\Type}{}{\Stmt^{+}} 
   \end{array}
 }
@@ -16736,7 +16735,7 @@ class Tagged(Value):
 \end{minipage}
 \fi}
 %
-\racket{The tags are \code{Integer}, \code{Boolean}, \code{Void},
+\racket{The tags are \code{Integer}, \BOOLTY{}, \code{Void},
   \code{Vector}, and \code{Procedure}.}
 %
 \python{The tags are \code{'int'}, \code{'bool'}, \code{'none'},
@@ -17604,7 +17603,7 @@ $\Rightarrow$
 &
 \begin{minipage}{0.65\textwidth}
 \begin{lstlisting}
-(any-vector-ref |$e_1'$| |$e_2'$|)
+(any-vector-ref |$e_1'$| (project |$e'_2$| Integer))
 \end{lstlisting}
 \end{minipage}
 \\[2ex]\hline
@@ -17686,7 +17685,7 @@ Inject(Project(|$e'_1$|, IntType())
 \\[2ex]\hline
 \begin{minipage}{0.23\textwidth}
 \begin{lstlisting}
-lambda |$x_1 \ldots x_n$|: |$e$|
+lambda |$x_1 \ldots$|: |$e$|
 \end{lstlisting}
 \end{minipage}
 &
@@ -17694,7 +17693,7 @@ $\Rightarrow$
 &
 \begin{minipage}{0.7\textwidth}
 \begin{lstlisting}
-Inject(Lambda([(|$x_1$|,AnyType),|$\ldots$|,(|$x_n$|,AnyType)], |$e'$|)
+Inject(Lambda([(|$x_1$|,AnyType),|$\ldots$|], |$e'$|)
        FunctionType([AnyType(),|$\ldots$|], AnyType()))
 \end{lstlisting}
 \end{minipage}
@@ -17724,7 +17723,8 @@ $\Rightarrow$
 &
 \begin{minipage}{0.7\textwidth}
 \begin{lstlisting}
-Call(Name('any_tuple_load'),[|$e_1'$|, |$e_2'$|])
+Call(Name('any_tuple_load'),
+     [|$e_1'$|, Project(|$e_2'$|, IntType())])
 \end{lstlisting}
 \end{minipage}
 %% \begin{minipage}{0.23\textwidth}
@@ -18411,14 +18411,6 @@ for the compilation of \LangDyn{}.
 \label{ch:Lgrad}
 \index{subject}{gradual typing}
 
-\if\edition\pythonEd
-
-UNDER CONSTRUCTION
-
-\fi
-
-\if\edition\racketEd
-
 This chapter studies a language, \LangGrad{}, in which the programmer
 can choose between static and dynamic type checking in different parts
 of a program, thereby mixing the statically typed \LangLam{} language
@@ -18432,41 +18424,73 @@ adding or removing type annotations on parameters and
 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 \itm{param} and \itm{ret}
-non-terminals that make type annotations optional. The return types
-are not optional in the abstract syntax; the parser fills in
-\code{Any} when the return type is not specified in the concrete
-syntax.
+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.
 
 \newcommand{\LgradGrammarRacket}{
 \begin{array}{lcl}
   \Type &::=& (\Type \ldots \; \key{->}\; \Type) \\
-  \itm{param} &::=& \Var \MID \LS\Var \key{:} \Type\RS \\
+  \Param &::=& \Var \MID \LS\Var \key{:} \Type\RS \\
   \itm{ret} &::=& \epsilon \MID \key{:} \Type \\
   \Exp &::=& \LP\Exp \; \Exp \ldots\RP 
-      \MID \CGLAMBDA{\LP\itm{param}\ldots\RP}{\itm{ret}}{\Exp} \\
+      \MID \CGLAMBDA{\LP\Param\ldots\RP}{\itm{ret}}{\Exp} \\
     &\MID& \LP \key{procedure-arity}~\Exp\RP \\
-  \Def &::=& \CGDEF{\Var}{\itm{param}\ldots}{\itm{ret}}{\Exp} 
+  \Def &::=& \CGDEF{\Var}{\Param\ldots}{\itm{ret}}{\Exp} 
 \end{array}
 }
 
 \newcommand{\LgradASTRacket}{
 \begin{array}{lcl}
   \Type &::=& (\Type \ldots \; \key{->}\; \Type) \\
-  \itm{param} &::=& \Var \MID \LS\Var \key{:} \Type\RS \\
+  \Param &::=& \Var \MID \LS\Var \key{:} \Type\RS \\
   \Exp &::=& \APPLY{\Exp}{\Exp\ldots}
-  \MID \LAMBDA{\LP\itm{param}\ldots\RP}{\Type}{\Exp} \\
+  \MID \LAMBDA{\LP\Param\ldots\RP}{\Type}{\Exp} \\
   \itm{op} &::=& \code{procedure-arity} \\
- \Def &::=& \FUNDEF{\Var}{\LP\itm{param}\ldots\RP}{\Type}{\code{'()}}{\Exp} 
+ \Def &::=& \FUNDEF{\Var}{\LP\Param\ldots\RP}{\Type}{\code{'()}}{\Exp} 
+\end{array}
+}
+
+\newcommand{\LgradGrammarPython}{
+\begin{array}{lcl}
+  \Type &::=& \key{Any}
+                \MID \key{int}
+                \MID \key{bool}
+                \MID \key{tuple}\LS \Type \code{, } \ldots  \RS
+                \MID \key{Callable}\LS \LS \Type \key{,} \ldots \RS \key{, } \Type \RS \\
+  \Exp &::=& \CAPPLY{\Exp}{\Exp\code{,} \ldots} 
+      \MID \CLAMBDA{\Var\code{, }\ldots}{\Exp}
+      \MID \CARITY{\Exp} \\
+  \Stmt &::=& \CANNASSIGN{\Var}{\Type}{\Exp} \MID \CRETURN{\Exp} \\ 
+  \Param &::=& \Var \MID \Var \key{:} \Type \\
+  \itm{ret} &::=& \epsilon \MID \key{->}~\Type \\
+  \Def &::=& \CGDEF{\Var}{\Param\key{, }\ldots}{\itm{ret}}{\Stmt^{+}} 
 \end{array}
 }
 
+\newcommand{\LgradASTPython}{
+  \begin{array}{lcl}
+  \Type &::=& \key{AnyType()} \MID \key{IntType()} \MID \key{BoolType()} \MID \key{VoidType()}\\
+        &\MID& \key{TupleType}\LP\Type^{*}\RP
+        \MID \key{FunctionType}\LP \Type^{*} \key{, } \Type \RP \\
+  \Exp &::=& \CALL{\Exp}{\Exp^{*}} \MID \LAMBDA{\Var^{*}}{\Exp}\\
+        &\MID& \ARITY{\Exp} \\
+  \Stmt &::=& \ANNASSIGN{\Var}{\Type}{\Exp}
+       \MID \RETURN{\Exp} \\
+   \Param &::=& \LP\Var\key{,}\Type\RP \\
+   \Def &::=& \FUNDEF{\Var}{\Param^{*}}{\Type}{}{\Stmt^{+}} 
+  \end{array}
+}  
+  
 \begin{figure}[tp]
 \centering
 \begin{tcolorbox}[colback=white]
     \small
+{\if\edition\racketEd    
 \[
 \begin{array}{l}
   \gray{\LintGrammarRacket{}} \\ \hline
@@ -18480,6 +18504,22 @@ syntax.
 \end{array}
 \end{array}
 \]
+\fi}
+{\if\edition\pythonEd
+\[
+\begin{array}{l}
+  \gray{\LintGrammarPython{}} \\ \hline
+  \gray{\LvarGrammarPython{}} \\ \hline
+  \gray{\LifGrammarPython{}} \\ \hline
+  \gray{\LwhileGrammarPython} \\ \hline
+  \gray{\LtupGrammarPython} \\   \hline
+  \LgradGrammarPython \\
+  \begin{array}{lcl}
+    \LangGradM{} &::=& \Def\ldots \Stmt\ldots
+  \end{array}
+\end{array}
+\]
+\fi}
 \end{tcolorbox}
 
 \caption{The concrete syntax of \LangGrad{}, extending \LangVec{} (Figure~\ref{fig:Lvec-concrete-syntax}).}
@@ -18490,6 +18530,7 @@ syntax.
 \centering
 \begin{tcolorbox}[colback=white]
     \small
+{\if\edition\racketEd
 \[
 \begin{array}{l}
   \gray{\LintOpAST} \\ \hline
@@ -18503,6 +18544,22 @@ syntax.
 \end{array}
 \end{array}
 \]
+\fi}
+{\if\edition\pythonEd
+\[
+\begin{array}{l}
+  \gray{\LintASTPython{}} \\ \hline
+  \gray{\LvarASTPython{}} \\ \hline
+  \gray{\LifASTPython{}} \\ \hline
+  \gray{\LwhileASTPython} \\ \hline
+  \gray{\LtupASTPython} \\   \hline
+  \LgradASTPython \\
+  \begin{array}{lcl}
+    \LangGradM{} &::=& \PROGRAM{}{\LS \Def \ldots \Stmt \ldots \RS}
+  \end{array}
+\end{array}
+\]
+\fi}
 \end{tcolorbox}
 
 \caption{The abstract syntax of \LangGrad{}, extending \LangVec{} (Figure~\ref{fig:Lvec-syntax}).}
@@ -18521,6 +18578,7 @@ function.
 \begin{figure}[btp]
 % gradual_test_9.rkt
   \begin{tcolorbox}[colback=white]
+{\if\edition\racketEd
     \begin{lstlisting}
 (define (map [f : (Integer -> Integer)]
                    [v : (Vector Integer Integer)])
@@ -18530,14 +18588,27 @@ function.
 (define (inc x) (+ x 1))
 
 (vector-ref (map inc (vector 0 41)) 1)
+    \end{lstlisting}
+    \fi}
+{\if\edition\pythonEd
+\begin{lstlisting}
+def map(f : Callable[[int], int], v : tuple[int,int]) -> tuple[int,int]:
+    return f(v[0]), f(v[1])
+
+def inc(x):
+    return x + 1
+
+t = map(inc, (0, 41))
+print(t[1])
 \end{lstlisting}
+  \fi}
   \end{tcolorbox}
 
   \caption{A partially-typed version of the \code{map} example.}
 \label{fig:gradual-map}
 \end{figure}
 
-\section{Type Checking \LangGrad{} and \LangCast{}}
+\section{Type Checking \LangGrad{}}
 \label{sec:gradual-type-check}
 
 The type checker for \LangGrad{} uses the \code{Any} type for missing
@@ -18550,10 +18621,19 @@ 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 \code{consistent?} predicate.
+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]
+{\if\edition\racketEd    
 \begin{lstlisting}
 (define/public (consistent? t1 t2)
   (match* (t1 t2)
@@ -18569,40 +18649,45 @@ Figure~\ref{fig:consistent} defines the \code{consistent?} predicate.
           (consistent? rt1 rt2))]
     [(other wise) #f]))
 \end{lstlisting}
+\fi}
+{\if\edition\pythonEd
+\begin{lstlisting}
+  def consistent(self, t1, t2):
+      match (t1, t2):
+        case (AnyType(), _):
+          return True
+        case (_, AnyType()):
+          return True
+        case (FunctionType(ps1, rt1), FunctionType(ps2, rt2)):
+          return all([self.consistent(p1, p2) for (p1,p2) in zip(ps1,ps2)]) \
+              and consistent(rt1, rt2)
+        case (TupleType(ts1), TupleType(ts2)):
+          return all([self.consistent(ty1, ty2) for (ty1,ty2) in zip(ts1,ts2)])
+        case (_, _):
+          return t1 == t2
+\end{lstlisting}  
+  \fi}
   \end{tcolorbox}
 
-  \caption{The consistency predicate on types.}
+  \caption{The consistency method on types.}
 \label{fig:consistent}
 \end{figure}
 
-Returning to the \code{map} example of
-Figure~\ref{fig:gradual-map}, the \code{inc} function has type
-\code{(Any -> Any)} but parameter \code{f} of \code{map} has type
-\code{(Integer -> Integer)}.  The type checker for \LangGrad{} allows this
-because the two types are consistent.  In particular, \code{->} is
-equal to \code{->} and because \code{Any} is consistent with
-\code{Integer}.
 
 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
+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,
-\code{(Any -> Any)} is consistent with \code{(Integer ->
-  Integer)}. One might say that a gradual type checker is optimistic
+\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.
 %
-Unfortunately, running this program with input \code{1} triggers an
-error when the \code{maybe-inc} function returns \code{\#t}.  The
-\LangGrad{} language performs checking at runtime to ensure the
-integrity of the static types, such as the \code{(Integer -> Integer)}
-annotation on parameter \code{f} of \code{map}.  This runtime checking
-is carried out by a new \code{Cast} form that is inserted by the type
-checker.  Thus, the output of the type checker is a program in the
-\LangCast{} language, which adds \code{Cast} and \ANYTY{} to
-\LangLam{}.
-%, as shown in Figure~\ref{fig:Lgrad-prime-syntax}.
+The type checker for \LangGrad{} is defined in
+Figures~\ref{fig:type-check-Lgradual-1}, \ref{fig:type-check-Lgradual-2},
+and \ref{fig:type-check-Lgradual-3}.
 
 %% \begin{figure}[tp]
 %% \centering
@@ -18624,6 +18709,7 @@ checker.  Thus, the output of the type checker is a program in the
 
 \begin{figure}[tbp]
 \begin{tcolorbox}[colback=white]  
+{\if\edition\racketEd    
 \begin{lstlisting}
 (define (map [f : (Integer -> Integer)]
                    [v : (Vector Integer Integer)])
@@ -18631,26 +18717,61 @@ checker.  Thus, the output of the type checker is a program in the
   (vector (f (vector-ref v 0)) (f (vector-ref v 1))))
 (define (inc x) (+ x 1))
 (define (true) #t)
-(define (maybe-inc x) (if (eq? 0 (read)) (inc x) (true)))
+(define (maybe_inc x) (if (eq? 0 (read)) (inc x) (true)))
+
+(vector-ref (map maybe_inc (vector 0 41)) 0)
+\end{lstlisting}
+\fi}
+{\if\edition\pythonEd    
+\begin{lstlisting}
+def map(f : Callable[[int], int], v : tuple[int,int]) -> tuple[int,int]:
+    return f(v[0]), f(v[1])
+
+def inc(x):
+    return x + 1
+def true():
+    return True
+def maybe_inc(x):
+    return inc(x) if input_int() == 0 else true()
 
-(vector-ref (map maybe-inc (vector 0 41)) 0)
+t = map(maybe_inc, (0, 41))
+print( t[1] )
 \end{lstlisting}
+\fi}
 \end{tcolorbox}
 
 \caption{A variant of the \code{map} example with an error.}
-\label{fig:map-maybe-inc}
+\label{fig:map-maybe_inc}
 \end{figure}
 
-Figure~\ref{fig:map-cast} shows the output of the type checker for
-\code{map} and \code{maybe-inc}.  The idea is that \code{Cast} is
+Running this program with input \code{1} triggers an
+error when the \code{maybe\_inc} function returns
+\racket{\code{\#t}}\python{\code{True}}.  The \LangGrad{} language
+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{}.
+%
+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 \code{Integer} and the result of the \code{+} is cast to
-\code{Any}.  In the call to \code{map}, the \code{inc} argument
-is cast from \code{(Any -> Any)} to \code{(Integer -> Integer)}.
+cast to \INTTY{} and the result of the \code{+} is cast to
+\ANYTY{}.  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]}}.
 
 \begin{figure}[btp]
-\begin{tcolorbox}[colback=white]  
+  \begin{tcolorbox}[colback=white]
+{\if\edition\racketEd        
 \begin{lstlisting}[basicstyle=\ttfamily\footnotesize]
 (define (map [f : (Integer -> Integer)] [v : (Vector Integer Integer)])
                    : (Vector Integer Integer)
@@ -18658,25 +18779,256 @@ is cast from \code{(Any -> Any)} to \code{(Integer -> Integer)}.
 (define (inc [x : Any]) : Any
   (cast (+ (cast x Any Integer) 1) Integer Any))
 (define (true) : Any (cast #t Boolean Any))
-(define (maybe-inc [x : Any]) : Any
+(define (maybe_inc [x : Any]) : Any
   (if (eq? 0 (read)) (inc x) (true)))
 
-(vector-ref (map (cast maybe-inc (Any -> Any) (Integer -> Integer))
+(vector-ref (map (cast maybe_inc (Any -> Any) (Integer -> Integer))
                        (vector 0 41)) 0)
 \end{lstlisting}
+\fi}
+{\if\edition\pythonEd        
+\begin{lstlisting}[basicstyle=\ttfamily\footnotesize]
+def map(f : Callable[[int], int], v : tuple[int,int]) -> tuple[int,int]:
+    return f(v[0]), f(v[1])
+
+def inc(x : Any) -> Any:
+    return Cast(Cast(x, Any, int) + 1, int, Any)
+def true() -> Any:
+    return Cast(True, bool, Any)
+def maybe_inc(x : Any) -> Any:
+    return inc(x) if input_int() == 0 else true()
+
+t = map(Cast(maybe_inc, Callable[[Any], Any], Callable[[int], int]),
+        (0, 41))
+print(t[1])
+\end{lstlisting}
+\fi}
 \end{tcolorbox}
 
-\caption{Output of type checking \code{map}
-  and \code{maybe-inc}.}
+\caption{Output of the \code{cast\_insert} pass for the \code{map}
+  and \code{maybe\_inc} example.}
 \label{fig:map-cast}
 \end{figure}
 
 
-The type checker for \LangGrad{} is defined in
-Figures~\ref{fig:type-check-Lgradual-1}, \ref{fig:type-check-Lgradual-2},
-and \ref{fig:type-check-Lgradual-3}.
+{\if\edition\pythonEd        
+\begin{figure}[tbp]
+\begin{tcolorbox}[colback=white]  
+\begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
+class TypeCheckLgrad(TypeCheckLlambda):
+  def type_check_exp(self, e, env):
+    match e:
+      case Name(id):
+        return env[id]
+      case Constant(value) if value is True or value is False:
+        return BoolType()
+      case Constant(value) if isinstance(value, int):
+        return IntType()
+      case Call(Name('input_int'), []):
+        return IntType()
+      case BinOp(left, op, right) if op == Add() or op == Sub():
+        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)
+        body_t = self.type_check_exp(body, env)
+        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])
+        match func_t:
+          case FunctionType(params_t, return_t):
+            for (arg_t, param_t) in zip(args_t, params_t):
+                self.check_consistent(param_t, arg_t, e)
+            return return_t
+          case AnyType():
+            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.}
+\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):
+    match e:
+      case Lambda(params, body):
+        match 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
+          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))
+      case _:
+        e_ty = self.type_check_exp(e, env)
+        self.check_consistent(e_ty, ty, e)
+\end{lstlisting}
+\end{tcolorbox}
+\caption{Type checker for the \LangGrad{} language, part 2.}
+\label{fig:type-check-Lgradual-2}
+\end{figure}
+
+\begin{figure}[tbp]
+\begin{tcolorbox}[colback=white]
+\begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
+  def type_check_stmt(self, s, env, return_type):
+    match s:
+      case Assign([Name(id)], value):
+        value_ty = self.type_check_exp(value, env)
+        if id in env:
+          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))
+
+  def type_check_stmts(self, ss, env, return_type):
+    for s in ss:
+      self.type_check_stmt(s, env, return_type)
+\end{lstlisting}
+\end{tcolorbox}
+\caption{Type checker for the \LangGrad{} language, part 3.}
+\label{fig:type-check-Lgradual-3}
+\end{figure}
+
+\begin{figure}[tbp]
+\begin{tcolorbox}[colback=white]  
+\begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
+  def join_types(self, t1, t2):
+      match (t1, t2):
+        case (AnyType(), _):
+          return t2
+        case (_, AnyType()):
+          return t1
+        case (FunctionType(ps1, rt1), FunctionType(ps2, rt2)):
+          return FunctionType([self.join_types(p1, p2) for (p1,p2) in zip(ps1, ps2)],
+                              self.join_types(rt1,rt2))
+        case (TupleType(ts1), TupleType(ts2)):
+          return TupleType([self.join_types(ty1, ty2) for (ty1,ty2) in zip(ts1,ts2)])
+        case (_, _):
+          return t1
+        
+  def check_consistent(self, t1, t2, e):
+    if not self.consistent(t1, t2):
+      raise Exception('error: ' + repr(t1) + ' inconsistent with ' + repr(t2) \
+                      + ' in ' + repr(e))
+
+\end{lstlisting}
+\end{tcolorbox}
+
+\caption{Auxiliary methods for type checking \LangGrad{}.}
+\label{fig:type-check-Lgradual-aux}
+\end{figure}
+
+\fi}
+
+
+{\if\edition\racketEd        
 \begin{figure}[tbp]
 \begin{tcolorbox}[colback=white]  
 \begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
@@ -18739,7 +19091,6 @@ and \ref{fig:type-check-Lgradual-3}.
 	     [else (error 'type-check "expected vector not ~a\nin ~v" t1 e)])]
 \end{lstlisting}
 \end{tcolorbox}
-
 \caption{Type checker for the \LangGrad{} language, part 1.}
 \label{fig:type-check-Lgradual-1}
 \end{figure}
@@ -18808,14 +19159,12 @@ and \ref{fig:type-check-Lgradual-3}.
            (values (WhileLoop (make-cast e1^ T1 'Boolean) e2^) 'Void)]
 \end{lstlisting}
 \end{tcolorbox}
-
 \caption{Type checker for the \LangGrad{} language, part 2.}
 \label{fig:type-check-Lgradual-2}
 \end{figure}
 
-
 \begin{figure}[tbp]
-\begin{tcolorbox}[colback=white]  
+\begin{tcolorbox}[colback=white]
 \begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
 	  [(Apply e1 e2s)
 	   (define-values (e1^ T1) (recur e1))
@@ -18848,12 +19197,10 @@ and \ref{fig:type-check-Lgradual-3}.
           )))
 \end{lstlisting}
 \end{tcolorbox}
-
 \caption{Type checker for the \LangGrad{} language, part 3.}
 \label{fig:type-check-Lgradual-3}
 \end{figure}
 
-
 \begin{figure}[tbp]
 \begin{tcolorbox}[colback=white]  
 \begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
@@ -18925,35 +19272,41 @@ and \ref{fig:type-check-Lgradual-3}.
 \label{fig:type-check-Lgradual-aux}
 \end{figure}
 
+\fi}
+
 \clearpage
 
 \section{Interpreting \LangCast{}}
 \label{sec:interp-casts}
 
-The runtime behavior of first-order casts is straightforward, that is,
-casts involving simple types such as \code{Integer} and
-\code{Boolean}.  For example, a cast from \code{Integer} to \code{Any}
-can be accomplished with the \code{Inject} operator of \LangAny{}, which
-puts the integer into a tagged value
-(Figure~\ref{fig:interp-Lany}). Similarly, a cast from \code{Any} to
-\code{Integer} is accomplished with the \code{Project} 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 for higher-order casts, that is, casts
-involving function or tuple types.
-
-Consider the cast of the function \code{maybe-inc} from \code{(Any ->
-  Any)} to \code{(Integer -> Integer)}. When a function flows through
+The runtime behavior of casts involving simple types such as
+\INTTY{} and \BOOLTY{} is straightforward.  For example, a
+cast from \INTTY{} to \CANYTY{} can be accomplished with the
+\code{Inject} operator of \LangAny{}, which puts the integer into a
+tagged value (Figure~\ref{fig:interp-Lany}). Similarly, a cast from
+\CANYTY{} to \INTTY{} is accomplished with the \code{Project}
+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.
+
+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.\footnote{Predicting the return value of
-  a function is equivalent to the halting problem, which is
-  undecidable.}  The \LangCast{} interpreter therefore delays the checking
+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
 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 \code{Integer} to \code{Any}, applies \code{maybe-inc}, and then
-casts the return value from \code{Any} to \code{Integer}.
+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}.
+
+UNDER CONSTRUCTION
 
 Turning our attention to casts involving tuple types, we consider the
 example in Figure~\ref{fig:map-bang} that defines a
@@ -18998,21 +19351,21 @@ read, the proxy reads from the underlying tuple and then applies a
 cast to the resulting value.  On a write, the proxy casts the argument
 value and then performs the write to the underlying tuple. For the
 first \code{(vector-ref v 0)} in \code{map!}, the proxy casts
-\code{0} from \code{Integer} to \code{Any}.  For the first
-\code{vector-set!}, the proxy casts a tagged \code{1} from \code{Any}
+\code{0} from \code{Integer} to \CANYTY{}.  For the first
+\code{vector-set!}, the proxy casts a tagged \code{1} from \CANYTY{}
 to \code{Integer}.
 
 The final category of cast that we need to consider are casts between
-the \code{Any} type and either a function or a tuple
+the \CANYTY{} type and either a function or a tuple
 type. Figure~\ref{fig:map-any} shows a variant of \code{map!}
 in which parameter \code{v} does not have a type annotation, so it is
-given type \code{Any}. In the call to \code{map!}, the tuple has
+given type \CANYTY{}. In the call to \code{map!}, the tuple has
 type \code{(Vector Integer Integer)} so the type checker inserts a
-cast from \code{(Vector Integer Integer)} to \code{Any}. A first
+cast from \code{(Vector Integer Integer)} to \CANYTY{}. A first
 thought is to use \code{Inject}, but that doesn't work because
 \code{(Vector Integer Integer)} is not a flat type. Instead, we must
 first cast to \code{(Vector Any Any)} (which is flat) and then inject
-to \code{Any}.
+to \CANYTY{}.
 
 \begin{figure}[tbp]
   \begin{tcolorbox}[colback=white]
@@ -19029,7 +19382,7 @@ to \code{Any}.
 \end{lstlisting}
   \end{tcolorbox}
 
-  \caption{Casting a tuple to \code{Any}.}
+  \caption{Casting a tuple to \CANYTY{}.}
 \label{fig:map-any}
 \end{figure}
 
@@ -19205,7 +19558,7 @@ named \code{raw-vector} instead of \code{vector} to create these
 tuples of functions. Figure~\ref{fig:map-bang-lower-cast} shows
 the output of \code{lower-casts} on the example in
 Figure~\ref{fig:map-bang} that involved casting a tuple of
-integers to a tuple of \code{Any}.
+integers to a tuple of \CANYTY{}.
 
 \begin{figure}[tbp]
 \begin{tcolorbox}[colback=white]  
@@ -19316,7 +19669,7 @@ Next we describe each of the new primitive operations.
 %
   This operation brands a vector proxy as value of the \code{PVector} type.
 \item[\code{proxy?} : (\key{PVector} $T \ldots$) $\to$
-  \code{Boolean}] \ \\
+  \BOOLTY{}] \ \\
 %
   This returns true if the value is a tuple proxy and false if it is a
   real tuple.
@@ -19327,7 +19680,7 @@ Next we describe each of the new primitive operations.
   tuple.
   
 \item[\code{proxy-vector-length} : (\key{PVector} $T \ldots$)
-  $\to$ \code{Boolean}]\ \\
+  $\to$ \BOOLTY{}]\ \\
 %
   Given a tuple proxy, this operation returns the length of the tuple.
   
@@ -19479,9 +19832,9 @@ movq %rax, |$\itm{lhs'}$|
 \end{lstlisting}
 
 We have another batch of tuple operations to deal with, those for the
-\code{Any} type. Recall that the type checker for \LangGrad{}
+\CANYTY{} type. Recall that the type checker for \LangGrad{}
 generates an \code{any-vector-ref} when there is a \code{vector-ref}
-on something of type \code{Any}, and similarly for
+on something of type \CANYTY{}, and similarly for
 \code{any-vector-set!}  and \code{any-vector-length}
 (Figure~\ref{fig:type-check-Lgradual-1}). In
 Section~\ref{sec:select-Lany} we selected instructions for these
@@ -19508,7 +19861,7 @@ be translated in a similar way.
   new programs, also test your compiler on all the tests for \LangLam{}
   and tests for \LangDyn{}. Sometimes you may get a type checking error
   on the \LangDyn{} programs but you can adapt them by inserting
-  a cast to the \code{Any} type around each subexpression
+  a cast to the \CANYTY{} type around each subexpression
   causing a type error. While \LangDyn{} does not have explicit casts,
   you can induce one by wrapping the subexpression \code{e}
   with a call to an un-annotated identity function, like this:
@@ -19637,8 +19990,6 @@ recommend the reader to the online gradual typing bibliography:
 %   type analysis and type specialization?
 %   coercions?
 
-\fi
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \chapter{Parametric Polymorphism}
 \label{ch:Lpoly}
@@ -19695,9 +20046,9 @@ Figure~\ref{fig:Lpoly-concrete-syntax} defines the concrete syntax of
 \LangPoly{} and Figure~\ref{fig:Lpoly-syntax} defines the abstract
 syntax. We add a second form for function definitions in which a type
 declaration comes before the \code{define}. In the abstract syntax,
-the return type in the \code{Def} is \code{Any}, but that should be
+the return type in the \code{Def} is \CANYTY{}, but that should be
 ignored in favor of the return type in the type declaration.  (The
-\code{Any} comes from using the same parser as in
+\CANYTY{} comes from using the same parser as in
 Chapter~\ref{ch:Ldyn}.)  The presence of a type declaration
 enables the use of an \code{All} type for a function, thereby making
 it polymorphic. The grammar for types is extended to include
@@ -20090,12 +20441,12 @@ polymorphism, which we describe below.
   
 \item[Uniform representation] generates one version of each
   polymorphic function but requires all values to have a common
-  ``boxed'' format, such as the tagged values of type \code{Any} in
+  ``boxed'' format, such as the tagged values of type \CANYTY{} in
   \LangAny{}. Both polymorphic and non-polymorphic (i.e. monomorphic)
   code is compiled similarly to code in a dynamically typed language
   (like \LangDyn{}), in which primitive operators require their
-  arguments to be projected from \code{Any} and their results are
-  injected into \code{Any}.  (In object-oriented languages, the
+  arguments to be projected from \CANYTY{} and their results are
+  injected into \CANYTY{}.  (In object-oriented languages, the
   projection is accomplished via virtual method dispatch.) The uniform
   representation approach is compatible with separate compilation and
   with first-class polymorphism.  However, it produces the
@@ -20140,11 +20491,11 @@ add just one new pass, \code{erase-types}, to compile \LangInst{} to
 \section{Erase Types}
 \label{sec:erase-types}
 
-We use the \code{Any} type from Chapter~\ref{ch:Ldyn} to
+We use the \CANYTY{} type from Chapter~\ref{ch:Ldyn} to
 represent type variables. For example, Figure~\ref{fig:map-erase}
 shows the output of the \code{erase-types} pass on the polymorphic
 \code{map} (Figure~\ref{fig:map-poly}). The occurrences of
-type parameter \code{a} are replaced by \code{Any} and the polymorphic
+type parameter \code{a} are replaced by \CANYTY{} and the polymorphic
 \code{All} types are removed from the type of \code{map}. 
 
 \begin{figure}[tbp]
@@ -20192,13 +20543,13 @@ instantiated type. The source and target type of a cast must be
 consistent (Figure~\ref{fig:consistent}), which indeed is the case
 because both the source and target are obtained from the same
 polymorphic type of \code{map}, replacing the type parameters with
-\code{Any} in the former and with the deduced type arguments in the
-later. (Recall that the \code{Any} type is consistent with any type.)
+\CANYTY{} in the former and with the deduced type arguments in the
+later. (Recall that the \CANYTY{} type is consistent with any type.)
 
 To implement the \code{erase-types} pass, we recommend defining a
 recursive auxiliary function named \code{erase-type} that applies the
 following two transformations. It replaces type variables with
-\code{Any}
+\CANYTY{}
 \begin{lstlisting}
 |$x$|
 |$\Rightarrow$|

defs.tex

@@ -101,6 +101,7 @@
 \newcommand{\Instr}{\itm{instr}}
 \newcommand{\Block}{\itm{block}}
 \newcommand{\Blocks}{\itm{blocks}}
+\newcommand{\Param}{\itm{prm}}
 \newcommand{\Params}{\itm{params}}
 \newcommand{\Tail}{\itm{tail}}
 \newcommand{\Prog}{\itm{prog}}
@@ -155,6 +156,7 @@
 \newcommand{\BOOLTY}{{\key{Boolean}}}
 \newcommand{\VECTY}[1]{{\LP\key{Vector}~#1\RP}}
 \newcommand{\ANYTY}{{\key{Any}}}
+\newcommand{\CANYTY}{{\key{Any}}}
 \newcommand{\CPROGRAM}[2]{\LP\code{CProgram}~#1~#2\RP}
 \newcommand{\CPROGRAMDEFS}[2]{\LP\code{CProgramDefs}~#1~#2\RP}
 \newcommand{\LET}[3]{\key{(Let}~#1~#2~#3\key{)}}
@@ -218,6 +220,7 @@
 \newcommand{\INTTY}{{\key{int}}}
 \newcommand{\BOOLTY}{{\key{bool}}}
 \newcommand{\ANYTY}{{\key{AnyType}}}
+\newcommand{\CANYTY}{{\key{Any}}}
 \newcommand{\VECTY}[1]{{\key{TupleType}\LP\LS #1 \RS\RP}}
 \newcommand{\INTTYPE}{{\key{IntType}}}
 \newcommand{\COLLECT}[1]{\key{Collect}\LP#1\RP}
@@ -275,10 +278,10 @@
 \newcommand{\ANYVECLEN}[1]{\LP\key{Prim}~\code{any-vector-length}~\LP #1\RP\RP}
 
 \newcommand{\VOID}{\key{(Void)}}
-\newcommand{\CGLAMBDA}[3]{\LP\key{lambda:}\,#1\,#2~\Exp\RP}
 \newcommand{\VALUEOF}[2]{\LP\key{ValueOf}~#1~#2\RP}
 
 \if\edition\racketEd
+\newcommand{\CGLAMBDA}[3]{\LP\key{lambda:}\,#1\,#2~\Exp\RP}
 \newcommand{\ALLOC}[2]{\LP\key{Allocate}~#1~#2\RP}
 \newcommand{\ALLOCCLOS}[3]{\LP\key{AllocateClosure}~#1~#2~#3\RP}
 \newcommand{\INJECT}[2]{\LP\key{Inject}~#1~#2\RP}
@@ -298,6 +301,7 @@
 \newcommand{\FUNDEF}[5]{\key{(Def}~#1~#2~#3~#4~#5\code{)}}
 \fi
 \if\edition\pythonEd
+\newcommand{\CGLAMBDA}[3]{\key{lambda}\,#1\,#2\code{:}~\Exp}
 \newcommand{\ALLOC}[2]{\key{Allocate}\LP#1\code{, }#2\RP}
 \newcommand{\ALLOCCLOS}[3]{\key{AllocateClosure}\LP#1\code{, }#2\code{, }#3\RP}
 \newcommand{\INJECT}[2]{\key{Inject}\LP#1\key{, }#2\RP}
@@ -326,6 +330,7 @@
 \newcommand{\SEQ}[2]{\key{(Seq}~#1~#2\key{)}}
 
 \if\edition\racketEd
+\newcommand{\CGDEF}[4]{\LP\key{define}~\LP#1~#2\RP\,#3~#4\RP}
 \newcommand{\IMM}[1]{\key{(Imm}~#1\key{)}}
 \newcommand{\REG}[1]{\key{(Reg}~#1\key{)}}
 \newcommand{\DEREF}[2]{\key{(Deref}~#1~#2\key{)}}
@@ -345,6 +350,7 @@
 \newcommand{\TAILJMP}[2]{\key{(TailJmp}~#1~#2\key{)}}
 \fi
 \if\edition\pythonEd
+\newcommand{\CGDEF}[4]{\key{def}~#1\LP #2 \RP~#3 \code{:}~#4}
 \newcommand{\TAILJMP}[2]{\key{TailJmp}\LP#1\code{, }#2\RP}
 \newcommand{\INDCALLQ}[2]{\key{IndirectCallq}\LP#1\code{, }#2\RP}
 \newcommand{\IMM}[1]{\key{Immediate}\LP #1\RP}
@@ -369,7 +375,6 @@
 
 
 
-\newcommand{\CGDEF}[4]{\LP\key{define}~\LP#1~#2\RP\,#3~#4\RP}
 \newcommand{\DECL}[2]{\LP\key{Decl}~#1~#2\RP}
 \newcommand{\INST}[3]{\LP\key{Inst}~#1~#2~#3\RP}
 \newcommand{\CFG}[1]{\key{(CFG}~#1\key{)}}