Commit 1a82d3f4 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

more revision

parent 1ea39487
......@@ -43,13 +43,16 @@ made to converge and, foremost, whether it is of use in practice is among our ob
\fi%
But the real challenges that lie ahead are the handling of side
effects and the addition of polymorphic types. Our analysis works in a
pure system and extending it to cope with side-effects is not
immediate. We plan to do it by defining effect systems---notably, we will try to graft
the effect system of~\citet{Cha2017} on ours---and/or by
performing some information flow analysis typically by enriching the
one we will develop to overcome the limitations above. But our plan is not
more defined than that. For polymorphism, instead, we can easily adapt
effects and the addition of polymorphic types.
\rev{%%%
Our analysis works in a
pure system and we already discussed at length at the end of the
previous section our plans to extend it to
cope with side-effects. However the
ultimate solution of integrating type and effect analysis in a unique tool
is not more defined than that.
}%%%
For polymorphism, instead, we can easily adapt
the main idea of this work to the polymorphic setting. Indeed, the
main idea is to remove from the type of an expression all
the results of the expression that would make some test fail (or
......
......@@ -251,7 +251,8 @@ gradual typing.
%% Acknowledgments
\subsubsection*{Acknowledgments}
\noindent The authors thank Paul-André Melliès for his help on type
ranking and Sam Tobin-Hochstadt for his feedback and useful insight.
ranking and Sam Tobin-Hochstadt and the other reviewers for their
feedback and useful insight.
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
......@@ -259,7 +260,6 @@ ranking and Sam Tobin-Hochstadt for his feedback and useful insight.
\newpage
%% Bibliography
\bibliographystyle{ACM-Reference-Format}
\bibliography{main}
......
......@@ -287,14 +287,14 @@ formalizing it in our system.
\rev{%%%
We end this presentation of related work with a discussion on side
effects. Even if in our system we did not take into account
effects. Although in our system we did not take into account
side-effects---and actually our system works because all the expressions
of our language are pure---it is interesting to see how the different
approaches of gradual typing position themselves with respect to the problem of
handling side-effects, since this helps to better position our work in the taxonomy
of the current litterature. As Sam Tobin-Hochstadt insightfully
approaches of occurrence typing position themselves with respect to the problem of
handling side effects, since this helps to better place our work in the taxonomy
of the current literature. As Sam Tobin-Hochstadt insightfully
noticed, one can distinguish the approaches that use types to reason about
the dynamic behaviour of programs according to the set of expressions
the dynamic behavior of programs according to the set of expressions
that are taken into account by the analysis. In the case of occurrence
typing, this set is often determined by the way impure expressions are
taken into account. On one end of the spectrum lies our approach: our
......@@ -306,22 +306,47 @@ accessors). Somewhere in-between lies the approach of the
Flow language which, as hinted above, implements a complex effect systems to determine
pure expressions. While the system presented here does not work for
impure languages, we argue that its foundational nature predisposes it
to be adapted to handle impure expression, by adopting existing
solutions or providing new ones. For instance, it is not hard to
to be adapted to handle impure expressions as well, by adopting existing
solutions or proposing new ones. For instance, it is not hard to
modify our system so that it takes into account only a set of
predetermined pure expressions, as done by Typed Racket: it suffices
to modify the definition of $\Gamma \evdash e
{(\neg)t} \Gamma'$ (cf.\ Section~\ref{sec:static}) so that $\Gamma'$
extends $\Gamma$ with type hypotheses for all expressions occurring in
$e$ that are also in the set of predetermined pure expressions
(instead of for all subexpressions of $e$, tout court).
However such a solution would be mildly interesting since by excluding
from the analysis all functions application we would lose most of the
advantages of our approach with respect to the one of logical
propositions.
(instead of extending it for all subexpressions of $e$, \emph{tout court}).
However, such a solution would be marginally interesting since by excluding
from the analysis all applications we would lose most of the
advantages of our approach with respect to the one with logical
propositions. Thus a more interesting solution would be to use some
external static analysis tools---e.g., to graft
the effect system of~\citet{Cha2017} on ours---to detect impure
expressions. The idea would be to mark different occurrences of a same
impure expression using different marks. These marks would essentially
be used to verify the presence of type hypotheses for a given
expression in a type environment $\Gamma$; the idea being that
expressions with different marks are to be considered as different
expressions and, therefore, would not share the same type
hypothesis. For instance, consider the test
$\ifty{f\,x}\Int{\,...\,}{\,...}$: if $f x$ were flagged as impure
then the occurrence of $f x$ in the ``then'' branch would not be
supposed to be of type $\Int$ since it would be typed in an
environment $\Gamma$ containing a binding for an $f\,x$ expression
having a mark different from the one in the ``then'' branch: the
regular typing rules would apply for $f\, x$ in that case. This
would certainly improve our analysis, but we believe that ultimately
our system should not resort to external static analysis tools to detect
impure expressions but, rather, it should integrate this analysis with
the typing one, so as to mark \emph{only} those impure expression
whose side-effects may affect the semantics of some type-cases. For
instance, consider a JavaScript object \code{obj} that we modify as
follows \code{obj["key"] = 3}. If the field \code{"key"} is already
present in \code{obj} with type \Int{} and we do not test it more than
about this type, then it is not necessary to mark different
occurrences of \code{obj} with different marks, since the result of
the type-case would not be changed by the assignment; the same holds
true if the field is absent but type-cases do not discriminate on its
presence. Otherwise, some occurrences of \code{obj} must use different
marks: the analysis will determine which ones. We leave this study for
future work.
}%%%rev
......@@ -71,7 +71,9 @@ discussion to compare our work with Andrew Kent dissertation, we
greatly increased the comparison of our work with the \emph{logical
proposition} approach of Typed Racket to better stress the limitation
of our approach and discussed at length some technical choices that
distinguish our approach from current ones.
distinguish our approach from current ones. We also positioned our
work in the design space of occurrence typing systems in particular
w.r.t. the handling of side effects.
\end{answer}
\section{Reviewer \#1:}
......@@ -176,10 +178,10 @@ in light of the topic and of the fact that it heavily relies on semantic
subtyping. Probably a consequence of the pandemic.
Of course, the new version of the related work section includes now a
detailed comparaison with the (highly related) chapter 5 of the
detailed comparaison with the (indeed highly related) chapter 5 of the
dissertations, see lines (??-??) and, yes, the function application
inversion of Kent is, in the spirit, the same as our worra operator
(we do not know whether the reviewer noticed that ``worra'' is an
(we do not know whether the reviewers noticed that ``worra'' is an
inversed ``arrow'': read it from right to left).
About that, we take the opportunity that the reviewer disclosed the fact
that he is Kent's supervisor to signal a small error that we think we
......@@ -194,7 +196,9 @@ inv(((\True\to\False)\land(\False\to\True))\lor((\True\to\True)\land(\False\to\F
\end{array}
\]
However, a function with a type $((\True\to\False) land (\False\to\True)) \lor ((\True\to\True)\land(\False\to\False))$ could definitively give a result in $\True$. The correct result should be \Bool.
However, a function with a type $((\True\to\False) \land
(\False\to\True)) \lor ((\True\to\True)\land(\False\to\False))$ may
definitively yield a result in $\True$ or in $\False$. The correct result should be \Bool.
The proof in Coq of the soundness of this definition given in the
......@@ -314,7 +318,7 @@ potential dynamic behavior of terms in the way done with occurrence
typing will need to decide \emph{which} terms the type system should
take note of, and what equations it will use over those terms. For
example, if we have the expression
\texttt{(f\ x) $\in$ (1,\ 1)}, should that refine the
\texttt{(f\ x) $\in$ (1,1)}, should that refine the
type of \texttt{(g\ x)}? Possible questions to ask here are: is
\texttt{f} pure? Is \texttt{f} syntactically equal to \texttt{g}? Can we
prove that \texttt{f} and \texttt{g} are equivalent?
......@@ -339,9 +343,10 @@ paper clearer.
\begin{answer}
Beppe: say that our approach in some sense subsumes the two others. Add
a part of related work discussing about pure expressions. Use (not
verbatim) the rebuttal of POPL. Thanks for the insight
This is a very nice insight. We reproduced it (giving credits) in the
section on related work, which now ends with a long discussion on the
design space w.r.t. side effects and on our future plans to cope with
the presence of impure expressions. (lines ??-??)
\end{answer}
......@@ -495,7 +500,7 @@ type preservation). We rewrote the sentence to be more clear.
interpretation of) \any. We added an explaination (see lines
???-???). In short \texttt{Undef} is a special singleton type
whose intepretation contains only a the
constant \texttt{undef} which is not in D.
constant \texttt{undef} which is not in $\Domain$.
\end{answer}
\item
......
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