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

Reworked section on gradual types

parent 12183920
......@@ -56,26 +56,39 @@ 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 type safe, 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.
would the whole function call.
Although this behavior is type safe, this violates the gradual
guarantee~\cite{siek2015refined} since giving a \emph{more precise} type to
the parameter \code{x} (such as \code{number}) would make the function succeed,
as the cast to $\dyn$ would not be inserted.
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 at least the 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 would allow 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.
\code{typeof}, to strip off all the casts in values, even nested ones.
While this adds a new overhead at runtime, this is preferable to losing the
gradual guarantee, and the overhead can be mitigated by having a proper
representation of cast values that allows to strip all casts at once.
However, this problem gets much more complex when considering functional values.
In fact, as we hinted in Section~\ref{ssec:algorithm}, there is no way to
modify the semantics of type cases to preserve both the gradual guarantee and
the soundness of the system in the presence of arbitrary type cases.
For example, consider the function
$f = \lambda^{(\Int \to \Int) \to \Int} g. \tcase{g}{(\Int \to \Int)}{g\
1}{\code{true}}$. This function is well-typed since the type of the
parameter guarantees that only the first branch can be taken, and thus that
only an integer can be returned. However, if we apply this function
to $h = \MCast{\Int \to \Int}{(\lambda^{\dyn \to \dyn} x.\ x)}$, the type case
strips off the cast around $h$ (to preserve the gradual guarantee), then
checks if $\lambda^{\dyn \to \dyn} x.\ x$ has type $\Int \to \Int$.
Since $\dyn \to \dyn$ is not a subtype of $\Int \to \Int$, the check fails
and the application returns $\code{true}$, which is unsound.
Therefore, to preserve soundness in the presence of gradual types, type cases
should not test functional types other than $\Empty \to \Any$, which is
the same restriction as the one presented by~\citet{siek2016recursive}.
While this solves the problem of the gradual guarantee, it is clear that
it would be much better if the application \code{foo(42)} were compiled as is,
without introducing the cast \code{\Cast{\dyn}{42}}, thus getting rid of the
overhead associated with removing this cast in the type case.
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 function in~\eqref{foo3} the type
......@@ -294,4 +294,21 @@ series = {POPL ’12}
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {},
bibsource = {dblp computer science bibliography,}
\ No newline at end of file
title={Refined criteria for gradual typing},
author={Siek, Jeremy G and Vitousek, Michael M and Cimini, Matteo and Boyland, John Tang},
booktitle={1st Summit on Advances in Programming Languages (SNAPL 2015)},
organization={Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik}
title={The recursive union of some gradual types},
author={Siek, Jeremy G and Tobin-Hochstadt, Sam},
booktitle={A List of Successes That Can Change the World},
......@@ -110,6 +110,7 @@
\newcommand {\Cast}[2]{\tt #2\(\langle\)#1\(\rangle\)}
\newcommand {\MCast}[2]{#2\langle #1\rangle}
\newcommand {\ifty}[4]{\ensuremath{\texttt{(}#1\in#2\texttt{)?}#3\texttt{:}#4}}
\newcommand {\code}[1]{\texttt{\color{darkblue}#1}}
\newcommand {\p}[1]{\texttt{#1}}
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