@@ -14,7 +14,7 @@ of any study in this sense. We study it for the formalism of Section~\ref{sec:la
In a sense, occurrence typing is a
discipline designed to push forward the frontiers beyond which gradual
typing is needed, thus reducing the amount of runtime checks needed. For
instance, the the JavaScript code of~\eqref{foo} and~\eqref{foo2} in the introduction can be
instance, the JavaScript code of~\eqref{foo} and~\eqref{foo2} in the introduction can also be
typed by using gradual typing:\vspace{-.4mm}
\begin{alltt}\color{darkblue}\morecompact
function foo(x\textcolor{darkred}{ : \pmb{\dyn}}) \{
...
...
@@ -32,11 +32,11 @@ where {\Cast{$t$}{$e$}} is a type-cast that dynamically checks whether the value
error")}. Not exactly though, since to implement compilation \emph{à la} sound gradual typing it is necessary to use casts on function types that need special handling.}
%
We already saw that thanks to occurrence typing we can annotate the parameter \code{x} by \code{number|string} instead of \dyn{} and avoid the insertion of any cast.
But occurrence typing can be used also on the gradually typed code in order to statically detect the insertion of useless casts. Using
But occurrence typing can be used also on the gradually typed code above in order to statically detect the insertion of useless casts. Using
occurrence typing to type the gradually-typed version of \code{foo} in~\eqref{foo3}, allows the system to avoid inserting the first cast
\code{\Cast{number}{x}} since, thanks to occurrence typing, the
occurrence of \code{x} at issue is given type \code{number} (the
second cast is still necessary however). But removing only this cast is far
occurrence of \code{x} at issue is given type \code{number} (but the
second cast is still necessary though). But removing only this cast is far
from being satisfactory, since when this function is applied to an integer
there are some casts that still need to be inserted outside the function.
The reason is that the compiled version of the function