Commit 5b570b68 authored by Victor Lanvin's avatar Victor Lanvin
Browse files

More on gradual typing

parent b2eca9cf
Gradual typing is an approach proposed by~\citet{siek2006gradual} to
combine the safety guarantees of static typing with the programming
flexibility of dynamic typing. The idea is to introduce an \emph{unknown}
(or \emph{dynamic}) type, denoted $\dyn$, used to inform the compiler that
some static type-checking can be omitted, at the cost of some additional
runtime checks. The use of both static typing and dynamic typing in a same
program creates a boundary between the two, where the compiler automatically
adds ---often costly~\cite{takikawa2016sound}--- dynamic type-checks to ensure
that a value crossing the barrier is correctly typed.
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
of any work in this sense. Moreover, the integration of gradual typing with
set-theoretic types has already been studied by~\citet{castagna2019gradual},
which allows us to keep the same formalism. 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
typing is needed, thus reducing the amount of runtime checks 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}) \{
......@@ -86,13 +99,51 @@ 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}
%\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}
\[
\textsc{[AbsInf+]}
\frac
{
\begin{align*}
\Gamma,x:&\sigma\vdash e\triangleright\psi \qquad \qquad \Gamma,x:\sigma\vdash e:\tau\\
T = \{ (\sigma, \tau) \}
&\cup \{ (\sigma,\tau) ~|~ \sigma \in \psi(x) \land \Gamma, x: \sigma \vdash e: \tau \}\\
&\cup \{ (\sigma^*,\tau) ~|~ \sigma \in \psi(x) \land \Gamma, x: \sigma^* \vdash e: \tau \}
\end{align*}
}
{
\Gamma\vdash\lambda x:\sigma.e:\textstyle\bigwedge_{(\sigma,\tau) \in T}\sigma\to \tau
}
\]
The main idea behind this rule is the same as before: we first collect all the
information we can into $\psi$ by analyzing the body of the function. We then
retype the function using the new hypothesis $x : \sigma$ for every
$\sigma \in \psi(x)$. However, we also retype the function using the hypothesis
$x : \sigma^*$, following the explanation we gave in the previous paragraph.
This allows us to eliminate unnecessary gradual types.
Going back to our previous example with function \code{foo}, we first deduce
the refined hypothesis
$\psi(x) = \{\code{number}\land\dyn, \dyn \textbackslash \code{number}\}$.
Typing the function using this new hypothesis but without considering the
maximal interpretation would yield
$(\dyn \to \code{number}) \land ((\code{number} \land \dyn) \to \code{number})
\land ((\dyn \textbackslash \code{number}) \to \code{number})$. However, as
we stated before, this would introduce an unnecessary cast if the function
were to be applied to an integer. Hence the need for the second part of
Rule~\textsc{[AbsInf+]}: the maximal interpretation of $\code{number} \land \dyn$
is $\code{number}$, and it is clear that, if $x$ is given type \code{number},
the function type-checks, thanks to occurrence typing. Thus, after some
simplifications, we can actually deduce the desired type
$(\code{number} \to \code{number}) \land ((\dyn \textbackslash \code{number}) \to \code{number})$.
......@@ -99,4 +99,36 @@ Finally, I took advantage of this opportunity to describe some undocumented adva
NUMBER = {POPL\,'19 46nd ACM Symposium on Principles of Programming Languages},
MONTH = jan,
YEAR = {2019},
}
\ No newline at end of file
}
@inproceedings{siek2006gradual,
title={Gradual typing for functional languages},
author={Siek, Jeremy G and Taha, Walid},
booktitle={Scheme and Functional Programming Workshop},
volume={6},
pages={81--92},
year={2006}
}
@inproceedings{takikawa2016sound,
title={Is sound gradual typing dead?},
author={Takikawa, Asumu and Feltey, Daniel and Greenman, Ben and New, Max S and Vitek, Jan and Felleisen, Matthias},
booktitle={ACM SIGPLAN Notices},
volume={51},
number={1},
pages={456--468},
year={2016},
organization={ACM}
}
@article{castagna2019gradual,
title={Gradual typing: a new perspective},
author={Castagna, Giuseppe and Lanvin, Victor and Petrucciani, Tommaso and Siek, Jeremy G},
journal={Proceedings of the ACM on Programming Languages},
volume={3},
number={POPL},
pages={16},
year={2019},
publisher={ACM}
}
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