check

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.
 %
@@ -16735,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'},
@@ -18420,13 +18420,13 @@ 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 \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}
@@ -18574,6 +18574,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)])
@@ -18583,14 +18584,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
@@ -18603,10 +18617,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}} predicate.
+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)
@@ -18622,40 +18645,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([consistent(p1, p2) for (p1,p2) in zip(ps1,ps2)]) \
+            and consistent(rt1, rt2)
+      case (TupleType(ts1), TupleType(ts2)):
+        return all([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.}
 \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
@@ -18677,6 +18705,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)])
@@ -18684,26 +18713,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)
@@ -18711,27 +18775,43 @@ 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}.
 
 
 \begin{figure}[tbp]
 \begin{tcolorbox}[colback=white]  
+{\if\edition\racketEd        
 \begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
 (define type-check-gradual-class
   (class type-check-Llambda-class
@@ -18791,6 +18871,10 @@ and \ref{fig:type-check-Lgradual-3}.
               (values (Prim 'any-vector-set! (list e1^ e2^^ e3^^)) 'Void)]
 	     [else (error 'type-check "expected vector not ~a\nin ~v" t1 e)])]
 \end{lstlisting}
+\fi}
+{\if\edition\pythonEd        
+UNDER CONSTRUCTION
+\fi}
 \end{tcolorbox}
 
 \caption{Type checker for the \LangGrad{} language, part 1.}
@@ -18799,6 +18883,7 @@ and \ref{fig:type-check-Lgradual-3}.
 
 \begin{figure}[tbp]
 \begin{tcolorbox}[colback=white]  
+  {\if\edition\racketEd
 \begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
           [(Prim 'eq? (list e1 e2))
            (define-values (e1^ t1) (recur e1))
@@ -18860,6 +18945,10 @@ and \ref{fig:type-check-Lgradual-3}.
            (define-values (e2^ T2) ((type-check-exp env) e2))
            (values (WhileLoop (make-cast e1^ T1 'Boolean) e2^) 'Void)]
 \end{lstlisting}
+\fi}
+{\if\edition\pythonEd        
+UNDER CONSTRUCTION
+\fi}
 \end{tcolorbox}
 
 \caption{Type checker for the \LangGrad{} language, part 2.}
@@ -18868,7 +18957,8 @@ and \ref{fig:type-check-Lgradual-3}.
 
 
 \begin{figure}[tbp]
-\begin{tcolorbox}[colback=white]  
+  \begin{tcolorbox}[colback=white]
+{\if\edition\racketEd            
 \begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
 	  [(Apply e1 e2s)
 	   (define-values (e1^ T1) (recur e1))
@@ -18900,6 +18990,10 @@ and \ref{fig:type-check-Lgradual-3}.
           [else  ((super type-check-exp env) e)]
           )))
 \end{lstlisting}
+\fi}
+{\if\edition\pythonEd        
+UNDER CONSTRUCTION
+\fi}
 \end{tcolorbox}
 
 \caption{Type checker for the \LangGrad{} language, part 3.}
@@ -18909,6 +19003,7 @@ and \ref{fig:type-check-Lgradual-3}.
 
 \begin{figure}[tbp]
 \begin{tcolorbox}[colback=white]  
+{\if\edition\racketEd            
 \begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
     (define/public (join t1 t2)
       (match* (t1 t2)
@@ -18972,6 +19067,10 @@ and \ref{fig:type-check-Lgradual-3}.
 	 `(,@ps -> ,rt)]
 	[else (error 'fun-def-type "ill-formed function definition in ~a" d)]))
 \end{lstlisting}
+\fi}
+{\if\edition\pythonEd        
+UNDER CONSTRUCTION
+\fi}
 \end{tcolorbox}
 
 \caption{Auxiliary functions for type checking \LangGrad{}.}
@@ -18983,30 +19082,34 @@ and \ref{fig:type-check-Lgradual-3}.
 \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
@@ -19051,21 +19154,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]
@@ -19082,7 +19185,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}
 
@@ -19258,7 +19361,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]  
@@ -19369,7 +19472,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.
@@ -19380,7 +19483,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.
   
@@ -19532,9 +19635,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
@@ -19561,7 +19664,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:
@@ -19746,9 +19849,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
@@ -20141,12 +20244,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
@@ -20191,11 +20294,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]
@@ -20243,13 +20346,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

@@ -156,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{)}}
@@ -219,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}