ch 10

book.tex

@@ -18289,7 +18289,7 @@ UNDER CONSTRUCTION
 
 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 \LangLoop{} language
+of a program, thereby mixing the statically typed \LangLam{} language
 with the dynamically typed \LangDyn{}. There are several approaches to
 mixing static and dynamic typing, including multi-language
 integration~\citep{Tobin-Hochstadt:2006fk,Matthews:2007zr} and hybrid
@@ -18300,48 +18300,59 @@ 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:Rgrad-concrete-syntax} and its abstract syntax is defined
-in Figure~\ref{fig:Rgrad-syntax}. The main syntactic difference between
-\LangLoop{} and \LangGrad{} is the additional \itm{param} and \itm{ret}
+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.
 
+\newcommand{\LgradGrammarRacket}{
+\begin{array}{lcl}
+  \Type &::=& (\Type \ldots \; \key{->}\; \Type) \\
+  \itm{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& \LP \key{procedure-arity}~\Exp\RP \\
+  \Def &::=& \CGDEF{\Var}{\itm{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 \\
+  \Exp &::=& \APPLY{\Exp}{\Exp\ldots}
+  \MID \LAMBDA{\LP\itm{param}\ldots\RP}{\Type}{\Exp} \\
+  \itm{op} &::=& \code{procedure-arity} \\
+ \Def &::=& \FUNDEF{\Var}{\LP\itm{param}\ldots\RP}{\Type}{\code{'()}}{\Exp} 
+\end{array}
+}
+
 \begin{figure}[tp]
 \centering
 \fbox{
   \begin{minipage}{0.96\textwidth}
     \small
 \[
+\begin{array}{l}
+  \gray{\LintGrammarRacket{}} \\ \hline
+  \gray{\LvarGrammarRacket{}} \\ \hline
+  \gray{\LifGrammarRacket{}} \\ \hline
+  \gray{\LwhileGrammarRacket} \\ \hline
+  \gray{\LtupGrammarRacket} \\   \hline
+  \LgradGrammarRacket \\
 \begin{array}{lcl}
-  \itm{param} &::=& \Var \MID \LS\Var \key{:} \Type\RS \\
-  \itm{ret} &::=& \epsilon \MID \key{:} \Type \\
-  \Exp &::=& \gray{ \Int \MID \CREAD{} \MID \CNEG{\Exp}
-     \MID \CADD{\Exp}{\Exp} \MID \CSUB{\Exp}{\Exp} }  \\
-    &\MID&  \gray{ \Var \MID \CLET{\Var}{\Exp}{\Exp} }\\
-    &\MID& \gray{\key{\#t} \MID \key{\#f} 
-     \MID (\key{and}\;\Exp\;\Exp) 
-     \MID (\key{or}\;\Exp\;\Exp) 
-     \MID (\key{not}\;\Exp) } \\
-    &\MID& \gray{ (\key{eq?}\;\Exp\;\Exp) \MID \CIF{\Exp}{\Exp}{\Exp} } \\
-    &\MID& \gray{ (\key{vector}\;\Exp\ldots) \MID
-          (\key{vector-ref}\;\Exp\;\Int)} \\
-    &\MID& \gray{(\key{vector-set!}\;\Exp\;\Int\;\Exp)\MID (\key{void})
-    \MID (\Exp \; \Exp\ldots) } \\
-    &\MID& \gray{ \LP \key{procedure-arity}~\Exp\RP }
-    \MID \CGLAMBDA{\LP\itm{param}\ldots\RP}{\itm{ret}}{\Exp} \\
-  &\MID& \gray{ \CSETBANG{\Var}{\Exp}
-  \MID \CBEGIN{\Exp\ldots}{\Exp}
-  \MID \CWHILE{\Exp}{\Exp} } \\
-  \Def &::=& \CGDEF{\Var}{\itm{param}\ldots}{\itm{ret}}{\Exp} \\
   \LangGradM{} &::=& \gray{\Def\ldots \; \Exp}
 \end{array}
+\end{array}
 \]
 \end{minipage}
 }
-\caption{The concrete syntax of \LangGrad{}, extending \LangLoop{} (Figure~\ref{fig:Lwhile-concrete-syntax}).}
-\label{fig:Rgrad-concrete-syntax}
+\caption{The concrete syntax of \LangGrad{}, extending \LangVec{} (Figure~\ref{fig:Lvec-concrete-syntax}).}
+\label{fig:Lgrad-concrete-syntax}
 \end{figure}
 
 \begin{figure}[tp]
@@ -18350,25 +18361,22 @@ syntax.
   \begin{minipage}{0.96\textwidth}
     \small
 \[
+\begin{array}{l}
+  \gray{\LintOpAST} \\ \hline
+  \gray{\LvarASTRacket{}} \\ \hline
+  \gray{\LifASTRacket{}} \\ \hline
+  \gray{\LwhileASTRacket{}} \\ \hline
+  \gray{\LtupASTRacket{}} \\ \hline
+  \LgradASTRacket \\
 \begin{array}{lcl}
-  \itm{param} &::=& \Var \MID \LS\Var \key{:} \Type\RS \\
-  \Exp &::=& \gray{ \INT{\Int} \VAR{\Var} \MID \LET{\Var}{\Exp}{\Exp} } \\
-       &\MID& \gray{ \PRIM{\itm{op}}{\Exp\ldots} }\\
-     &\MID& \gray{ \BOOL{\itm{bool}}
-      \MID \IF{\Exp}{\Exp}{\Exp} } \\
-     &\MID& \gray{ \VOID{} \MID \LP\key{HasType}~\Exp~\Type \RP 
-     \MID \APPLY{\Exp}{\Exp\ldots} }\\
-  &\MID& \LAMBDA{\LP\itm{param}\ldots\RP}{\Type}{\Exp} \\
-  &\MID& \gray{ \SETBANG{\Var}{\Exp} \MID \BEGIN{\LP\Exp\ldots\RP}{\Exp} } \\
-  &\MID& \gray{ \WHILE{\Exp}{\Exp} } \\
- \Def &::=& \FUNDEF{\Var}{\LP\itm{param}\ldots\RP}{\Type}{\code{'()}}{\Exp} \\
-  \LangGradM{} &::=& \gray{ \PROGRAMDEFSEXP{\code{'()}}{\LP\Def\ldots\RP}{\Exp} }
+  \LangGradM{} &::=& \PROGRAMDEFSEXP{\code{'()}}{\LP\Def\ldots\RP}{\Exp}
+\end{array}
 \end{array}
 \]
 \end{minipage}
 }
-\caption{The abstract syntax of \LangGrad{}, extending \LangLoop{} (Figure~\ref{fig:Lwhile-syntax}).}
-\label{fig:Rgrad-syntax}
+\caption{The abstract syntax of \LangGrad{}, extending \LangVec{} (Figure~\ref{fig:Lvec-syntax}).}
+\label{fig:Lgrad-syntax}
 \end{figure}
 
 
@@ -18376,9 +18384,9 @@ syntax.
 Both the type checker and the interpreter for \LangGrad{} require some
 interesting changes to enable gradual typing, which we discuss in the
 next two sections in the context of the \code{map} example from
-Chapter~\ref{ch:Lfun}.  In Figure~\ref{fig:gradual-map} we
-revised the \code{map} example, omitting the type annotations from
-the \code{inc} function.
+Chapter~\ref{ch:Lfun}.  In Figure~\ref{fig:gradual-map} we revisit the
+\code{map} example, omitting the type annotations from the \code{inc}
+function.
 
 \begin{figure}[btp]
 % gradual_test_9.rkt
@@ -18439,42 +18447,43 @@ 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 the
-\code{map} to a function that sometimes returns a Boolean, as
-shown in Figure~\ref{fig:map-maybe-inc}.  The type checker for
-\LangGrad{} accepts this program because the type of \code{maybe-inc} is
-consistent with the type of parameter \code{f} of \code{map}, that
-is, \code{(Any -> 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
+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
 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}. \LangGrad{}
-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} to \LangLoop{}, as shown in
-Figure~\ref{fig:Rgrad-prime-syntax}.
+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}.
 
-\begin{figure}[tp]
-\centering
-\fbox{
-\begin{minipage}{0.96\textwidth}
-\small
-\[
-\begin{array}{lcl}
-  \Exp &::=& \ldots \MID \CAST{\Exp}{\Type}{\Type} \\
-  \LangCastM{} &::=& \gray{ \PROGRAMDEFSEXP{\code{'()}}{\LP\Def\ldots\RP}{\Exp} }
-\end{array}
-\]
-\end{minipage}
-}
-\caption{The abstract syntax of \LangCast{}, extending \LangLoop{} (Figure~\ref{fig:Lwhile-syntax}).}
-\label{fig:Rgrad-prime-syntax}
-\end{figure}
+%% \begin{figure}[tp]
+%% \centering
+%% \fbox{
+%% \begin{minipage}{0.96\textwidth}
+%% \small
+%% \[
+%% \begin{array}{lcl}
+%%   \Exp &::=& \ldots \MID \CAST{\Exp}{\Type}{\Type} \\
+%%   \LangCastM{} &::=& \gray{ \PROGRAMDEFSEXP{\code{'()}}{\LP\Def\ldots\RP}{\Exp} }
+%% \end{array}
+%% \]
+%% \end{minipage}
+%% }
+%% \caption{The abstract syntax of \LangCast{}, extending \LangLam{} (Figure~\ref{fig:Lwhile-syntax}).}
+%% \label{fig:Lgrad-prime-syntax}
+%% \end{figure}
 
 
 \begin{figure}[tbp]
@@ -18522,14 +18531,14 @@ is cast from \code{(Any -> Any)} to \code{(Integer -> Integer)}.
 
 
 The type checker for \LangGrad{} is defined in
-Figures~\ref{fig:type-check-Rgradual-1}, \ref{fig:type-check-Rgradual-2},
-and \ref{fig:type-check-Rgradual-3}.
+Figures~\ref{fig:type-check-Lgradual-1}, \ref{fig:type-check-Lgradual-2},
+and \ref{fig:type-check-Lgradual-3}.
 
 
 \begin{figure}[tbp]
 \begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
 (define type-check-gradual-class
-  (class type-check-Lwhile-class
+  (class type-check-Llambda-class
     (super-new)
     (inherit operator-types type-predicates)
 
@@ -18587,7 +18596,7 @@ and \ref{fig:type-check-Rgradual-3}.
 	     [else (error 'type-check "expected vector not ~a\nin ~v" t1 e)])]
 \end{lstlisting}
 \caption{Type checker for the \LangGrad{} language, part 1.}
-\label{fig:type-check-Rgradual-1}
+\label{fig:type-check-Lgradual-1}
 \end{figure}
 
 \begin{figure}[tbp]
@@ -18653,7 +18662,7 @@ and \ref{fig:type-check-Rgradual-3}.
            (values (WhileLoop (make-cast e1^ T1 'Boolean) e2^) 'Void)]
 \end{lstlisting}
 \caption{Type checker for the \LangGrad{} language, part 2.}
-\label{fig:type-check-Rgradual-2}
+\label{fig:type-check-Lgradual-2}
 \end{figure}
 
 
@@ -18690,7 +18699,7 @@ and \ref{fig:type-check-Rgradual-3}.
           )))
 \end{lstlisting}
 \caption{Type checker for the \LangGrad{} language, part 3.}
-\label{fig:type-check-Rgradual-3}
+\label{fig:type-check-Lgradual-3}
 \end{figure}
 
 
@@ -18759,7 +18768,7 @@ and \ref{fig:type-check-Rgradual-3}.
 	[else (error 'fun-def-type "ill-formed function definition in ~a" d)]))
 \end{lstlisting}
 \caption{Auxiliary functions for type checking \LangGrad{}.}
-\label{fig:type-check-Rgradual-aux}
+\label{fig:type-check-Lgradual-aux}
 \end{figure}
 
 \clearpage
@@ -18779,7 +18788,7 @@ 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 vector types.
+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
@@ -18792,20 +18801,20 @@ 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}.
 
-Turning our attention to casts involving vector types, we consider the
+Turning our attention to casts involving tuple types, we consider the
 example in Figure~\ref{fig:map-bang} that defines a
 partially-typed version of \code{map} whose parameter \code{v} has
 type \code{(Vector Any Any)} and that updates \code{v} in place
-instead of returning a new vector. So we name this function
-\code{map!}. We apply \code{map!} to a vector of integers, so
+instead of returning a new tuple. So we name this function
+\code{map!}. We apply \code{map!} to a tuple of integers, so
 the type checker inserts a cast from \code{(Vector Integer Integer)}
 to \code{(Vector Any Any)}. A naive way for the \LangCast{} interpreter to
-cast between vector types would be a build a new vector whose elements
+cast between tuple types would be a build a new tuple whose elements
 are the result of casting each of the original elements to the
 appropriate target type. However, this approach is only valid for
-immutable vectors; and our vectors are mutable. In the example of
-Figure~\ref{fig:map-bang}, if the cast created a new vector, then
-the updates inside of \code{map!} would happen to the new vector
+immutable tuples; and our tuples are mutable. In the example of
+Figure~\ref{fig:map-bang}, if the cast created a new tuple, then
+the updates inside of \code{map!} would happen to the new tuple
 and not the original one.
 
 \begin{figure}[tbp]
@@ -18827,20 +18836,20 @@ and not the original one.
 \end{figure}
 
 Instead the interpreter needs to create a new kind of value, a
-\emph{vector proxy}, that intercepts every vector operation. On a
-read, the proxy reads from the underlying vector and then applies a
+\emph{tuple proxy}, that intercepts every tuple operation. On a
+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 vector. For the
+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}
 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 vector
+the \code{Any} 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 vector has
+given type \code{Any}. 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
 thought is to use \code{Inject}, but that doesn't work because
@@ -18860,7 +18869,7 @@ to \code{Any}.
 (let ([v (vector 0 41)])
   (begin (map! inc v) (vector-ref v 1)))
 \end{lstlisting}
-\caption{Casting a vector to \code{Any}.}
+\caption{Casting a tuple to \code{Any}.}
 \label{fig:map-any}
 \end{figure}
 
@@ -18920,14 +18929,14 @@ of the kinds of casts that we've discussed in this section.
 
 The interpreter for \LangCast{} is defined in
 Figure~\ref{fig:interp-Lcast}, with the case for \code{Cast}
-dispatching to \code{apply-cast}. To handle the addition of vector
-proxies, we update the vector primitives in \code{interp-op} using the
-functions in Figure~\ref{fig:guarded-vector}.
+dispatching to \code{apply-cast}. To handle the addition of tuple
+proxies, we update the tuple primitives in \code{interp-op} using the
+functions in Figure~\ref{fig:guarded-tuple}.
 
 \begin{figure}[tbp]
 \begin{lstlisting}[basicstyle=\ttfamily\footnotesize]
 (define interp-Lcast-class
-  (class interp-Lwhile-class
+  (class interp-Llambda-class
     (super-new)
     (inherit apply-fun apply-inject apply-project)
 
@@ -18988,8 +18997,8 @@ functions in Figure~\ref{fig:guarded-vector}.
          (guarded-vector-length (vector-ref proxy 0))]
         [else (vector-length vec)]))
 \end{lstlisting}
-\caption{The guarded-vector auxiliary functions.}
-  \label{fig:guarded-vector}
+\caption{The \code{guarded-vector} auxiliary functions.}
+  \label{fig:guarded-tuple}
 \end{figure}
 
 
@@ -18999,7 +19008,7 @@ functions in Figure~\ref{fig:guarded-vector}.
 The next step in the journey towards x86 is the \code{lower-casts}
 pass that translates the casts in \LangCast{} to the lower-level
 \code{Inject} and \code{Project} operators and a new operator for
-creating vector proxies, extending the \LangLoop{} language to create
+creating tuple proxies, extending the \LangLam{} language to create
 \LangProxy{}. We recommend creating an auxiliary function named
 \code{lower-cast} that takes an expression (in \LangCast{}), a source type,
 and a target type, and translates it to expression in \LangProxy{} that has
@@ -19011,24 +19020,24 @@ the \code{apply-cast} function (Figure~\ref{fig:apply-cast}) used in
 the interpreter for \LangCast{} because it must handle the same cases as
 \code{apply-cast} and it needs to mimic the behavior of
 \code{apply-cast}. The most interesting cases are those concerning the
-casts between two vector types and between two function types.
+casts between two tuple types and between two function types.
 
-As mentioned in Section~\ref{sec:interp-casts}, a cast from one vector
-type to another vector type is accomplished by creating a proxy that
-intercepts the operations on the underlying vector. Here we make the
+As mentioned in Section~\ref{sec:interp-casts}, a cast from one tuple
+type to another tuple type is accomplished by creating a proxy that
+intercepts the operations on the underlying tuple. Here we make the
 creation of the proxy explicit with the \code{vector-proxy} primitive
 operation. It takes three arguments, the first is an expression for
-the vector, the second is a vector of functions for casting an element
-that is being read from the vector, and the third is a vector of
-functions for casting an element that is being written to the vector.
+the tuple, the second is a tuple of functions for casting an element
+that is being read from the tuple, and the third is a tuple of
+functions for casting an element that is being written to the tuple.
 You can create the functions using \code{Lambda}. Also, as we shall
-see in the next section, we need to differentiate these vectors from
+see in the next section, we need to differentiate these tuples from
 the user-created ones, so we recommend using a new primitive operator
 named \code{raw-vector} instead of \code{vector} to create these
-vectors of functions. Figure~\ref{fig:map-bang-lower-cast} shows
+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 vector of
-integers to a vector of \code{Any}.
+Figure~\ref{fig:map-bang} that involved casting a tuple of
+integers to a tuple of \code{Any}.
 
 \begin{figure}[tbp]
 \begin{lstlisting}
@@ -19061,14 +19070,14 @@ integers to a vector of \code{Any}.
 A cast from one function type to another function type is accomplished
 by generating a \code{Lambda} whose parameter and return types match
 the target function type. The body of the \code{Lambda} should cast
-the parameters from the target type to the source type (yes,
-backwards! functions are contravariant\index{subject}{contravariant} in the
-parameters), then call the underlying function, and finally cast the
-result from the source return type to the target return type.
+the parameters from the target type to the source type. (Yes,
+backwards! Functions are contravariant\index{subject}{contravariant}
+in the parameters.). Afterwards, call the underlying function and then
+cast the result from the source return type to the target return type.
 Figure~\ref{fig:map-lower-cast} shows the output of the
 \code{lower-casts} pass on the \code{map} example in
-Figure~\ref{fig:gradual-map}. Note that the \code{inc} argument
-in the call to \code{map} is wrapped in a \code{lambda}.
+Figure~\ref{fig:gradual-map}. Note that the \code{inc} argument in the
+call to \code{map} is wrapped in a \code{lambda}.
 
 \begin{figure}[tbp]
 \begin{lstlisting}
@@ -19093,26 +19102,26 @@ in the call to \code{map} is wrapped in a \code{lambda}.
 \section{Differentiate Proxies}
 \label{sec:differentiate-proxies}
 
-So far the job of differentiating vectors and vector proxies has been
+So far the job of differentiating tuples and tuple proxies has been
 the job of the interpreter. For example, the interpreter for \LangCast{}
 implements \code{vector-ref} using the \code{guarded-vector-ref}
-function in Figure~\ref{fig:guarded-vector}.  In the
+function in Figure~\ref{fig:guarded-tuple}.  In the
 \code{differentiate-proxies} pass we shift this responsibility to the
 generated code.
 
-We begin by designing the output language $R^p_8$.  In
-\LangGrad{} we used the type \code{Vector} for both real vectors and vector
-proxies. In $R^p_8$ we return the \code{Vector} type to
-its original meaning, as the type of real vectors, and we introduce a
-new type, \code{PVector}, whose values can be either real vectors or
-vector proxies. This new type comes with a suite of new primitive
-operations for creating and using values of type \code{PVector}. We
-don't need to introduce a new type to represent vector proxies.  A
-proxy is represented by a vector containing three things: 1) the
-underlying vector, 2) a vector of functions for casting elements that
-are read from the vector, and 3) a vector of functions for casting
-values to be written to the vector. So we define the following
-abbreviation for the type of a vector proxy:
+We begin by designing the output language \LangPVec.  In
+\LangGrad{} we used the type \code{Vector} for both real tuples and tuple
+proxies. In \LangPVec we return the \code{Vector} type to
+its original meaning, as the type of real tuples, and we introduce a
+new type, \code{PVector}, whose values can be either real tuples or
+tuple proxies. This new type comes with a suite of new primitive
+operations for creating and using values of type \code{PVector}.
+%We don't need to introduce a new type to represent tuple proxies.
+A proxy is represented by a tuple containing three things: 1) the
+underlying tuple, 2) a tuple of functions for casting elements that
+are read from the tuple, and 3) a tuple of functions for casting
+values to be written to the tuple. So we define the following
+abbreviation for the type of a tuple proxy:
 \[
 \itm{Proxy} (T\ldots \Rightarrow T'\ldots)
 = (\ttm{Vector}~(\ttm{PVector}~ T\ldots) ~R~ W)
@@ -19135,37 +19144,36 @@ Next we describe each of the new primitive operations.
 \item[\code{proxy?} : (\key{PVector} $T \ldots$) $\to$
   \code{Boolean}] \ \\
 %
-  returns true if the value is a vector proxy and false if it is a
-  real vector.
+  This returns true if the value is a tuple proxy and false if it is a
+  real tuple.
 \item[\code{project-vector} : (\key{PVector} $T \ldots$) $\to$
   (\key{Vector} $T \ldots$)]\ \\
 %
-  Assuming that the input is a vector (and not a proxy), this
-  operation returns the vector.
+  Assuming that the input is a tuple, this operation returns the
+  tuple.
   
 \item[\code{proxy-vector-length} : (\key{PVector} $T \ldots$)
   $\to$ \code{Boolean}]\ \\
 %
-  Given a vector proxy, this operation returns the length of the
-  underlying vector.
+  Given a tuple proxy, this operation returns the length of the tuple.
   
 \item[\code{proxy-vector-ref} : (\key{PVector} $T \ldots$)
   $\to$ ($i$ : \code{Integer}) $\to$ $T_i$]\ \\
 %
-  Given a vector proxy, this operation returns the $i$th element of
-  the underlying vector.
+  Given a tuple proxy, this operation returns the $i$th element of the
+  tuple.
   
 \item[\code{proxy-vector-set!} : (\key{PVector} $T \ldots$) $\to$ ($i$
-  : \code{Integer}) $\to$ $T_i$ $\to$ \key{Void}]\ \\ Given a vector
-  proxy, this operation writes a value to the $i$th element of the
-  underlying vector.
+  : \code{Integer}) $\to$ $T_i$ $\to$ \key{Void}]\ \\
+  Given a tuple proxy, this operation writes a value to the $i$th element
+  of the tuple.
 \end{description}
 
-Now to discuss the translation that differentiates vectors from
-proxies. First, every type annotation in the program must be
-translated (recursively) to replace \code{Vector} with \code{PVector}.
-Next, we must insert uses of \code{PVector} operations in the
-appropriate places. For example, we wrap every vector creation with an
+Now to discuss the translation that differentiates tuples from
+proxies. First, every type annotation in the program is translated
+(recursively) to replace \code{Vector} with \code{PVector}.  Next, we
+insert uses of \code{PVector} operations in the appropriate
+places. For example, we wrap every tuple creation with an
 \code{inject-vector}.
 \begin{lstlisting}
 (vector |$e_1 \ldots e_n$|)
@@ -19187,9 +19195,9 @@ The \code{vector-proxy} primitive translates as follows.
 (inject-proxy (vector |$e'_1~e'_2~e'_3$|))
 \end{lstlisting}
 
-We translate the vector operations into conditional expressions that
+We translate the tuple operations into conditional expressions that
 check whether the value is a proxy and then dispatch to either the
-appropriate proxy vector operation or the regular vector operation.
+appropriate proxy tuple operation or the regular tuple operation.
 For example, the following is the translation for \code{vector-ref}.
 \begin{lstlisting}
 (vector-ref |$e_1$| |$i$|)
@@ -19199,7 +19207,7 @@ For example, the following is the translation for \code{vector-ref}.
     (proxy-vector-ref |$v$| |$i$|)
     (vector-ref (project-vector |$v$|) |$i$|)
 \end{lstlisting}
-Note in the case of a real vector, we must apply \code{project-vector}
+Note in the case of a real tuple, we must apply \code{project-vector}
 before the \code{vector-ref}.
 
 \section{Reveal Casts}
@@ -19243,10 +19251,10 @@ operations on the \code{PVector} type.
 Recall that the \code{select\_instructions} pass is responsible for
 lowering the primitive operations into x86 instructions.  So we need
 to translate the new \code{PVector} operations to x86.  To do so, the
-first question we need to answer is how will we differentiate the two
-kinds of values (vectors and proxies) that can inhabit \code{PVector}.
+first question we need to answer is how to differentiate the two
+kinds of values (tuples and proxies) that can inhabit \code{PVector}.
 We need just one bit to accomplish this, and use the bit in position
-$57$ of the 64-bit tag at the front of every vector (see
+$57$ of the 64-bit tag at the front of every tuple (see
 Figure~\ref{fig:tuple-rep}). So far, this bit has been set to $0$, so
 for \code{inject-vector} we leave it that way.
 \begin{lstlisting}
@@ -19267,7 +19275,7 @@ movq %r11, |$\itm{lhs'}$|
 
 The \code{proxy?} operation consumes the information so carefully
 stashed away by \code{inject-vector} and \code{inject-proxy}.  It
-isolates the $57$th bit to tell whether the value is a real vector or
+isolates the $57$th bit to tell whether the value is a real tuple or
 a proxy.
 \begin{lstlisting}
 (Assign |$\itm{lhs}$| (Prim 'proxy? (list e)))
@@ -19284,7 +19292,7 @@ so we leave it up to the reader.
 
 Regarding the \code{proxy-vector} operations, the runtime provides
 procedures that implement them (they are recursive functions!)  so
-here we simply need to translate these vector operations into the
+here we simply need to translate these tuple operations into the
 appropriate function call. For example, here is the translation for
 \code{proxy-vector-ref}.
 \begin{lstlisting}
@@ -19296,18 +19304,18 @@ callq proxy_vector_ref
 movq %rax, |$\itm{lhs'}$|
 \end{lstlisting}
 
-We have another batch of vector operations to deal with, those for the
-\code{Any} 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 \code{any-vector-set!}  and
-\code{any-vector-length} (Figure~\ref{fig:type-check-Rgradual-1}). In
+We have another batch of tuple operations to deal with, those for the
+\code{Any} 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
+\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
 operations based on the idea that the underlying value was a real
-vector. But in the current setting, the underlying value is of type
-\code{PVector}. So \code{any-vector-ref} can be translates to
-pseudo-x86 as follows. We begin by projecting the underlying value out
-of the tagged value and then call the \code{proxy\_vector\_ref}
-procedure in the runtime.
+tuple. But in the current setting, the underlying value is of type
+\code{PVector}. So \code{any-vector-ref} can be translated follows. We
+begin by projecting the underlying value out of the tagged value and
+then call the \code{proxy\_vector\_ref} procedure in the runtime.
 \begin{lstlisting}
 (Assign |$\itm{lhs}$| (Prim 'any-vector-ref (list |$e_1$| |$e_2$|)))
 movq |$\neg 111$|, %rdi
@@ -19321,9 +19329,9 @@ be translated in a similar way.
 
 \begin{exercise}\normalfont\normalsize
   Implement a compiler for the gradually-typed \LangGrad{} language by
-  extending and adapting your compiler for \LangLoop{}. Create 10 new
+  extending and adapting your compiler for \LangLam{}. Create 10 new
   partially-typed test programs. In addition to testing with these
-  new programs, also test your compiler on all the tests for \LangLoop{}
+  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
@@ -19335,19 +19343,20 @@ be translated in a similar way.
 
 \begin{figure}[p]
 \begin{tikzpicture}[baseline=(current  bounding  box.center)]
-\node (Rgradual) at (6,4)  {\large \LangGrad{}};
-\node (Rgradualp) at (3,4)  {\large \LangCast{}};
-\node (Lwhilepp) at (0,4)  {\large \LangProxy{}};
-\node (Lwhileproxy) at (0,2)  {\large \LangPVec{}};
-\node (Lwhileproxy-2) at (3,2)  {\large \LangPVec{}};
-\node (Lwhileproxy-3) at (6,2)  {\large \LangPVec{}};
-\node (Lwhileproxy-4) at (9,2)  {\large \LangPVecFunRef{}};
-\node (Lwhileproxy-5) at (12,2)  {\large \LangPVecFunRef{}};
-\node (F1-1) at (12,0)  {\large \LangPVecFunRef{}};
-\node (F1-2) at (9,0)  {\large \LangPVecFunRef{}};
-\node (F1-3) at (6,0)  {\large \LangPVecFunRef{}};
-\node (F1-4) at (3,0)  {\large \LangPVecAlloc{}};
-\node (F1-5) at (0,0)  {\large \LangPVecAlloc{}};
+\node (Lgradual) at (9,4)  {\large \LangGrad{}};
+\node (Lgradualp) at (6,4)  {\large \LangCast{}};
+\node (Llambdapp) at (3,4)  {\large \LangProxy{}};
+\node (Llambdaproxy) at (0,4)  {\large \LangPVec{}};
+\node (Llambdaproxy-2) at (0,2)  {\large \LangPVec{}};
+\node (Llambdaproxy-3) at (3,2)  {\large \LangPVec{}};
+\node (Llambdaproxy-4) at (6,2)  {\large \LangPVecFunRef{}};
+\node (Llambdaproxy-5) at (9,2)  {\large \LangPVecFunRef{}};
+\node (F1-1) at (12,2)  {\large \LangPVecFunRef{}};
+\node (F1-2) at (12,0)  {\large \LangPVecFunRef{}};
+\node (F1-3) at (9,0)  {\large \LangPVecFunRef{}};
+\node (F1-4) at (6,0)  {\large \LangPVecAlloc{}};
+\node (F1-5) at (3,0)  {\large \LangPVecAlloc{}};
+\node (F1-6) at (0,0)  {\large \LangPVecAlloc{}};
 \node (C3-2) at (3,-2)  {\large \LangCLoopPVec{}};
 
 \node (x86-2) at (3,-4)  {\large \LangXIndCallVar{}};
@@ -19358,31 +19367,33 @@ be translated in a similar way.
 \node (x86-5) at (9,-6) {\large \LangXIndCall{}};
 
 
-\path[->,bend right=15] (Rgradual) edge [above] node
-     {\ttfamily\footnotesize type\_check} (Rgradualp);
-\path[->,bend right=15] (Rgradualp) edge [above] node
-     {\ttfamily\footnotesize lower\_casts} (Lwhilepp);
-\path[->,bend right=15] (Lwhilepp) edge [right] node
-     {\ttfamily\footnotesize differentiate\_proxies} (Lwhileproxy);
-\path[->,bend left=15] (Lwhileproxy) edge [above] node
-     {\ttfamily\footnotesize shrink} (Lwhileproxy-2);
-\path[->,bend left=15] (Lwhileproxy-2) edge [above] node
-     {\ttfamily\footnotesize uniquify} (Lwhileproxy-3);
-\path[->,bend left=15] (Lwhileproxy-3) edge [above] node
-     {\ttfamily\footnotesize reveal\_functions} (Lwhileproxy-4);
-\path[->,bend left=15] (Lwhileproxy-4) edge [above] node
-     {\ttfamily\footnotesize reveal\_casts} (Lwhileproxy-5);
-\path[->,bend left=15] (Lwhileproxy-5) edge [left] node
+\path[->,bend right=15] (Lgradual) edge [above] node
+     {\ttfamily\footnotesize type\_check} (Lgradualp);
+\path[->,bend right=15] (Lgradualp) edge [above] node
+     {\ttfamily\footnotesize lower\_casts} (Llambdapp);
+\path[->,bend right=15] (Llambdapp) edge [above] node
+     {\ttfamily\footnotesize differentiate.} (Llambdaproxy);
+\path[->,bend left=15] (Llambdaproxy) edge [right] node
+     {\ttfamily\footnotesize shrink} (Llambdaproxy-2);
+\path[->,bend left=15] (Llambdaproxy-2) edge [above] node
+     {\ttfamily\footnotesize uniquify} (Llambdaproxy-3);
+\path[->,bend left=15] (Llambdaproxy-3) edge [above] node
+     {\ttfamily\footnotesize reveal\_functions} (Llambdaproxy-4);
+\path[->,bend left=15] (Llambdaproxy-4) edge [above] node
+     {\ttfamily\footnotesize reveal\_casts} (Llambdaproxy-5);
+\path[->,bend left=15] (Llambdaproxy-5) edge [above] node
      {\ttfamily\footnotesize convert\_assignments} (F1-1);
-\path[->,bend left=15] (F1-1) edge [below] node
+\path[->,bend left=15] (F1-1) edge [left] node
      {\ttfamily\footnotesize convert\_to\_clos.} (F1-2);
-\path[->,bend right=15] (F1-2) edge [above] node
+\path[->,bend left=15] (F1-2) edge [below] node
      {\ttfamily\footnotesize limit\_fun.} (F1-3);
 \path[->,bend right=15] (F1-3) edge [above] node
      {\ttfamily\footnotesize expose\_alloc.} (F1-4);
 \path[->,bend right=15] (F1-4) edge [above] node
-     {\ttfamily\footnotesize remove\_complex.} (F1-5);
-\path[->,bend right=15] (F1-5) edge [right] node
+     {\ttfamily\footnotesize uncover\_get!} (F1-5);
+\path[->,bend right=15] (F1-5) edge [above] node
+     {\ttfamily\footnotesize remove\_complex.} (F1-6);
+\path[->,bend right=15] (F1-6) edge [right] node
      {\ttfamily\footnotesize explicate\_control} (C3-2);
 \path[->,bend left=15] (C3-2) edge [left] node
      {\ttfamily\footnotesize select\_instr.} (x86-2);
@@ -19394,14 +19405,14 @@ be translated in a similar way.
      {\ttfamily\footnotesize allocate\_reg.} (x86-3);
 \path[->,bend left=15] (x86-3) edge [above] node
      {\ttfamily\footnotesize patch\_instr.} (x86-4);
-\path[->,bend left=15] (x86-4) edge [right] node {\ttfamily\footnotesize print-x86} (x86-5);
+\path[->,bend left=15] (x86-4) edge [right] node {\ttfamily\footnotesize prelude\_and\_conc.} (x86-5);
 \end{tikzpicture}
   \caption{Diagram of the passes for \LangGrad{} (gradual typing).}
-\label{fig:Rgradual-passes}
+\label{fig:Lgradual-passes}
 \end{figure}
 
-Figure~\ref{fig:Rgradual-passes} provides an overview of all the passes needed
-for the compilation of \LangGrad{}.
+Figure~\ref{fig:Lgradual-passes} provides an overview of the passes
+needed for the compilation of \LangGrad{}.
 
 \section{Further Reading}
 
@@ -19419,13 +19430,13 @@ original location of the cast in the source program.
 
 The problem addressed by space-efficient casts also relates to
 higher-order casts. It turns out that in partially typed programs, a
-function or vector can flow through very-many casts at runtime. With
+function or tuple can flow through very-many casts at runtime. With
 the approach described in this chapter, each cast adds another
-\code{lambda} wrapper or a vector proxy. Not only does this take up
-considerable space, but it also makes the function calls and vector
+\code{lambda} wrapper or a tuple proxy. Not only does this take up
+considerable space, but it also makes the function calls and tuple
 operations slow.  For example, a partially-typed version of quicksort
 could, in the worst case, build a chain of proxies of length $O(n)$
-around the vector, changing the overall time complexity of the
+around the tuple, changing the overall time complexity of the
 algorithm from $O(n^2)$ to $O(n^3)$! \citet{Herman:2006uq} suggested a
 solution to this problem by representing casts using the coercion
 calculus of \citet{Henglein:1994nz}, which prevents the creation of
@@ -19473,7 +19484,7 @@ parameterizing functions and data structures with respect to the types
 that they operate on. For example, Figure~\ref{fig:map-poly}
 revisits the \code{map} example but this time gives it a more
 fitting type.  This \code{map} function is parameterized with
-respect to the element type of the vector. The type of \code{map}
+respect to the element type of the tuple. The type of \code{map}
 is the following polymorphic type as specified by the \code{All} and
 the type parameter \code{a}.
 \begin{lstlisting}
@@ -19481,9 +19492,9 @@ the type parameter \code{a}.
 \end{lstlisting}
 The idea is that \code{map} can be used at \emph{all} choices of a
 type for parameter \code{a}. In Figure~\ref{fig:map-poly} we apply
-\code{map} to a vector of integers, a choice of \code{Integer} for
+\code{map} to a tuple of integers, a choice of \code{Integer} for
 \code{a}, but we could have just as well applied \code{map} to a
-vector of Booleans (and a function on Booleans).
+tuple of Booleans (and a function on Booleans).
 
 \begin{figure}[tbp]
   % poly_test_2.rkt
@@ -19528,8 +19539,8 @@ polymorphic types and type variables.
 \]
 \end{minipage}
 }
-\caption{The concrete syntax of \LangPoly{}, extending \LangLoop{}
-    (Figure~\ref{fig:Lwhile-concrete-syntax}).}
+\caption{The concrete syntax of \LangPoly{}, extending \LangLam{}
+    (Figure~\ref{fig:Llambda-concrete-syntax}).}
 \label{fig:Rpoly-concrete-syntax}
 \end{figure}
 
@@ -19549,8 +19560,8 @@ polymorphic types and type variables.
 \]
 \end{minipage}
 }
-\caption{The abstract syntax of \LangPoly{}, extending \LangLoop{}
-    (Figure~\ref{fig:Lwhile-syntax}).}
+\caption{The abstract syntax of \LangPoly{}, extending \LangLam{}
+    (Figure~\ref{fig:Llambda-syntax}).}
 \label{fig:Rpoly-syntax}
 \end{figure}
 
@@ -19583,7 +19594,7 @@ applies the polymorphic function to a Boolean and to an integer.
 \end{figure}
 
 The type checker for \LangPoly{} in Figure~\ref{fig:type-check-Lvar0} has
-three new responsibilities (compared to \LangLoop{}). The type checking of
+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
@@ -19610,7 +19621,7 @@ deduced type arguments, using the \code{subst-type} function.
 The second responsibility of the type checker is extending the
 function \code{type-equal?} to handle the \code{All} type.  This is
 not quite a simple as equal on other types, such as function and
-vector types, because two polymorphic types can be syntactically
+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
@@ -19647,8 +19658,8 @@ process in next pass of the compiler.
 \]
 \end{minipage}
 }
-\caption{The abstract syntax of \LangInst{}, extending \LangLoop{}
-    (Figure~\ref{fig:Lwhile-syntax}).}
+\caption{The abstract syntax of \LangInst{}, extending \LangLam{}
+    (Figure~\ref{fig:Llambda-syntax}).}
 \label{fig:Rpoly-prime-syntax}
 \end{figure}
 
@@ -19674,7 +19685,7 @@ example is listed in Figure~\ref{fig:map-type-check}.
 \begin{figure}[tbp]
 \begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
 (define type-check-poly-class
-  (class type-check-Lwhile-class
+  (class type-check-Llambda-class
     (super-new)
     (inherit check-type-equal?)
   
@@ -19876,7 +19887,7 @@ polymorphism, which we describe below.
   
 \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 \LangLoop{})
+  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
   and called). This approach is compatible with separate compilation
@@ -20014,13 +20025,13 @@ annotations and the body.
 \begin{tikzpicture}[baseline=(current  bounding  box.center)]
 \node (Rpoly) at (9,4)  {\large \LangPoly{}};
 \node (Rpolyp) at (6,4)  {\large \LangInst{}};
-\node (Rgradualp) at (3,4)  {\large \LangCast{}};
-\node (Lwhilepp) at (0,4)  {\large \LangProxy{}};
-\node (Lwhileproxy) at (0,2)  {\large \LangPVec{}};
-\node (Lwhileproxy-2) at (3,2)  {\large \LangPVec{}};
-\node (Lwhileproxy-3) at (6,2)  {\large \LangPVec{}};
-\node (Lwhileproxy-4) at (9,2)  {\large \LangPVecFunRef{}};
-\node (Lwhileproxy-5) at (12,2)  {\large \LangPVecFunRef{}};
+\node (Lgradualp) at (3,4)  {\large \LangCast{}};
+\node (Llambdapp) at (0,4)  {\large \LangProxy{}};
+\node (Llambdaproxy) at (0,2)  {\large \LangPVec{}};
+\node (Llambdaproxy-2) at (3,2)  {\large \LangPVec{}};
+\node (Llambdaproxy-3) at (6,2)  {\large \LangPVec{}};
+\node (Llambdaproxy-4) at (9,2)  {\large \LangPVecFunRef{}};
+\node (Llambdaproxy-5) at (12,2)  {\large \LangPVecFunRef{}};
 \node (F1-1) at (12,0)  {\large \LangPVecFunRef{}};
 \node (F1-2) at (9,0)  {\large \LangPVecFunRef{}};
 \node (F1-3) at (6,0)  {\large \LangPVecFunRef{}};
@@ -20039,20 +20050,20 @@ annotations and the body.
 \path[->,bend right=15] (Rpoly) edge [above] node
      {\ttfamily\footnotesize type\_check} (Rpolyp);
 \path[->,bend right=15] (Rpolyp) edge [above] node
-     {\ttfamily\footnotesize erase\_types} (Rgradualp);
-\path[->,bend right=15] (Rgradualp) edge [above] node
-     {\ttfamily\footnotesize lower\_casts} (Lwhilepp);
-\path[->,bend right=15] (Lwhilepp) edge [right] node
-     {\ttfamily\footnotesize differentiate\_proxies} (Lwhileproxy);
-\path[->,bend left=15] (Lwhileproxy) edge [above] node
-     {\ttfamily\footnotesize shrink} (Lwhileproxy-2);
-\path[->,bend left=15] (Lwhileproxy-2) edge [above] node
-     {\ttfamily\footnotesize uniquify} (Lwhileproxy-3);
-\path[->,bend left=15] (Lwhileproxy-3) edge [above] node
-     {\ttfamily\footnotesize reveal\_functions} (Lwhileproxy-4);
-\path[->,bend left=15] (Lwhileproxy-4) edge [above] node
-     {\ttfamily\footnotesize reveal\_casts} (Lwhileproxy-5);
-\path[->,bend left=15] (Lwhileproxy-5) edge [left] node
+     {\ttfamily\footnotesize erase\_types} (Lgradualp);
+\path[->,bend right=15] (Lgradualp) edge [above] node
+     {\ttfamily\footnotesize lower\_casts} (Llambdapp);
+\path[->,bend right=15] (Llambdapp) edge [right] node
+     {\ttfamily\footnotesize differentiate\_proxies} (Llambdaproxy);
+\path[->,bend left=15] (Llambdaproxy) edge [above] node
+     {\ttfamily\footnotesize shrink} (Llambdaproxy-2);
+\path[->,bend left=15] (Llambdaproxy-2) edge [above] node
+     {\ttfamily\footnotesize uniquify} (Llambdaproxy-3);
+\path[->,bend left=15] (Llambdaproxy-3) edge [above] node
+     {\ttfamily\footnotesize reveal\_functions} (Llambdaproxy-4);
+\path[->,bend left=15] (Llambdaproxy-4) edge [above] node
+     {\ttfamily\footnotesize reveal\_casts} (Llambdaproxy-5);
+\path[->,bend left=15] (Llambdaproxy-5) edge [left] node
      {\ttfamily\footnotesize convert\_assignments} (F1-1);
 \path[->,bend left=15] (F1-1) edge [below] node
      {\ttfamily\footnotesize convert\_to\_clos.} (F1-2);

defs.tex

@@ -67,9 +67,9 @@
 \newcommand{\LangArray}{\ensuremath{\Lang^{\mathsf{Array}}_{\mathsf{While}}}} %\Lang^s3
 \newcommand{\LangGrad}{$\Lang_{\mathsf{?}}$} %R9
 \newcommand{\LangGradM}{\Lang_{\mathsf{?}}} %R9
-\newcommand{\LangCast}{$\Lang_{\mathsf{cast}}$} %R9'
-\newcommand{\LangCastM}{\Lang_{\mathsf{cast}}} %R9'
-\newcommand{\LangProxy}{\ensuremath{\Lang_{\mathsf{proxy}}}} %R8''
+\newcommand{\LangCast}{$\Lang_{\mathsf{Cast}}$} %R9'
+\newcommand{\LangCastM}{\Lang_{\mathsf{Cast}}} %R9'
+\newcommand{\LangProxy}{\ensuremath{\Lang_{\mathsf{Proxy}}}} %R8''
 \newcommand{\LangPVec}{\ensuremath{\Lang_{\mathsf{PVec}}}} %R8''
 \newcommand{\LangPVecFunRef}{\ensuremath{\Lang^{\mathsf{FunRef}}_{\mathsf{PVec}}}} %R8''
 \newcommand{\LangPVecAlloc}{\ensuremath{\Lang^{\mathsf{Alloc}}_{\mathsf{PVec}}}} %R8''