check

book.tex

@@ -17038,8 +17038,8 @@ Languages that allow expressions to produce different kinds of values
 are called \emph{polymorphic}, a word composed of the Greek roots
 ``poly'', meaning ``many'', and ``morph'', meaning ``form''.  There
 are several kinds of polymorphism in programming languages, such as
-subtype polymorphism and parametric
-polymorphism~\citep{Cardelli:1985kx}. The kind of polymorphism we
+subtype polymorphism and parametric polymorphism
+(aka. generics)~\citep{Cardelli:1985kx}. The kind of polymorphism we
 study in this chapter does not have a special name but it is the kind
 that arises in dynamically typed languages.
 
@@ -20900,10 +20900,9 @@ the Grift compiler.
 \end{center}
 
 There are also interesting interactions between gradual typing and
-other language features, such as parametetric polymorphism,
-information-flow types, and type inference, to name a few. We
-recommend the reader to consult the online gradual typing bibliography
-for more material:
+other language features, such as generics, information-flow types, and
+type inference, to name a few. We recommend the reader to consult the
+online gradual typing bibliography for more material:
 \begin{center}
   \url{http://samth.github.io/gradual-typing-bib/}
 \end{center}
@@ -20939,12 +20938,20 @@ specified by the \code{All} type with parameter \code{T}.
   All[[T], Callable[[Callable[[T],T], tuple[T,T]], tuple[T,T]]]
 \end{lstlisting}
 \fi
+%
 The idea is that \code{map} can be used at \emph{all} choices of a
 type for parameter \code{T}. In Figure~\ref{fig:map-poly} we apply
-\code{map} to a tuple of integers, choosing
+\code{map} to a tuple of integers, implicitly choosing
 \racket{\code{Integer}}\python{\code{int}} for \code{T}, but we could
 have just as well applied \code{map} to a tuple of Booleans.
 %
+A \emph{monomorphic} function is simply one that is not generic.
+%
+We use the term \emph{instantiation} for the process (within the
+language implementation) of turning a generic function into a
+monomorphic one, where the type parameters have been replaced by
+types.
+
 \if\edition\pythonEd
 %
 In Python, when writing a generic function such as \code{map}, one
@@ -20983,7 +20990,7 @@ print(t[1])
 \fi
 \end{tcolorbox}
 
-\caption{The \code{map} example using parametric polymorphism.}
+\caption{A generic version of hte \code{map} function.}
 \label{fig:map-poly}
 \end{figure}
 
@@ -20999,7 +21006,7 @@ ignored in favor of the return type in the type declaration.  (The
 \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.
+it generic.
 \fi
 %
 The grammar for types is extended to include generic types and type
@@ -21029,7 +21036,7 @@ variables.
 
 \newcommand{\LpolyASTPython}{
 \begin{array}{lcl}
-  \Type &::=& \key{GenericType}\LP\LS\Var\ldots\RS, \Type\RP \MID \Var 
+  \Type &::=& \key{AllType}\LP\LS\Var\ldots\RS, \Type\RP \MID \Var 
 \end{array}
 }  
 
@@ -21170,22 +21177,20 @@ print(apply_twice(id))
 \fi
 \end{tcolorbox}
 
-\caption{An example illustrating first-class polymorphism.}
+\caption{An example illustrating first-class generics.}
 \label{fig:apply-twice}
 \end{figure}
 
-\if\edition\pythonEd
-UNDER CONSTRUCTION
-\fi
+{\color{red}[TODO: discuss generic function definitions]}
 
-The type checker for \LangPoly{} in Figure~\ref{fig:type-check-Lvar0} has
-three new responsibilities (compared to \LangLam{}). The type checking of
-function application is extended to handle the case where the operator
-expression is a polymorphic function. In that case the type arguments
-are deduced by matching the type of the parameters with the types of
-the arguments.
+The type checker for \LangPoly{} in Figure~\ref{fig:type-check-Lvar0}
+has several new responsibilities (compared to \LangLam{}). The type
+checking of function application is extended to handle the case where
+the operator expression is a generic function. In that case the type
+arguments are deduced by matching the type of the parameters with the
+types of the arguments.
 %
-The \code{match-types} auxiliary function carries out this deduction
+The \code{match\_types} auxiliary function carries out this deduction
 by recursively descending through a parameter type \code{pt} and the
 corresponding argument type \code{at}, making sure that they are equal
 except when there is a type parameter on the left (in the parameter
@@ -21195,87 +21200,38 @@ parameter to the corresponding type on the right (in the argument
 type). If it is not the first time that the type parameter has been
 encountered, the algorithm looks up its deduced type and makes sure
 that it is equal to the type on the right.
-%
-Once the type arguments are deduced, the operator expression is
-wrapped in an \code{Inst} AST node (for instantiate) that records the
-type of the operator, but more importantly, records the deduced type
-arguments. The return type of the application is the return type of
-the polymorphic function, but with the type parameters replaced by the
-deduced type arguments, using the \code{subst-type} function.
-
-The second responsibility of the type checker to extend the
-\code{type-equal?} function to handle the \code{All} type.  This is
-not quite as simple as for other types, such as function and tuple
-types, because two polymorphic types can be syntactically different
-even though they are equivalent types. For example, \code{(All (a) (a
-  -> a))} is equivalent to \code{(All (b) (b -> b))}.  Two polymorphic
-types should be considered equal if they differ only in the choice of
-the names of the type parameters. The \code{type-equal?} function in
-Figure~\ref{fig:type-check-Lvar0-aux} renames the type parameters of
-the first type to match the type parameters of the second type.
+%%
+%% Once the type arguments are deduced, the operator expression is
+%% wrapped in an \code{Inst} AST node (for instantiate) that records the
+%% type of the operator, but more importantly, records the deduced type
+%% arguments.
+%%
+The return type of the application is the return type of
+the generic function, but with the type parameters replaced by the
+deduced type arguments, using the \code{substitute\_type} function.
+
+The second responsibility of the type checker to extend type equality
+to handle the \code{All} type.  This is not quite as simple as for
+other types, such as function and tuple types, because two \code{All}
+types can be syntactically different even though they are equivalent.
+For example,
+\racket{\code{(All (T) (T -> T))}}
+\python{\code{All[[T], Callable[[T], T]]}}
+is equivalent to
+\racket{\code{(All (U) (U -> U))}}
+\python{\code{All[[U], Callable[[U], U]]}}.
+%
+Two generic types should be considered equal if they differ only in
+the choice of the names of the type parameters. The definition of type
+equality in Figure~\ref{fig:type-check-Lvar0-aux} renames the type
+parameters in one type to match the type parameters of the other type.
 
 The third responsibility of the type checker is to make sure that only
 defined type variables appear in type annotations. The
-\code{check-well-formed} function defined in
+\code{check\_well\_formed} function defined in
 Figure~\ref{fig:well-formed-types} recursively inspects a type, making
 sure that each type variable has been defined.
 
-The output language of the type checker is \LangInst{}, defined in
-Figure~\ref{fig:Lpoly-prime-syntax}. The type checker combines the type
-declaration and polymorphic function into a single definition, using
-the \code{Poly} form, to make polymorphic functions more convenient to
-process in next pass of the compiler.
-
-\begin{figure}[tp]
-\centering
-\begin{tcolorbox}[colback=white]
-\small
-\if\edition\racketEd
-\[
-\begin{array}{lcl}
-  \Type &::=& \ldots \MID \LP\key{All}~\LP\Var\ldots\RP~ \Type\RP \MID \Var \\
-  \Exp &::=& \ldots \MID \INST{\Exp}{\Type}{\LP\Type\ldots\RP} \\
-  \Def &::=& \gray{ \DEF{\Var}{\LP\LS\Var \key{:} \Type\RS \ldots\RP}{\Type}{\code{'()}}{\Exp} } \\
-   &\MID& \LP\key{Poly}~\LP\Var\ldots\RP~ \DEF{\Var}{\LP\LS\Var \key{:} \Type\RS \ldots\RP}{\Type}{\code{'()}}{\Exp}\RP  \\
-  \LangInst{} &::=& \PROGRAMDEFSEXP{\code{'()}}{\LP\Def\ldots\RP}{\Exp}
-\end{array}
-\]
-\fi
-\if\edition\pythonEd
-UNDER CONSTURCTION
-\fi
-\end{tcolorbox}
-
-\caption{The abstract syntax of \LangInst{}, extending \LangLam{}
-    (Figure~\ref{fig:Llam-syntax}).}
-\label{fig:Lpoly-prime-syntax}
-\end{figure}
-
-The output of the type checker on the polymorphic \code{map}
-example is listed in Figure~\ref{fig:map-type-check}.
-
-\begin{figure}[tbp]
-  % poly_test_2.rkt
-\begin{tcolorbox}[colback=white]  
-\if\edition\racketEd    
-\begin{lstlisting}
-(poly (a) (define (map [f : (a -> a)] [v : (Vector a a)]) : (Vector a a)
-  (vector (f (vector-ref v 0)) (f (vector-ref v 1)))))
-
-(define (inc [x : Integer]) : Integer (+ x 1))
-
-(vector-ref ((inst map (All (a) ((a -> a) (Vector a a) -> (Vector a a)))
-                           (Integer))
-              inc (vector 0 41)) 1)
-\end{lstlisting}
-\fi
-\if\edition\pythonEd
-UNDER CONSTRUCTION
-\fi
-\end{tcolorbox}
-\caption{Output of the type checker on the \code{map} example.}
-\label{fig:map-type-check}
-\end{figure}
 
 \begin{figure}[tbp]
   \begin{tcolorbox}[colback=white]
@@ -21298,24 +21254,24 @@ UNDER CONSTRUCTION
         [`(All ,xs (,tys ... -> ,rt))
          (define env^ (append (for/list ([x xs]) (cons x 'Type)) env))
          (define env^^ (for/fold ([env^^ env^]) ([arg-ty ty*] [param-ty tys])
-                         (match-types env^^ param-ty arg-ty)))
+                         (match_types env^^ param-ty arg-ty)))
          (define targs
            (for/list ([x xs])
              (match (dict-ref env^^ x (lambda () #f))
                [#f (error 'type-check "type variable ~a not deduced\nin ~v"
                           x (Apply e1 es))]
                [ty ty])))
-         (values (Inst e^ ty targs) es^ (subst-type env^^ rt))]
+         (values (Inst e^ ty targs) es^ (substitute_type env^^ rt))]
         [else (error 'type-check "expected a function, not ~a" ty)]))
     
     (define/override ((type-check-exp env) e)
       (match e
         [(Lambda `([,xs : ,Ts] ...) rT body)
-         (for ([T Ts]) ((check-well-formed env) T))
-         ((check-well-formed env) rT)
+         (for ([T Ts]) ((check_well_formed env) T))
+         ((check_well_formed env) rT)
          ((super type-check-exp env) e)]
         [(HasType e1 ty)
-         ((check-well-formed env) ty)
+         ((check_well_formed env) ty)
          ((super type-check-exp env) e)]
         [else ((super type-check-exp env) e)]))
 
@@ -21324,8 +21280,8 @@ UNDER CONSTRUCTION
       (match d
         [(Generic ts (Def f (and p:t* (list `[,xs : ,ps] ...)) rt info body))
          (define ts-env (for/list ([t ts]) (cons t 'Type)))
-         (for ([p ps]) ((check-well-formed ts-env) p))
-         ((check-well-formed ts-env) rt)
+         (for ([p ps]) ((check_well_formed ts-env) p))
+         ((check_well_formed ts-env) rt)
          (define new-env (append ts-env (map cons xs ps) env))
          (define-values (body^ ty^) ((type-check-exp new-env) body))
          (check-type-equal? ty^ rt body)
@@ -21364,24 +21320,24 @@ UNDER CONSTRUCTION
   (match* (t1 t2)
     [(`(All ,xs ,T1) `(All ,ys ,T2))
      (define env (map cons xs ys))
-     (type-equal? (subst-type env T1) T2)]
+     (type-equal? (substitute_type env T1) T2)]
     [(other wise)
      (super type-equal? t1 t2)]))
 
-(define/public (match-types env pt at)
+(define/public (match_types env pt at)
   (match* (pt at)
     [('Integer 'Integer) env] [('Boolean 'Boolean) env]
     [('Void 'Void) env] [('Any 'Any) env]
     [(`(Vector ,pts ...) `(Vector ,ats ...))
      (for/fold ([env^ env]) ([pt1 pts] [at1 ats])
-       (match-types env^ pt1 at1))]
+       (match_types env^ pt1 at1))]
     [(`(,pts ... -> ,prt) `(,ats ... -> ,art))
-     (define env^ (match-types env prt art))
+     (define env^ (match_types env prt art))
      (for/fold ([env^^ env^]) ([pt1 pts] [at1 ats])
-       (match-types env^^ pt1 at1))]
+       (match_types env^^ pt1 at1))]
     [(`(All ,pxs ,pt1) `(All ,axs ,at1))
      (define env^ (append (map cons pxs axs) env))
-     (match-types env^ pt1 at1)]
+     (match_types env^ pt1 at1)]
     [((? symbol? x) at)
      (match (dict-ref env x (lambda () #f))
        [#f (error 'type-check "undefined type variable ~a" x)]
@@ -21389,16 +21345,16 @@ UNDER CONSTRUCTION
        [t^ (check-type-equal? at t^ 'matching) env])]
     [(other wise) (error 'type-check "mismatch ~a != a" pt at)]))
 
-(define/public (subst-type env pt)
+(define/public (substitute_type env pt)
   (match pt
     ['Integer 'Integer] ['Boolean 'Boolean]
     ['Void 'Void] ['Any 'Any]
     [`(Vector ,ts ...)
-     `(Vector ,@(for/list ([t ts]) (subst-type env t)))]
+     `(Vector ,@(for/list ([t ts]) (substitute_type env t)))]
     [`(,ts ... -> ,rt)
-     `(,@(for/list ([t ts]) (subst-type env t)) -> ,(subst-type env rt))]
+     `(,@(for/list ([t ts]) (substitute_type env t)) -> ,(substitute_type env rt))]
     [`(All ,xs ,t)
-     `(All ,xs ,(subst-type (append (map cons xs xs) env) t))]
+     `(All ,xs ,(substitute_type (append (map cons xs xs) env) t))]
     [(? symbol? x) (dict-ref env x)]
     [else (error 'type-check "expected a type not ~a" pt)]))
 
@@ -21435,7 +21391,7 @@ UNDER CONSTRUCTION
 \begin{tcolorbox}[colback=white]  
 \if\edition\racketEd    
 \begin{lstlisting}%[basicstyle=\ttfamily\scriptsize]
-(define/public ((check-well-formed env) ty)
+(define/public ((check_well_formed env) ty)
   (match ty
     ['Integer (void)]
     ['Boolean (void)]
@@ -21445,13 +21401,13 @@ UNDER CONSTRUCTION
        ['Type (void)]
        [else (error 'type-check "undefined type variable ~a" a)])]
     [`(Vector ,ts ...)
-     (for ([t ts]) ((check-well-formed env) t))]
+     (for ([t ts]) ((check_well_formed env) t))]
     [`(,ts ... -> ,t)
-     (for ([t ts]) ((check-well-formed env) t))
-     ((check-well-formed env) t)]
+     (for ([t ts]) ((check_well_formed env) t))
+     ((check_well_formed env) t)]
     [`(All ,xs ,t)
      (define env^ (append (for/list ([x xs]) (cons x 'Type)) env))
-     ((check-well-formed env^) t)]
+     ((check_well_formed env^) t)]
     [else (error 'type-check "unrecognized type ~a" ty)]))
 \end{lstlisting}
 \fi
@@ -21467,82 +21423,204 @@ UNDER CONSTRUCTION
 % TODO: interpreter for R'_10
 \clearpage
 
-\section{Compiling Polymorphism}
+\section{Compiling Generics}
 \label{sec:compiling-poly}
 
-Broadly speaking, there are four approaches to compiling parametric
-polymorphism, which we describe below.
+Broadly speaking, there are four approaches to compiling generics,
+which we describe below.
 
 \begin{description}
-\item[Monomorphization] generates a different version of a polymorphic
+\item[Monomorphization] generates a different version of a generic
   function for each set of type arguments that it is used with,
   producing type-specialized code. This approach results in the most
   efficient code but requires whole-program compilation (no separate
-  compilation) and increases code size. For our current purposes
-  monomorphization is a non-starter because, with first-class
-  polymorphism, it is sometimes not possible to determine which
-  generic functions are used with which type arguments during
-  compilation. (It can be done at runtime, with just-in-time
-  compilation.) Monomorphization is used to compile C++
-  templates~\citep{stroustrup88:_param_types} and polymorphic
-  functions in NESL~\citep{Blelloch:1993aa} and
-  ML~\citep{Weeks:2006aa}.
+  compilation) and may increase code size.  Unfortunately,
+  monomorphization is incompatible with first-class generics
+  because it is not always possible to determine which generic
+  functions are used with which type arguments during compilation. (It
+  can be done at runtime, with just-in-time compilation.)
+  Monomorphization is used to compile C++
+  templates~\citep{stroustrup88:_param_types} and generic functions in
+  NESL~\citep{Blelloch:1993aa} and ML~\citep{Weeks:2006aa}.
   
-\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 \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 \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
-  least-efficient code because it introduces overhead in the entire
-  program. This approach is used in implementations of
-  CLU~\cite{liskov79:_clu_ref,Liskov:1993dk},
-  ML~\citep{Cardelli:1984aa,Appel:1987aa}, and
-  Java~\citep{Bracha:1998fk}.
+\item[Uniform representation] generates one version of each generic
+  function and requires all values to have a common ``boxed'' format,
+  such as the tagged values of type \CANYTY{} in \LangAny{}. Both
+  generic and 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 \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 generics.  However, it
+  produces the least-efficient code because it introduces overhead in
+  the entire program. This approach is used in
+  Java~\citep{Bracha:1998fk},
+  CLU~\cite{liskov79:_clu_ref,Liskov:1993dk}, and some implementations
+  of ML~\citep{Cardelli:1984aa,Appel:1987aa}.
   
-\item[Mixed representation] generates one version of each polymorphic
-  function, using a boxed representation for type
-  variables. Monomorphic code is compiled as usual (as in \LangLam{})
-  and conversions are performed at the boundaries between monomorphic
-  and polymorphic (e.g. when a polymorphic function is instantiated
+\item[Mixed representation] generates one version of each generic
+  function, using a boxed representation for type variables. However,
+  monomorphic code is compiled as usual (as in \LangLam{}) and
+  conversions are performed at the boundaries between monomorphic code
+  and polymorphic code (e.g. when a generic function is instantiated
   and called). This approach is compatible with separate compilation
-  and first-class polymorphism and maintains efficiency in monomorphic
+  and first-class generics and maintains efficiency in monomorphic
   code. The trade off is increased overhead at the boundary between
-  monomorphic and polymorphic code.  This approach is used in
+  monomorphic and generic code.  This approach is used in
   implementations of ML~\citep{Leroy:1992qb} and Java, starting in
   Java 5 with the addition of autoboxing.
   
 \item[Type passing] uses the unboxed representation in both
-  monomorphic and polymorphic code. Each polymorphic function is
-  compiled to a single function with extra parameters that describe
-  the type arguments. The type information is used by the generated
-  code to know how to access the unboxed values at runtime. This
-  approach is used in implementation of the Napier88
-  language~\citep{Morrison:1991aa} and ML~\citep{Harper:1995um}.  Type
-  passing is compatible with separate compilation and first-class
-  polymorphism and maintains the efficiency for monomorphic
-  code. There is runtime overhead in polymorphic code from dispatching
-  on type information.
+  monomorphic and generic code. Each generic function is compiled to a
+  single function with extra parameters that describe the type
+  arguments. The type information is used by the generated code to
+  know how to access the unboxed values at runtime. This approach is
+  used in implementation of Napier88~\citep{Morrison:1991aa} and
+  ML~\citep{Harper:1995um}.  Type passing is compatible with separate
+  compilation and first-class generics and maintains the
+  efficiency for monomorphic code. There is runtime overhead in
+  polymorphic code from dispatching on type information.
 \end{description}
 
 In this chapter we use the mixed representation approach, partly
 because of its favorable attributes, and partly because it is
 straightforward to implement using the tools that we have already
-built to support gradual typing. To compile polymorphic functions, we
-add just one new pass, \code{erase-types}, to compile \LangInst{} to
-\LangCast{}.
+built to support gradual typing. The work of compiling generic
+functions is performed in two passes, \code{resolve} and
+\code{erase\_types}, that we discuss next. The output of
+\code{erase\_types} is \LangCast{}
+(Section~\ref{sec:gradual-insert-casts}), so the rest of the
+compilation is handled by the compiler of Chapter~\ref{ch:Lgrad}.
+
+\section{Resolve Types}
+\label{sec:generic-resolve}
+
+Recall that the type checker for \LangPoly{} deduces the type
+arguments in a call to a generic function. The purpose of the
+\code{resolve} pass is to turn this implicit instantiation into an
+explicit one, by adding \code{Inst} nodes to the syntax of the
+intermediate language.  An \code{Inst} node records the mapping of
+type parameters to type arguments. The semantics of the \code{Inst}
+node is to instantiate the result of its first argument, a generic
+function, to produce a monomorphic function. However, because the
+interpreter never analyzes type annotations, instantiation can be a
+no-op and simply return the generic function.
+%
+The output language of the \code{resolve} pass is \LangInst{}, defined
+in Figure~\ref{fig:Lpoly-prime-syntax}.
+
+\if\edition\racketEd    
+The \code{resolve} pass combines the type declaration and polymorphic
+function into a single definition, using the \code{Poly} form, to make
+polymorphic functions more convenient to process in the next pass of the
+compiler.
+\fi
+
+\newcommand{\LinstASTRacket}{
+\begin{array}{lcl}
+  \Type &::=& \LP\key{All}~\LP\Var\ldots\RP~ \Type\RP \MID \Var \\
+  \Exp &::=& \INST{\Exp}{\Type}{\LP\Type\ldots\RP} \\
+  \Def &::=& \gray{ \DEF{\Var}{\LP\LS\Var \key{:} \Type\RS \ldots\RP}{\Type}{\code{'()}}{\Exp} } \\
+   &\MID& \LP\key{Poly}~\LP\Var\ldots\RP~ \DEF{\Var}{\LP\LS\Var \key{:} \Type\RS \ldots\RP}{\Type}{\code{'()}}{\Exp}\RP 
+\end{array}
+}  
+
+\newcommand{\LinstASTPython}{
+\begin{array}{lcl}
+  \Type &::=& \key{AllType}\LP\LS\Var\ldots\RS, \Type\RP \MID \Var \\
+  \Exp &::=& \INST{\Exp}{\LC\Var\key{:}\Type\ldots\RC} 
+\end{array}
+}
+
+\begin{figure}[tp]
+\centering
+\begin{tcolorbox}[colback=white]
+\small
+\if\edition\racketEd
+\[
+\begin{array}{l}
+  \gray{\LintOpAST} \\ \hline
+  \gray{\LvarASTRacket{}} \\ \hline
+  \gray{\LifASTRacket{}} \\ \hline
+  \gray{\LwhileASTRacket{}} \\ \hline
+  \gray{\LtupASTRacket{}} \\ \hline
+  \gray{\LfunASTRacket} \\ \hline
+  \gray{\LlambdaASTRacket} \\ \hline
+  \LinstASTRacket \\
+\begin{array}{lcl}
+  \LangInst{} &::=& \PROGRAMDEFSEXP{\code{'()}}{\LP\Def\ldots\RP}{\Exp}
+\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
+  \gray{\LfunASTPython} \\ \hline
+  \gray{\LlambdaASTPython} \\ \hline
+  \LinstASTPython \\
+  \begin{array}{lcl}
+  \LangInst{} &::=& \PROGRAM{}{\LS \Def \ldots \Stmt \ldots \RS}
+  \end{array}
+\end{array}
+\]
+\fi
+\end{tcolorbox}
+
+\caption{The abstract syntax of \LangInst{}, extending \LangLam{}
+    (Figure~\ref{fig:Llam-syntax}).}
+\label{fig:Lpoly-prime-syntax}
+\end{figure}
+
+The output of the \code{resolve} pass on the generic \code{map}
+example is listed in Figure~\ref{fig:map-resolve}. Note that the use
+of \code{map} is wrapped in an \code{inst} node, with the parameter
+\code{T} chosen to be \racket{\code{Integer}} \python{\code{int}}.
+
+\begin{figure}[tbp]
+  % poly_test_2.rkt
+\begin{tcolorbox}[colback=white]  
+\if\edition\racketEd    
+\begin{lstlisting}
+(poly (T) (define (map [f : (T -> T)] [v : (Vector T T)]) : (Vector T T)
+  (vector (f (vector-ref v 0)) (f (vector-ref v 1)))))
+
+(define (inc [x : Integer]) : Integer (+ x 1))
+
+(vector-ref ((inst map (All (T) ((T -> T) (Vector T T) -> (Vector T T)))
+                           (Integer))
+              inc (vector 0 41)) 1)
+\end{lstlisting}
+\fi
+\if\edition\pythonEd
+\begin{lstlisting}
+def map(f : Callable[[T],T], tup : tuple[T,T]) -> tuple[T,T]:
+    return (f(tup[0]), f(tup[1]))
+
+def add1(x : int) -> int:
+    return x + 1
+
+t = inst(map, {T: int})(add1, (0, 41))
+print(t[1])
+\end{lstlisting}
+\fi
+\end{tcolorbox}
+\caption{Output of the \code{resolve} pass on the \code{map} example.}
+\label{fig:map-resolve}
+\end{figure}
 
 \section{Erase Types}
-\label{sec:erase-types}
+\label{sec:erase_types}
 
 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
+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 \CANYTY{} and the polymorphic
 \code{All} types are removed from the type of \code{map}. 
@@ -21569,41 +21647,67 @@ UNDER CONSTRUCTION
 \fi
 \end{tcolorbox}
 
-\caption{The polymorphic \code{map} example after type erasure.}
+\caption{The generic \code{map} example after type erasure.}
 \label{fig:map-erase}
 \end{figure}
 
 This process of type erasure creates a challenge at points of
 instantiation. For example, consider the instantiation of
-\code{map} in Figure~\ref{fig:map-type-check}.
+\code{map} in Figure~\ref{fig:map-resolve}.
 The type of \code{map} is
+%
+\if\edition\racketEd    
+\begin{lstlisting}
+(All (T) ((T -> T) (Vector T T) -> (Vector T T)))
+\end{lstlisting}
+\fi
+\if\edition\pythonEd    
 \begin{lstlisting}
-(All (a) ((a -> a) (Vector a a) -> (Vector a a)))
+All[[T], Callable[[Callable[[T], T], tuple[T, T]], tuple[T, T]]]
 \end{lstlisting}
+\fi
+%
 and it is instantiated to 
+%
+\if\edition\racketEd
 \begin{lstlisting}
 ((Integer -> Integer) (Vector Integer Integer)
    -> (Vector Integer Integer))
 \end{lstlisting}
+\fi
+\if\edition\pythonEd
+\begin{lstlisting}
+Callable[[Callable[[int], int], tuple[int, int]], tuple[int, int]]
+\end{lstlisting}
+\fi
+%
 After erasure, the type of \code{map} is
+%
+\if\edition\racketEd
 \begin{lstlisting}
 ((Any -> Any) (Vector Any Any) -> (Vector Any Any))
 \end{lstlisting}
+\fi
+\if\edition\pythonEd
+\begin{lstlisting}
+Callable[[Callable[[Any], Any], tuple[Any, Any]], tuple[Any, Any]]
+\end{lstlisting}
+\fi
+%
 but we need to convert it to the instantiated type.  This is easy to
 do in the language \LangCast{} with a single \code{cast}.  In
 Figure~\ref{fig:map-erase}, the instantiation of \code{map} has been
 compiled to a \code{cast} from the type of \code{map} to the
 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
-\CANYTY{} in the former and with the deduced type arguments in the
-later. (Recall that the \CANYTY{} type is consistent with any type.)
+because both the source and target are obtained from the same generic
+type of \code{map}, replacing the type parameters with \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
-\CANYTY{}
+To implement the \code{erase\_types} pass, we first recommend defining
+a recursive function that translates types, named
+\code{erase\_type}. It replaces type variables with \CANYTY{}
 \begin{lstlisting}
 |$x$|
 |$\Rightarrow$|
@@ -21615,8 +21719,8 @@ and it removes the polymorphic \code{All} types.
 |$\Rightarrow$|
 |$T'_1$|
 \end{lstlisting}
-Apply the \code{erase-type} function to all of the type annotations in
-the program.
+Apply the \code{erase\_type} function to all of the type annotations
+in the program.
 
 Regarding the translation of expressions, the case for \code{Inst} is
 the interesting one. We translate it into a \code{Cast}, as shown
@@ -21630,7 +21734,7 @@ $T$ followed by doing type erasure.
 |$\Rightarrow$|
 (Cast |$e'$| |$T'$| |$T''$|)
 \end{lstlisting}
-where $T'' = \LP\code{erase-type}~\LP\code{subst-type}~s~T\RP\RP$
+where $T'' = \LP\code{erase-type}~\LP\code{substitute\_type}~s~T\RP\RP$
 and $s = \LP\code{map}~\code{cons}~xs~ts\RP$.
 
 Finally, each polymorphic function is translated to a regular
@@ -21646,7 +21750,7 @@ annotations and the body.
   Implement a compiler for the polymorphic language \LangPoly{} by
   extending and adapting your compiler for \LangGrad{}. Create 6 new test
   programs that use polymorphic functions. Some of them should make
-  use of first-class polymorphism. 
+  use of first-class generics. 
 \end{exercise}
 
 \begin{figure}[p]
@@ -21726,7 +21830,7 @@ UNDER CONSTRUCTION
 \fi
 \end{tcolorbox}
 
-\caption{Diagram of the passes for \LangPoly{} (parametric polymorphism).}
+\caption{Diagram of the passes for \LangPoly{} (generics).}
 \label{fig:Lpoly-passes}
 \end{figure}
 

defs.tex

@@ -392,6 +392,7 @@
 \newcommand{\DEF}[5]{\LP\key{Def}~#1~#2~#3~#4~#5\RP}
 \newcommand{\INDCALLQ}[2]{\key{(IndirectCallq}~#1~#2\key{)}}
 \newcommand{\TAILJMP}[2]{\key{(TailJmp}~#1~#2\key{)}}
+\newcommand{\INST}[3]{\LP\key{Inst}~#1~#2~#3\RP}
 \fi
 \if\edition\pythonEd
 \newcommand{\CGDEF}[4]{\key{def}~#1\LP #2 \RP~#3 \code{:}~#4}
@@ -415,12 +416,12 @@
 \newcommand{\CDEF}[4]{\key{def}~#1\LP #2 \RP ~\key{->}~ #3 \key{:}~#4}
 \newcommand{\CDEFU}[3]{\key{def}~#1\LP #2 \RP \key{:}~#3}
 \newcommand{\DEF}[6]{\key{FunctionDef}\LP#1\key{, }#2\key{, }#3\key{, }#4\key{, }#5\key{, }#6\RP}
+\newcommand{\INST}[2]{\key{Inst}\LP#1\key{, }#2\RP}
 \fi
 
 
 
 \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{)}}
 \newcommand{\BLOCK}[2]{\key{(Block}~#1~#2\key{)}}
 \newcommand{\STACKLOC}[1]{(\key{stack}~#1)}