Commit 91a1fc2d authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

finished revision (for me)

parent 2770feef
......@@ -38,12 +38,12 @@ is-y-a-number(x) \{ return(typeof(y)\,===\,"number") \}} which defines
a functions that
disregards its argument and returns whether the variable \code{y} is
an integer or not.\footnote{Although such a function may appear
nonsensical, Kent~\cite{kent19phd} argues that it corresponds a programming
patter that may occurr in Typed Racked due to the the expansion of some
nonsensical, \citet{kent19phd} argues that it corresponds a programming
patter that may occur in Typed Racked due to the expansion of some
sophisticated macro definitions.} While our approach cannot deduce for this function but the
type $\Any\to\Bool$, the logical approach of Tobin-Hochstadt and
Felleisen can record in the type of \code{is-y-a-number} that fact
when the function returns \texttt{true} then \code{y} is a number, and
Felleisen can record in the type of \code{is-y-a-number} the fact that
when the function returns \texttt{true}, then \code{y} is a number, and
the opposite when it returns \texttt{false}. In our approach, the only
possibility to track such a dependency is that the variable \code{y}
is the parameter of an outer function to which our analysis could give
......@@ -182,7 +182,9 @@ the algorithm given in~\citet[Figure 5.2]{kent19phd}
for \emph{function application inversion} is sound only for functions
whose type is an intersection of arrows, whereas our definition
of worra, given in~\eqref{worralgo}, is sound and complete for any function, in
particular, for functions that have a union type, too. The main
particular, for functions that have a union type (for which Kent's
definition may yield unsound results). Apart from these technical
issues, the main
difference of Kent's approach with respect to ours is that, since it
builds on the logical propositions approach, then it focus the use of
set-theoretic types and of the worra (or application inversion)
......@@ -201,15 +203,15 @@ approach does); and when such an application is the argument of a type
test, such as in \texttt{number?\,(f\,x)}, then in Kent's approach it is no longer possible
to refine the information on the argument \texttt{x}. The latter is
not is a flaw of the approach but a design choice: as we explain at
the end of this section, the approach of Type Racket non only focus on the inference of two logical
the end of this section, the approach of Type Racket not only focuses on the inference of two logical
propositions according to the truthy or false value of an expression,
but it does it only for a selected set of \emph{pure} expressions of
but also it does it only for a selected set of \emph{pure} expressions of
the language, to cope with the possible presence of side effects (and
applications do not belong to this set since they can be be impure).
That said the very fact of focusing on truthy vs.\ false results may
make Kent's analysis fail even for pure Boolean tests where it would
be expected to work. For example, consider
the polymophic function that when applied to two integers returns
the polymorphic function that when applied to two integers returns
whether they have the same parity and false
otherwise: \code{have\_same\_parity:$(\Int\To\Int\To\Bool)\land(\neg\Int\To\ANY\To\False)\land(\ANY\To\neg\Int\To\False)$}. We
can imagine to use this function to implicitly test whether two
......@@ -253,38 +255,42 @@ $e_2$} construct
of Dminor refines the type of each branch by remembering that $e$
(resp. $\lnot e$) is true in $e_1$ (resp. $e_2$) and this information
is not propagated to the outer context.
A similar approach is taken in \cite{Chugh12}, and extended to so-called nested refinement types. In these types, an arrow type may
A similar approach is taken by \citet{Chugh12}, and extended to so-called nested refinement types. In these types, an arrow type may
appear in a logical formula (where previous work only allowed formulae
on ``base types''). This is done in the context of a dynamic
language and their approach is extended with polymorphism, dynamic
dispatch and record types.
\rev{A problem that is faced by refinement type systems is the one of
\rev{%%%
A problem that is faced by refinement type systems is the one of
propagating in the branches of a test the information learned on
a \emph{sub-expression} of a tested expression. A solution
e.g. choosen by \cite{OTMW04} and \cite{KF09} is to devise a
that is for instance chosen by~\citet{OTMW04} and \citet{KF09} is to devise a
meta-function that recursively explores both a type and an expression
and propagates the type information on the sub-expressions. This
process (called \emph{selfification} in the cited works) roughly
process---called \emph{selfification} in the cited works---roughly
corresponds to our $\constrf$ function (see Section~\ref{sec:typenv}).
Another approach is the one followed by \cite{RKJ08} is based purely
on a program transformation, namely putting the the term
Another approach is the one followed by \citet{RKJ08} which is
completely based on a program transformation, namely, it consists in putting the term
in \emph{administrative normal form} (\cite{SF92}). Using a program
transformation, every destructor application (function application,
projection, \ldots) is given a name through a let-binding. The problem
of tracking precise type information for every sub-expression is
therefore reduced to the one of keeping precise typing information for
a variable. While this solution seems appealing, it is not as
a variable. While this solution seems appealing, it is not completely
straightforward in our case. Indeed, to retain the same degree of
precision, we would need to identify alpha equivalent sub-expressions
and share the same binding, something that a plain A-normalisation
does not provide.
}
precision, one would need to identify $\alpha$-equivalent sub-expressions
so that they share the same binding, something that a plain A-normalization
does not provide (and which, actually, must not provide, since in that
case the transformation may not preserve the reduction semantics).
}%%%rev
\rev{TODO Intersection + refinement}
\rev{TODO refinement + gradual ?}
\citet{Kent16} bridge the gap between prior work on occurrence typing
and SMT based (sub) typing. It introduces the $\lambda_{RTR}$ core calculus, an
extension of $\lambda_{TR}$ where the logical formulæ embedded in
and SMT-based (sub-)typing. They introduce the $\lambda_{RTR}$ core calculus, an
extension of $\lambda_{TR}$ of~\cite{THF10} where the logical formulæ embedded in
types are not limited to built-in type predicates, but accept
predicates of arbitrary theories. This allows them to provide some
form of dependent typing (and in particular they provide an
......@@ -322,8 +328,31 @@ features (e.g., gradual typing and polymorphism) and we are eager to
test how much of their analysis we can capture and enhance by
formalizing it in our system.
\nocite{typescript,flow}
\rev{%%%
More generally, we believe that what sets apart our work in the
palimpsest of the research on occurrence typing is that we have a type-theoretic
foundational approach striving as much as possible to explain
occurrence typing by extending prior (unrelated but standard) work
while keeping prior results. In that respect, we think that our
approach is not satisfactory, yet, because it uses non standard
type-environments that map expressions rather than variables to
types: but all the rest is standard type-theory. And even on the latter
aspect it must be recognized that the necessity of tracking types not
only for variables but also for more structured expressions is
something that shows up, in different forms, in several other
approaches. For instance, in the approach defined for Typed
Racket~\cite{THF10} the type-system associates to an expression a
quadruple formed by its type, two logical propositions, and an object which is
a pointer to the environment for the type hypothesis about the
expression and, as such, it plays the role of our extended type
environments. Likewise, the \emph{selfification} of ... \textbf{KIM
PLEASE ADD A LINE ON THIS POINT}.
Nevertheless, we are confident that even this last non-standard aspect
of our system can be removed and that occurrence typing can be
explained in a pure standard type-theoretic setting.
We end this presentation of related work with a discussion on side
effects. Although in our system we did not take into account
side-effects---and actually our system works because all the expressions
......@@ -335,7 +364,7 @@ noticed, one can distinguish the approaches that use types to reason about
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
handled. On the one end of the spectrum lies our approach: our
analysis takes into account \emph{all} expressions but, in its current
formulation, it works only for pure languages. On the other end of the
spectrum we find the approach of Typed Racket whose analysis reasons
......@@ -374,7 +403,7 @@ 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
impure expressions but, rather, it has to 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
......
......@@ -76,7 +76,7 @@ distinguish our approach from current ones. We expanded the discussion
on refinement types starting from the references given by reviewer
2. We added few examples. We also positioned our work in the design space of occurrence
typing systems in particular w.r.t. the handling of side effects. All
in all the related work section is now four times longer than in the
in all the related work section is now more than four times longer than in the
submitted version.
\end{answer}
......@@ -310,7 +310,7 @@ prove a more general set of propositions (here, about arbitrary
expressions, there, about expressions with a limited set a pure
functions, but see below) is also present in both.
\begin{answer}
Kim: check this
Done. See lines (???-???)
\end{answer}
Similarly the need for an explosion rule in order to circumvent
......@@ -403,28 +403,30 @@ unneeded:
and have never seen this pattern.
\begin{answer}
We agree with the reviewer on the fact that
interdependent tests do not seem to appear in real
examples. The example we give page 6 to justify the need of
interdependent tests is specifically built for this purpose
and we did not find this pattern in the real examples we
studied.
Still, in a theoretical point of view, we think that it is
important to notice the existence of interdependent tests. It
helps to understand why the parameter \texttt{n\_0} introduced
in the algorithmic type system is required for the
completeness. In a sense, it is similar to the use of type
schemes in our algorithmic type system: as we explained in the
preceding answer, it makes our
algorithmic type system more complex but also more complete
with respect to the declarative one.
We agree with the reviewer that in all examples that we
gleaned on internet to test our system we did not find any
case for interdependent tests, which is why the example we
gave in page 6 to justify the need of
interdependent tests was specifically built for this purpose.
Then, once these formal results have been established and that
the role of type schemes and \texttt{n\_0} are understood, we
can choose to include it or not in a practical implementation
depending on our needs. The remark of the reviewer seems to
imply that a value of \texttt{n\_0\ =\ 1} is enough in practice, and we agree with this.
Still, from a theoretical perspective, we think that it is
important to notice the existence of interdependent tests. It
helps to understand why the parameter $n_o$ introduced in the
algorithmic type system is required for completeness. In a
sense, considering interdependent test has the same motivation
as the use of type schemes in our algorithmic type system: as
we explained in the preceding answer, it makes our algorithmic
type system more complex but also ``more complete'' with respect
to the declarative one.
Once these formal results have been established and that the
role of type schemes and of $n_o$ is understood, we can then
choose whether to include them or not in a practical
implementation depending on our needs.
% The remark of the
% reviewer seems to imply that a value of \texttt{n\_0\ =\ 1} is
% enough in practice, and we agree with this.
% Maybe we should add this remark in the paper? We already say that
......@@ -494,7 +496,8 @@ function (x : [string,string]|[number,number]) {
then again it type checks in our system, in Typed Racket, but it fails in
Flow and in TypeScript.
So we do not really understand the purpose of the example, unless to
So we do not really understand the purpose of the example, unless it
is to
show an example that works both in Typed Racket and in our system but
it does not in TypeScript and Flow. In the case that this were the
correct interpretation of the remark of the reviewer,we added a
......@@ -723,7 +726,7 @@ refinement types, using the given references has a starting point.
\begin{answer}
We can surely answer to the second question, whether users are
required to write more annotations. The answer is an unambiguous
non, quite the contrary. We thought we had stressed enough that a
no, quite the contrary. We thought we had stressed enough that a
clear advantage of our system with respect to existing ones is
that it can infer intersection types without any annotation,
something that only our system can do. In general on the examples
......@@ -930,9 +933,13 @@ language with a large base of existing code. Flow and TypeScript are
amazing industrial implementations that are based on strong
theoretical foundation but they are far from providing any foundation
to this research: it happened more than once that we found some
examples that our work captured and on which TypeScript and Flaw
examples that our work captured and on which TypeScript and Flow
failed and that after a couple of months were fixed and magically
worked in one or the other.
We significantly extended the part in Section 5 where we explain this,
by enriching it with the comments above. See lines (???-???)
\end{answer}
Finally, the implementation section makes me think that the flow
......@@ -1059,6 +1066,13 @@ typing and `smart casts' in Kotlin, resp. type promotion in Dart? Those
languages use a mostly sound static type system, and smart-casts / type-promotion play a big role in practice.
\begin{answer}
ANYBODY? Victor?!!!
This is ground zero occurrence typing that does not require any
formal development. It is less expressive than a small hack that we
implemented in CDuce (which works not only when the tested
expression is a variable but also when it has a value form in which
some variables may occur) and that we did not consider worth
mentioning in the related work section.
\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