Commit 94d30602 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

final touches

parent 37a871d3
* We refine the type of expressions occurring in type tests, thus removing the limitations of current occurrence-typing approaches where both tests and refinements are limited to variables.
* We define a type-theoretic approach alternative to the current flow-based approaches: it provides different results and can thus be combined with flow-based techniques.
* We use our analysis for defining a formal framework that reconstructs intersection types for unannotated or partially-annotated functions
* We prove the soundness of our system. We define algorithms to infer the types that we prove to be sound and complete.
* We show how to extend our approach to records with field addition, update, and deletion operations.
* We show how occurrence typing can be extended to and combined with gradual typing and used to optimize the latter.
......@@ -5,26 +5,26 @@ these languages.
First, we consider record types and record expressions which, in dynamic
languages, are used to implement objects. In particular, we extend our
system to cope with typical usage patterns of objects in these
system to cope with typical usage patterns of objects employed in these
languages such as adding, modifying, or deleting a field, or dynamically
test its presence to specify different behaviors.
testing its presence to specify different behaviors.
Second, in order
to precisely type applications in dynamic languages it is
crucial to refine the type of some functions to account for their
different behaviors with specific input types. But current approaches
are bad at it: they require the programmer to explicitly specify a
precise intersection type for these function and, even with such specifications, several common cases
precise intersection type for these functions and, even with such specifications, some common cases
fail to type (in that case the only solution is to hard-code the
function and its typing discipline into the language). We show how we
can use the work developed in the previous sections to infer precise
intersection types for functions. These functions do not
require any type annotation in our system or just an annotation for
intersection types for functions. In our system, these functions do not
require any type annotation or just an annotation for
the function parameters, whereas some of them fail to type in
current alternative approaches even when they are given the full intersection type
specification.
Finally, to type dynamic language it is often necessary to make
Finally, to type dynamic languages it is often necessary to make
statically-typed parts of a program coexist with dynamically-typed
ones. This is the aim of gradually typed systems that we explore in
the third extension of this section.
......
......@@ -10,7 +10,8 @@ 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 study in this sense. We study it for the formalism of Section~\ref{sec:language} for which the integration of gradual typing was defined by~\citet{castagna2019gradual}.
of any study in this sense. We explore this integration for the formalism of Section~\ref{sec:language} for which the integration of gradual typing was defined by~\citet{castagna2019gradual}.
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
......@@ -21,7 +22,7 @@ typed by using gradual typing:%\svvspace{-.2mm}
return (typeof(x) === "number")? x+1 : x.trim(); \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo3}
\}\negspace
\end{alltt}
``Standard'' gradual typing inserts two dynamic checks since it compiles the code above into:
``Standard'' or ``safe'' gradual typing inserts two dynamic checks since it compiles the code above into:
\begin{alltt}\color{darkblue}\morecompact
function foo(x) \{
return (typeof(x) === "number")? (\textcolor{darkred}{\Cast{number}{{\color{darkblue}x}}})+1 : (\textcolor{darkred}{\Cast{string}{{\color{darkblue}x}}}).trim();
......@@ -60,7 +61,7 @@ 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.
as the cast to \code{$\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 values, even nested ones.
While this adds a new overhead at runtime, this is preferable to losing the
......
......@@ -181,7 +181,17 @@
\input{abstract}
\end{abstract}
\begin{keyword}
occurrence typing \sep
type inference \sep
union types \sep
intersection types \sep
TypeScript \sep
Flow language \sep
dynamic languages \sep
type case \sep
gradual typing.
\end{keyword}
\end{frontmatter}
......@@ -225,7 +235,7 @@
%% Acknowledgments
\subsubsection*{Acknowledgments}
The authors thank Paul-André Melliès for his help on type ranking.
\noindent The authors thank Paul-André Melliès for his help on type ranking.
This research was partially supported by Labex DigiCosme (project ANR-11-LABEX-0045-
DIGICOSME) operated by ANR as part of the program «Investissement d'Avenir» Idex
......@@ -233,7 +243,7 @@ The authors thank Paul-André Melliès for his help on type ranking.
\newpage
%% Bibliography
\bibliographystyle{ACM-Reference-Format}
\bibliography{main}
......
......@@ -151,7 +151,7 @@ url={http://www.cduce.org/papers/frisch_phd.pdf}
}
@article{Cas15,
author = {G. Castagna},
author = {Giuseppe Castagna},
title = {Covariance and Contravariance: a fresh look at an
old issue (a primer in advanced type systems for
learning functional programmers)},
......@@ -224,7 +224,7 @@ url={http://www.cduce.org/papers/frisch_phd.pdf}
@inproceedings{siek2006gradual,
title={Gradual typing for functional languages},
author={Siek, Jeremy G and Taha, Walid},
author={Siek, Jeremy G. and Taha, Walid},
booktitle={Scheme and Functional Programming Workshop},
volume={6},
pages={81--92},
......@@ -328,7 +328,7 @@ series = {POPL ’12}
@inproceedings{siek2015refined,
title={Refined criteria for gradual typing},
author={Siek, Jeremy G and Vitousek, Michael M and Cimini, Matteo and Boyland, John Tang},
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)},
year={2015},
organization={Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik}
......@@ -336,7 +336,7 @@ series = {POPL ’12}
@incollection{siek2016recursive,
title={The recursive union of some gradual types},
author={Siek, Jeremy G and Tobin-Hochstadt, Sam},
author={Siek, Jeremy G. and Tobin-Hochstadt, Sam},
booktitle={A List of Successes That Can Change the World},
pages={388--410},
year={2016},
......
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