Commit d36f7214 authored by Victor Lanvin's avatar Victor Lanvin
Browse files

Work on gradual part

parent ae31184f
......@@ -212,122 +212,8 @@ Finally, we add the following typing rules:
\subsection{Refining function types}
\input{refining}
\subsection{Integrating gradual typing}
Occurrence typing and gradual typing are two complementary disciplines
which have a lot to gain to be integrated, although we are not aware
of any work in this sense. In a sense occurrence typing is a
discipline designed to push forward the frontiers beyond which gradual
typing is needed. For instance, the example at the beginning can be
typed by using gradual typing:
\begin{alltt}\color{darkblue}
function foo(x\textcolor{darkred}{ : ?}) \{
(typeof(x) === "number")? x++ : x.length
\}
\end{alltt}
Using ``standard'' gradual typing this is compiled into:
\begin{alltt}\color{darkblue}
function foo(x) \{
(typeof(x) === "number")? (\Cast{number}{x})++ : (\Cast{string}{x}).length
\}
\end{alltt}
where {\Cast{$t$}{$e$}} is a type-cast.\footnote{Intuitively, \code{\Cast{$t$}{$e$}} is
syntactic sugar for \code{(typeof($e$)==="$t$")? $e$ : (throw "Type
error")}. Not exactly though, since to implement compilation \emph{à la} sound gradual typing we need cast on function types.}
%
We have already seen in the introduction that by using occurrence
typing combined with a union type instead of the gradual type \code{?}
for parameter annotation, we can avoid the insertion of any cast. But
occurrence typing can be used also on the gradually typed code. If we use
occurrence typing in typing the gradually-typed version of the code of \code{foo} this
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 instead). But removing 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 applied at the
application. The reason is that the compiled version of the function
has type \code{?$\to$number}, it therefore expects an argument of type
\code{?}, and thus we have to apply a cast (either to the argument or
to the function) whenever this is not the case. In particular, the
application \code{foo(42)} will be compiled as
\code{foo(\Cast{?}{42})}. Now the main problem with such a cast is not
that it produces some unnecessary overhead by performing useless
checks. The main problem is that the presence of such a cast either
requires to complexify the operational semantics of type-cases or it
leads to unintuitive results. Indeed, consider the standard semantics
of the type case \code{(typeof($e$)==="$t$")} which consists in
reducing $e$ to a value and checking whether the type of the value is a
subtype of $t$. The point is that \code{\Cast{?}{42}} is a value, of
type \code{?} which is not a subtype of \code{number}. Therefore the
check in \code{foo} would fail for \code{\Cast{?}{42}} (and so would
the whole function call) which, although sound, it is the opposite of
what every programmer would expect. Indeed, we would expect the test
\code{(typeof($e$)==="number")} to return true for \code{\Cast{?}{42}}
and false for, say, \code{\Cast{?}{true}}, while the stendard
semantics would return false in both cases. It is clear that this
requires to modify the semantic of \code{typeof} to strip off in the
value all the casts, even those that are nested in the value. Changing
the semantics of typecase is feasible though it inserts a new overhead
at run-time. Furthermore one may also consider that not changing it
allows to dynamically check whether some argument has the dynamic type
\code{?} (i.e., whether it was applied to a cast to such a type,
simply by \code{(typeof($e$)==="?")}, thus promoting dynamic types to
a first class type, and not just a directive to the
front-end. Whatever solution we choose it is clear that in both cases
it would be much better if the application \code{foo(42)} were
compiled as it is, thus getting rid of a cast that at best is useless
and at worse gives a counterintuitive and unexpected semantics.
In order to obtain this we have fully exploit the information of
occurrence typing and deduce for the compiled function the type
\code{(number$\to$number)$\wedge$((?\textbackslash
number)$\to$number)} so that the cast is not inserted when the
function is applied to a number. To make this deduction we need a
separate deduction system to collect the type information generated by
the occurrence typing technique we developed in the previous section
(we define a separate deduction system only for presentation purposes:
in reality this should be merged with the type deduction system in
order to avoid several passes on the parse tree).
\beppe{Side remark:
notice that the type \code{(number$\to$number)$\wedge$((?\textbackslash
number)$\to$number)} and \code{((?$\vee$number)$\to$number)} are
equivalent types for subtyping (are they?) but they yield different compilations and,
thus, different results. This is not nice}.
------------------
Finally to take into account gradual typing we need a little bit of
extra work, but just in this last typing rule, all the rest remains
unchanged.
Let $\tau$ be a gradual type. Define $\tau^*$ as the type obtained from $\tau$ by replacing all covariant occurrences of ? by \Any\ and all contravariant ones by \Empty. Now modify the rule above as follows:
\begin{mathpar}
\Infer[Abs]
{\Gamma,x:\tau^*\vdash e\triangleright\psi\and \Gamma,x:\tau\setminus\textstyle\vee_{i\in I}s_i\vdash e:\tau_\circ\and \forall i\in I\quad \Gamma,x:s_i\vdash e:t_i }
{
\Gamma\vdash\lambda x:\tau.e:\textstyle\bigwedge_{i\in I}s_i\to t_i\wedge((\tau\setminus\vee_{i\in I}s_i)\to \tau_\circ)
}
{\psi(x)\supseteq\{s_i\alt i\in I\}\supsetneq\varnothing}
\end{mathpar}
In reality, we want to consider the largest $I$ such that $\{s_i\alt i\in I\}\subseteq\psi(x)$ and the typing does not fail (and $I$ must not be empty). We exclude those that fail because they correspond to branches whose typing requires the presence of gradual types (that we have excluded by considering $\tau$ instead of $\tau$. Notice that if we do not take the maximum, then we obtain a supertype, so the rule is sound but not algorithmic (unless we specify maximum).
The idea behind this rule is the following. We have the function $\lambda x:\tau.e$, where $\tau$ is graudal. Instead of trying to deduce from $\Gamma, x:\tau\vdash e: \tau'$ a generic type $\tau\to\tau'$, we use the occurence typing analysis we developped to collect the set $\psi(x)$ of the (static) types the varible $x$ is checked against in the body of the function. To do that we assign the variable $x$ the type $\tau^*$, that is, the greatest type which is a concretization of $\tau$ and deduce $\psi(x)$. Then, for each type in $\psi(x)$ we try to type the body of the function under the hypothesis that $x$ has that type. If we suceed, we keep the arrow type we just deduced otherwise we discard the typing. Finally, we type the body a last time under the hypothesis that $x$ has the type $\tau$ minus all the types for which the typechecking suceeded (these are the types in $I$), and take the intersection of all these types.
\beppe{I seriously wonder whether the extra arrow is necessary or we can prove that it is already covered by the other arrows but without considering the case $\tau^*$. Plus j'y pense et plus je suis convaincu que la première regle va bien aussi pour le cas graduel, problème il me fait des intersections avec des types graduels}
Note that every time the function is applied to an argument of type $s_i$ no cast is required.
To see how this work, consider again our case study for the case $\tau$ equal to \code{?}. The analysis would yield $\psi(x)=\{\Int,\Real\setminus\Int\}$ for the branch \code{(x $\in$ Int) ? succ x : sqrt x} (as before), but yield $\psi(x)=\{\Any\setminus\Real\}$ for the branch \code{$\neg$x}. Therefore, according to the rule above the function would be checked for the input types, $\Int$, $\Real\setminus\Int$, $\Any\setminus\Real$, and $\code{?}\setminus(\Int\vee(\Real\setminus\Int)$. The typing would fail for the case $\Any\setminus\Real$ leaving just the relevant cases.
\input{gradual}
\subsection{Limitations}
......
Occurrence typing and gradual typing are two complementary disciplines
which have a lot to gain to be integrated, although we are not aware
of any work in this sense. In a sense occurrence typing is a
discipline designed to push forward the frontiers beyond which gradual
typing is needed. For instance, the example at the beginning can be
typed by using gradual typing:
\begin{alltt}\color{darkblue}
function foo(x\textcolor{darkred}{ : \dyn}) \{
(typeof(x) === "number")? x++ : x.length
\}
\end{alltt}
Using ``standard'' gradual typing this is compiled into:
\begin{alltt}\color{darkblue}
function foo(x) \{
(typeof(x) === "number")? (\Cast{number}{x})++ : (\Cast{string}{x}).length
\}
\end{alltt}
where {\Cast{$t$}{$e$}} is a type-cast.\footnote{Intuitively, \code{\Cast{$t$}{$e$}} is
syntactic sugar for \code{(typeof($e$)==="$t$")? $e$ : (throw "Type
error")}. Not exactly though, since to implement compilation \emph{à la} sound gradual typing we need cast on function types.}
%
We have already seen in the introduction that by using occurrence
typing combined with a union type instead of the gradual type \dyn
for parameter annotation, we can avoid the insertion of any cast, at the cost
of some additional type annotations.
But occurrence typing can be used also on the gradually typed code. If we use
occurrence typing to type the gradually-typed version of \code{foo}, this
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 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 of the function.
The reason is that the compiled version of the function
has type \code{\dyn$\to$number}, that is, it expects an argument of type
\dyn, and thus we have to apply a cast (either to the argument or
to the function) whenever this is not the case. In particular, the
application \code{foo(42)} will be compiled as
\code{foo(\Cast{\dyn}{42})}. Now the main problem with such a cast is not
that it produces some unnecessary overhead by performing useless
checks (a cast to \dyn can easily be detected and safely ignored at runtime).
The main problem is that the combination of such a cast with type-cases
will lead to unintuitive results under the standard operational
semantics of type-cases and casts.
Indeed, consider the standard semantics
of the type-case \code{(typeof($e$)==="$t$")} which consists in
reducing $e$ to a value and checking whether the type of the value is a
subtype of $t$. In standard gradual semantics, \code{\Cast{\dyn}{42}} is a value.
And this value is of type \code{\dyn}, which is not a subtype of \code{number}.
Therefore the check in \code{foo} would fail for \code{\Cast{\dyn}{42}}, and so
would the whole function call.
Although this behavior is sound, this is the opposite of
what every programmer would expect: one would expect the test
\code{(typeof($e$)==="number")} to return true for \code{\Cast{\dyn}{42}}
and false for, say, \code{\Cast{\dyn}{true}}, whereas
the standard semantics of type-cases would return false in both cases.
A solution is to modify the semantics of type-cases, and in particular of
\code{typeof}, to strip off all the casts in a value, even nested ones. This
however adds a new overhead at runtime. Another solution is to simply accept
this counter-intuitive result, which has the additional benefit of promoting
the dynamic type to a first class type, instead of just considering it as a
directive to the front-end. Indeed, this approach allows to dynamically check
whether some argument has the dynamic type \code{\dyn} (i.e., whether it was
applied to a cast to such a type, simply by \code{(typeof($e$)==="\dyn")}.
Whatever solution we choose it is clear that in both cases it would be much
better if the application \code{foo(42)} were compiled as is, thus getting
rid of a cast that at best is useless and at worse gives a counter-intuitive and
unexpected semantics.
This is where the previous section about refining function types comes in handy.
To get rid of all superfluous casts, we have to fully exploit the information
provided to us by occurrence typing and deduce for the compiled function the type
\code{(number$\to$number)$\wedge$((\dyn\textbackslash
number)$\to$number)}, so that no cast is inserted when the
function is applied to a number.
To achieve this, we simply modify the typing rule for functions that we defined
in the previous section to accommodate for gradual typing. For every gradual type
$\tau$, we define $\tau^*$ as the type obtained from $\tau$ by replacing all
covariant occurrences of \dyn by \Any\ and all contravariant ones by \Empty. The
type $\tau^*$ can be seen as the \emph{maximal} interpretation of $\tau$, that is,
any expression that can safely be cast to $\tau$ is of type $\tau^*$. In
other words, if a function expects an argument of type $\tau$ but can be
typed under the hypothesis that the argument has type $\tau^*$, then no casts
are needed, since every cast that succeeds will always be to a subtype of
$\tau^*$. Taking advantage of this property, we modify the typing rule for
functions as follows:
\begin{mathpar}
\Infer[Abs]
{\Gamma,x:\tau\vdash e\triangleright\psi\and \forall i\in I\quad \Gamma,x:\sigma_i\vdash e:\tau_i
\and \forall j \in J \subseteq I\quad \Gamma,x:\sigma_j^*\vdash e:\tau_j}
{
\Gamma\vdash\lambda x:\tau.e:\textstyle\bigwedge_{i\in I}\sigma_i\to \tau_i
\land \bigwedge_{j\in J}\sigma_j^*\to \tau_j
}
{\psi(x)=\{\sigma_i\alt i\in I\}}
\end{mathpar}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment