|
@@ -13115,10 +13115,12 @@ class TypeCheckLarray(TypeCheckLtup):
|
|
|
self.check_type_equal(index_ty, IntType(), index)
|
|
|
match tup_t:
|
|
|
case ListType(ty):
|
|
|
- self.check_type_equal(ty, value_t, ss[0])
|
|
|
+ self.check_type_equal(ty, value_t, ss[0])
|
|
|
+ case TupleType(ts):
|
|
|
+ return self.type_check_stmts(ss, env)
|
|
|
case _:
|
|
|
- raise Exception('type_check_stmts: expected a list, not ' \
|
|
|
- + repr(tup_t))
|
|
|
+ raise Exception('type_check_stmts: '
|
|
|
+ 'expected tuple or list, not ' + repr(tup_t))
|
|
|
return self.type_check_stmts(ss[1:], env)
|
|
|
case _:
|
|
|
return super().type_check_stmts(ss, env)
|
|
@@ -13206,10 +13208,10 @@ However, we limit tuples to a length of $50$ so that their length and
|
|
|
pointer mask can fit into the 64-bit tag at the beginning of each
|
|
|
tuple (Section~\ref{sec:data-rep-gc}). We intend arrays to allow
|
|
|
millions of elements, so we need more bits to store the length.
|
|
|
-However, because arrays are homogeneous, we only need $1$ bit for the
|
|
|
-pointer mask instead of one bit per array elements. Finally, the
|
|
|
-garbage collector will need to be able to distinguish between tuples
|
|
|
-and arrays, so we need to reserve $1$ bit for that purpose. So we
|
|
|
+However, because arrays are homogeneous, we only need one bit for the
|
|
|
+pointer mask instead of one bit per array element. Finally, the
|
|
|
+garbage collector must be able to distinguish between tuples
|
|
|
+and arrays, so we need to reserve one bit for that purpose. We
|
|
|
arrive at the following layout for the 64-bit tag at the beginning of
|
|
|
an array:
|
|
|
\begin{itemize}
|
|
@@ -13311,8 +13313,9 @@ operations. In particular, the new AST node \ALLOCARRAY{\Exp}{\Type}
|
|
|
is analogous to the \code{Allocate} AST node for tuples. The $\Type$
|
|
|
argument must be \ARRAYTY{T} where $T$ is the element type for the
|
|
|
array. The \code{AllocateArray} AST node allocates an array of the
|
|
|
-length specified by the $\Exp$ but does not initialize the elements of
|
|
|
-the array. Generate code in this pass to initialize the elements.
|
|
|
+length specified by the $\Exp$ (of type \INTTY), but does not initialize the elements of
|
|
|
+the array. Generate code in this pass to initialize the elements
|
|
|
+analogous to the case for tuples.
|
|
|
|
|
|
\subsection{Remove Complex Operands}
|
|
|
|
|
@@ -18743,6 +18746,7 @@ movq 0(%r11) |$\itm{lhs'}$|
|
|
|
\fi}
|
|
|
\end{minipage}
|
|
|
\end{center}
|
|
|
+% $ pacify font lock
|
|
|
|
|
|
%% \paragraph{\racket{\code{any-vector-set!}}\python{\code{any\_tuple\_store}}}
|
|
|
|
|
@@ -18909,7 +18913,7 @@ 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 that type annotations
|
|
|
-optional, which is specified in the grammar using the \Param{} and
|
|
|
+are optional, which is specified in the grammar using the \Param{} and
|
|
|
\itm{ret} non-terminals. In the abstract syntax, type annotations are
|
|
|
not optional but we use the \CANYTY{} type when a type annotation is
|
|
|
absent.
|
|
@@ -19084,7 +19088,7 @@ tuple. The \code{inc} function has type
|
|
|
\racket{\code{(Any -> Any)}}\python{\code{Callable[[Any],Any]}}
|
|
|
but parameter \code{f} of \code{map} has type
|
|
|
\racket{\code{(Integer -> Integer)}}\python{\code{Callable[[int],int]}}.
|
|
|
-The type checker for \LangGrad{} allows this because the two types are
|
|
|
+The type checker for \LangGrad{} accepts this call because the two types are
|
|
|
consistent.
|
|
|
|
|
|
\begin{figure}[btp]
|
|
@@ -19149,10 +19153,9 @@ print(t[1])
|
|
|
case (_, AnyType()):
|
|
|
return True
|
|
|
case (FunctionType(ps1, rt1), FunctionType(ps2, rt2)):
|
|
|
- return all([self.consistent(p1, p2) for (p1,p2) in zip(ps1,ps2)]) \
|
|
|
- and consistent(rt1, rt2)
|
|
|
+ return all(map(self.consistent, ps1, ps2)) and consistent(rt1, rt2)
|
|
|
case (TupleType(ts1), TupleType(ts2)):
|
|
|
- return all([self.consistent(ty1, ty2) for (ty1,ty2) in zip(ts1,ts2)])
|
|
|
+ return all(map(self.consistent, ts1, ts2))
|
|
|
case (_, _):
|
|
|
return t1 == t2
|
|
|
\end{lstlisting}
|
|
@@ -19311,11 +19314,11 @@ print(t[1])
|
|
|
\begin{tcolorbox}[colback=white]
|
|
|
\begin{lstlisting}[basicstyle=\ttfamily\footnotesize]
|
|
|
class TypeCheckLgrad(TypeCheckLlambda):
|
|
|
- def type_check_exp(self, e, env):
|
|
|
+ def type_check_exp(self, e, env) -> Type:
|
|
|
match e:
|
|
|
case Name(id):
|
|
|
return env[id]
|
|
|
- case Constant(value) if value is True or value is False:
|
|
|
+ case Constant(value) if isinstance(value, bool):
|
|
|
return BoolType()
|
|
|
case Constant(value) if isinstance(value, int):
|
|
|
return IntType()
|
|
@@ -19336,9 +19339,9 @@ class TypeCheckLgrad(TypeCheckLlambda):
|
|
|
return self.join_types(body_t, orelse_t)
|
|
|
case Call(func, args):
|
|
|
func_t = self.type_check_exp(func, env)
|
|
|
- args_t = unzip([self.type_check_exp(arg, env) for arg in args])
|
|
|
+ args_t = [self.type_check_exp(arg, env) for arg in args]
|
|
|
match func_t:
|
|
|
- case FunctionType(params_t, return_t):
|
|
|
+ case FunctionType(params_t, return_t) if len(params_t) == len(args_t):
|
|
|
for (arg_t, param_t) in zip(args_t, params_t):
|
|
|
self.check_consistent(param_t, arg_t, e)
|
|
|
return return_t
|
|
@@ -19364,15 +19367,14 @@ class TypeCheckLgrad(TypeCheckLlambda):
|
|
|
case Lambda(params, body):
|
|
|
match expected_ty:
|
|
|
case FunctionType(params_t, return_t):
|
|
|
- new_env = {x:t for (x,t) in env.items()}
|
|
|
- for (p,t) in zip(new_params, params_t):
|
|
|
- new_env[p] = t
|
|
|
+ new_env = env.copy().update(zip(params, params_t))
|
|
|
e.has_type = expected_ty
|
|
|
+ body_ty = self.type_check_exp(body, new_env)
|
|
|
+ self.check_consistent(body_ty, return_t)
|
|
|
case AnyType():
|
|
|
- new_env = {x:t for (x,t) in env.items()}
|
|
|
- for p in new_params:
|
|
|
- new_env[p] = AnyType()
|
|
|
- e.has_type = FunctionType([AnyType() for _ in new_params], AnyType())
|
|
|
+ new_env = env.copy().update((p, AnyType()) for p in params)
|
|
|
+ e.has_type = FunctionType([AnyType() for _ in params], AnyType())
|
|
|
+ body_ty = self.type_check_exp(body, new_env)
|
|
|
case _:
|
|
|
raise Exception('lambda does not have type ' + str(expected_ty))
|
|
|
case _:
|
|
@@ -19394,7 +19396,7 @@ class TypeCheckLgrad(TypeCheckLlambda):
|
|
|
if id in env:
|
|
|
self.check_consistent(env[id], value_ty, value)
|
|
|
else:
|
|
|
- env[id] = t
|
|
|
+ env[id] = value_ty
|
|
|
...
|
|
|
case _:
|
|
|
raise Exception('type_check_stmts: unexpected ' + repr(ss))
|
|
@@ -19418,10 +19420,10 @@ class TypeCheckLgrad(TypeCheckLlambda):
|
|
|
case (_, AnyType()):
|
|
|
return t1
|
|
|
case (FunctionType(ps1, rt1), FunctionType(ps2, rt2)):
|
|
|
- return FunctionType([self.join_types(p1, p2) for (p1,p2) in zip(ps1, ps2)],
|
|
|
- self.join_types(rt1,rt2))
|
|
|
+ return FunctionType(list(map(self.join_types, ps1, ps2)),
|
|
|
+ self.join_types(rt1,rt2))
|
|
|
case (TupleType(ts1), TupleType(ts2)):
|
|
|
- return TupleType([self.join_types(ty1, ty2) for (ty1,ty2) in zip(ts1,ts2)])
|
|
|
+ return TupleType(list(map(self.join_types, ts1, ts2)))
|
|
|
case (_, _):
|
|
|
return t1
|
|
|
|
|
@@ -19698,11 +19700,11 @@ cast from \INTTY{} to \CANYTY{} can be accomplished with the
|
|
|
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
|
|
|
+the underlying integer or signalling an error if the tag is not the
|
|
|
one for integers (Figure~\ref{fig:interp-Lany-aux}).
|
|
|
%
|
|
|
-Things get more interesting casts involving function, tuple, or array
|
|
|
-types, that is, casts involving higher-order types.
|
|
|
+Things get more interesting for casts involving function, tuple, or array
|
|
|
+types.
|
|
|
|
|
|
Consider the cast of the function \code{maybe\_inc} from
|
|
|
\racket{\code{(Any -> Any)}}\python{\code{Callable[[Any], Any]}}
|
|
@@ -19713,8 +19715,8 @@ When the \code{maybe\_inc} function flows through
|
|
|
this cast at runtime, we don't know whether it will return
|
|
|
an integer, as that depends on the input from the user.
|
|
|
The \LangCast{} interpreter therefore delays the checking
|
|
|
-of the cast until the function is applied. This is accomplished by
|
|
|
-wrapping \code{maybe\_inc} in a new function that casts its parameter
|
|
|
+of the cast until the function is applied. To do so it
|
|
|
+wraps \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 \INTTY{}.
|
|
|
|
|
@@ -19808,7 +19810,7 @@ from \CANYTY{} to \INTTY{}.
|
|
|
For the subscript \code{v[i]} in \code{f([v[i])} of \code{map\_inplace},
|
|
|
the proxy casts the integer from \INTTY{} to \CANYTY{}.
|
|
|
For the subscript on the left of the assignment,
|
|
|
- the proxy casts the tagged value from from \CANYTY{} to \INTTY{}.
|
|
|
+ the proxy casts the tagged value from \CANYTY{} to \INTTY{}.
|
|
|
}
|
|
|
|
|
|
The final category of cast that we need to consider are casts between
|
|
@@ -19941,7 +19943,7 @@ print( v[1] )
|
|
|
case (FunctionType(ps1, rt1), FunctionType(ps2, rt2)):
|
|
|
params = [generate_name('x') for p in ps2]
|
|
|
args = [Cast(Name(x), t2, t1)
|
|
|
- for (x,(t1,t2)) in zip(params, zip(ps1, ps2))]
|
|
|
+ for (x,t1,t2) in zip(params, ps1, ps2)]
|
|
|
body = Cast(Call(ValueExp(value), args), rt1, rt2)
|
|
|
return Function('cast', params, [Return(body)], {})
|
|
|
case (TupleType(ts1), TupleType(ts2)):
|
|
@@ -20120,30 +20122,30 @@ The \code{cast\_insert} pass is closely related to the type checker
|
|
|
for \LangGrad{} (starting in Figure~\ref{fig:type-check-Lgradual-1}).
|
|
|
In particular, the type checker allows implicit casts between
|
|
|
consistent types. The job of the \code{cast\_insert} pass is to make
|
|
|
-those into explicit casts. This is accomplished by inserting
|
|
|
+those casts explicit. It does so by inserting
|
|
|
\code{Cast} nodes into the AST.
|
|
|
%
|
|
|
For the most part, the implicit casts occur in places where the type
|
|
|
-checker checks two types for consistenty. Consider the case for
|
|
|
+checker checks two types for consistency. Consider the case for
|
|
|
binary operators in Figure~\ref{fig:type-check-Lgradual-1}. The type
|
|
|
checker requires that the type of the left operand is consistent with
|
|
|
\INTTY{}. Thus, the \code{cast\_insert} pass should insert a
|
|
|
\code{Cast} around the left operand, converting from its type to
|
|
|
-\INTTY{}. The story is similar for the right operand. Note that a cast
|
|
|
-is not always necessary, e.g., if the left operand already has type
|
|
|
-\INTTY{} then there is no need to insert a \code{Cast}.
|
|
|
+\INTTY{}. The story is similar for the right operand. It is not always
|
|
|
+necessary to insert a cast, e.g., if the left operand already has type
|
|
|
+\INTTY{} then there is no need for a \code{Cast}.
|
|
|
|
|
|
-Some of the implicit casts are not as straightforward, such as the
|
|
|
+Some of the implicit casts are not as straightforward. One such case
|
|
|
+arises with the
|
|
|
conditional expression. In Figure~\ref{fig:type-check-Lgradual-1} we
|
|
|
see that the type checker requires that the two branches have
|
|
|
consistent types and that type of the conditional expression is the
|
|
|
-join of the branches' types. In the target language \LangCast{}, the
|
|
|
-branches will need to have the same type as each other, and that type
|
|
|
-will be the type of the conditional expression. Thus, one must insert
|
|
|
-a \code{Cast} around each branch to convert from its type to the join
|
|
|
-type.
|
|
|
+join of the branches' types. In the target language \LangCast{}, both
|
|
|
+branches will need to have the same type, and that type
|
|
|
+will be the type of the conditional expression. Thus, each branch requires
|
|
|
+a \code{Cast} to convert from its type to the join type.
|
|
|
|
|
|
-The case for function call exhibits another interesting situation. If
|
|
|
+The case for the function call exhibits another interesting situation. If
|
|
|
the function expression is of type \CANYTY{}, then it needs to be cast
|
|
|
to a function type so that it can be used in a function call in
|
|
|
\LangCast{}. Which function type should it be cast to? The parameter
|
|
@@ -20161,7 +20163,7 @@ to type \CANYTY{} (if they are not already of that type).
|
|
|
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 new operators for
|
|
|
-proxies, extending the \LangLam{} language to create \LangProxy{}.
|
|
|
+proxies, extending the \LangLam{} language to \LangProxy{}.
|
|
|
The \LangProxy{} language can also be described as an extension of
|
|
|
\LangAny{}, with the addition of proxies. We recommend creating an
|
|
|
auxiliary function named \code{lower\_cast} that takes an expression
|
|
@@ -20173,7 +20175,7 @@ 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 involing tuple, array, and function types.
|
|
|
+the casts involving tuple, array, and function types.
|
|
|
|
|
|
As mentioned in Section~\ref{sec:interp-casts}, a cast from one array
|
|
|
type to another array type is accomplished by creating a proxy that
|
|
@@ -20337,7 +20339,7 @@ Likewise, we return the
|
|
|
meaning, as the type of arrays, and we introduce a new type,
|
|
|
\PARRAYTYNAME{}, whose values
|
|
|
can be either arrays or array proxies.
|
|
|
-These new types come with a suite of new primitive operations
|
|
|
+These new types come with a suite of new primitive operations.
|
|
|
|
|
|
{\if\edition\racketEd
|
|
|
A tuple proxy is represented by a tuple containing three things: 1) the
|
|
@@ -20465,12 +20467,12 @@ and primitive functions.
|
|
|
|
|
|
\fi}
|
|
|
|
|
|
-Now to discuss the translation that differentiates tuples and arrays
|
|
|
+Now we discuss the translation that differentiates tuples and arrays
|
|
|
from proxies. First, every type annotation in the program is
|
|
|
translated (recursively) to replace \TUPLETYPENAME{} with \PTUPLETYNAME{}.
|
|
|
Next, we insert uses of \PTUPLETYNAME{} operations in the appropriate
|
|
|
places. For example, we wrap every tuple creation with an
|
|
|
-\racket{\code{inject-vector}}\python{\code{InjectTupleProxy}}.
|
|
|
+\racket{\code{inject-vector}}\python{\code{InjectTuple}}.
|
|
|
{\if\edition\racketEd
|
|
|
\begin{lstlisting}
|
|
|
(vector |$e_1 \ldots e_n$|)
|
|
@@ -20535,7 +20537,7 @@ operation.
|
|
|
\fi}
|
|
|
%
|
|
|
Note that in the branch for a tuple, we must apply
|
|
|
-\racket{\code{project-vector}} \python{project\_tuple} before reading
|
|
|
+\racket{\code{project-vector}}\python{\code{project\_tuple}} before reading
|
|
|
from the tuple.
|
|
|
|
|
|
The translation of array operations is similar to the ones for tuples.
|
|
@@ -20612,7 +20614,7 @@ Assign([|$\itm{lhs}$|], InjectTuple(|$e_1$|))
|
|
|
movq |$e'_1$|, |$\itm{lhs'}$|
|
|
|
\end{lstlisting}
|
|
|
\fi}
|
|
|
-\python{The translation for \code{InjectList} is just a move instruction.}
|
|
|
+\python{The translation for \code{InjectList} is also a move instruction.}
|
|
|
\noindent On the other hand,
|
|
|
\racket{\code{inject-proxy}}\python{\code{InjectTupleProxy}} sets bit
|
|
|
$63$ to $1$.
|
|
@@ -20675,7 +20677,7 @@ movq %rax, |$\itm{lhs'}$|
|
|
|
%
|
|
|
The \racket{\code{project-vector} operation is}
|
|
|
\python{\code{project\_tuple} and \code{project\_array} operations are}
|
|
|
-straightforward to translate, so we leave that up to the reader.
|
|
|
+straightforward to translate, so we leave that to the reader.
|
|
|
|
|
|
Regarding the element access operations for tuples and arrays, the
|
|
|
runtime provides procedures that implement them (they are recursive
|
|
@@ -20769,7 +20771,7 @@ and \code{proxy\_vec\_length} functions.
|
|
|
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 \LangLam{}
|
|
|
- and tests for \LangDyn{}.
|
|
|
+ and for \LangDyn{}.
|
|
|
%
|
|
|
\racket{Sometimes you may get a type checking error on the
|
|
|
\LangDyn{} programs but you can adapt them by inserting a cast to
|
|
@@ -20879,7 +20881,7 @@ 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 tuple 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 tuple proxy. Not only does this take up
|
|
|
considerable space, but it also makes the function calls and tuple
|
|
@@ -20890,7 +20892,7 @@ 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
|
|
|
long chains of proxies by compressing them into a concise normal
|
|
|
-form. \citet{Siek:2015ab} give and algorithm for compressing coercions
|
|
|
+form. \citet{Siek:2015ab} give an algorithm for compressing coercions
|
|
|
and \citet{Kuhlenschmidt:2019aa} show how to implement these ideas in
|
|
|
the Grift compiler.
|
|
|
\begin{center}
|
|
@@ -20900,7 +20902,8 @@ the Grift compiler.
|
|
|
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 the online gradual typing bibliography:
|
|
|
+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}
|