Commit bfad3b89 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

more

parent 32d96eb6
......@@ -363,10 +363,17 @@ negated arrow types for functions. This means that the algorithmic
system is not complete as we discuss in details in the next section.
\subsubsection{Properties of the algorithmic system}\label{sec:algoprop}
\rev{%%%
In what follow we will use $\Gamma\vdashA^{n_o} e:t$ to stress the
fact that the judgement $\Gamma\vdashA e:t$ is provable in the
algorithmic system where $\Refinef_{e,t}$ is defined as
$(\RefineStep{e,t})^{n_o}$; we will omit the index $n_o$---thus keeping
it implicit---whenever it does not matter in the context.
}%%%rev
The algorithmic system above is sound with respect to the deductive one of Section~\ref{sec:static}
\begin{theorem}[Soundness]\label{th:algosound}
For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA e: t$, then $\Gamma \vdash e:t$.
For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA^{n_o} e: t$, then $\Gamma \vdash e:t$.
\end{theorem}
The proof of this theorem (see \Appendix\ref{sec:proofs_algorithmic_without_ts}) is obtained by
defining an algorithmic system $\vdashAts$ that uses type schemes,
......@@ -417,7 +424,7 @@ than $\Empty\to\Any$ (see
definition). Then we have:
\begin{theorem}[Completeness for Positive Expressions]
For every type environment $\Gamma$ and \emph{positive} expression $e$, if
$\Gamma\vdash e: t$, then there exist $n_o$ and $t'$ such that $\Gamma\vdashA
$\Gamma\vdash e: t$, then there exist $n_o$ and $t'$ such that $\Gamma\vdashA^{n_o}
e: t'$.
\end{theorem}\noindent
We can use the algorithmic system $\vdashAts$ defined for the proof
......@@ -440,7 +447,7 @@ types, since, intuitively, it corresponds to typing a language in
which in the types used in dynamic tests, a negated arrow never occurs on the
left-hand side of another negated arrow.
\begin{theorem}[Rank-0 Completeness]
For every $\Gamma$, $e$, $t$, if $\Gamma \vdash e:t$ is derivable by a rank-0 negated derivation, then there exists $n_o$ such that $\Gamma\vdashAts e: t'$ and $t'\leq t$.
For every $\Gamma$, $e$, $t$, if $\Gamma \vdash e:t$ is derivable by a rank-0 negated derivation, then there exists $n_o$ such that $\Gamma\vdashAts^{n_o} e: t'$ and $t'\leq t$.
\end{theorem}
\noindent This last result is only of theoretical interest since, in
practice, we expect to have only languages with positive
......
......@@ -312,7 +312,7 @@ where \code{and2\_} is the uncurried version of the \code{and\_}
function we defined in \eqref{and+} and \code{is\_int} is the fuction
defined in the third row of Table~\ref{tab:implem}.
Our system rejects the expression above, while the system by~\citet{THF10}
correctly infers the the function always return an integer. The reason
correctly infers the function always return an integer. The reason
why our system rejects it is because the type it deduces for the
occurrence of \code{input} in the 6th line of the code
is \code{Int|String} rather than \code{String} as required by the
......
......@@ -71,9 +71,10 @@ 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. We also positioned our
work in the design space of occurrence typing systems in particular
w.r.t. the handling of side effects.
distinguish our approach from current ones. We expanded the discussion
on refinement types starting from the references given by reviewer
2. 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:}
......@@ -453,7 +454,7 @@ est de inferer comme nous faison dans le nouveau papier.
@STH. We are not sure we understand this point. It seems that if we
do not want to rewrite the whole function (using a single argument
that we will type as (Int,Int)|(String,String) is to either to have an
that we could type as \texttt{(Int,Int)$\lor$(String,String)} is to either to have an
inference for the non-annotated function able to infer the
intersection type, or explicitly annotate the function with the
intersection type. And this in whatever system on considers,
......@@ -645,6 +646,9 @@ the new contributions.
preserving the gradual guarantees.
\begin{answer}
Victor
The reviewer forgot to include the reference [5] in the report but
we are pretty sure that [5] must refer to ...
\end{answer}
\end{itemize}
\begin{answer}
......@@ -661,6 +665,9 @@ refinment types, using the given references has a starting point.
14) that ``in practise the problem is a very mild one'' but some
discussion on the expected running time of the algorithm in practise
is missing.
\begin{answer}
ANY IDEA?!?!?
\end{answer}
\item \textbf{Evaluation}
......@@ -669,27 +676,89 @@ refinment types, using the given references has a starting point.
these. Instead, section 4 evaluates against {[}23{]} and states that
the new system ``goes beyond what languages like TypeScipt and Flow
do''. Yet, the cost of the new features is not discussed. Is the
presented system much slower than {[}23, TypeScipt, Flow{]}? Are the
presented system much slower than {[}23, TypeScript, Flow{]}? Are the
users required to write more annotations?
\begin{answer}
We can surely answer to the second question, wheter users are
required to write more annotations. The answer is an unambigous
non, 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
that can be captured by our approach (e.g., does that not require
a control flow analysis or involve side effects), our approach
requires less or none annotations and/or infers more precise
types. We substantially expanded the related work section for a
better comparison with related work.
For what concern the first question, viz., whether the presented
system is much slower than Typed Racket, TypeScript, Flow, it is
very difficult to compare mature industrial-scale implementations
such as the cited one with what our system could give if were
implemented with comparable human resources. Already, it is very
difficult to speak of the performance of these systems: for
instant Flow relies on constraint generation and solving which, on
such a large scale can easily give exponential
explosion. Typed Racket, by admission of the authors themselves
(reviewer 1 can contradict us if we are wrong) uses some
not very well documented (euphemism) typing features and heuristics.
In any case our proof-of-concept implementation constitute a very
poor yardstick in this respect.
What we can say is how we expect some characteristics of our
system to impact on the complexity of the inference. For instance
the inference of arrow types has practically zero impact. It adds
just one pass on the parse tree to the normal CDuce type checking
of intersection types for functions (and probably the same for
languages that allow such kind of explicit annotations), that
corresponds to one pass on the function for each arrow in the
intersection.(shall we add such a sentece somewhere?)
Likewise ...
\end{answer}
\end{enumerate}
\subsection*{Minor Comments:}
\begin{itemize}
\item pg 11: In the {[}BASE{]} rule is the comparison of the
environments only syntactic or subtyping is also allowed.
environments only syntactic or subtyping is also allowed.
\begin{answer}
It is (syntactic) identity
\end{answer}
\item Theorem 2.7
mentions n\_0 which does not appear in the theorem statement.
mentions $n_o$ which does not appear in the theorem statement.
\begin{answer}
We changed the notation of the judgments so that it now explicitly
mentions the ${n_o}$ (lines ??-??)
\end{answer}
\item Section
3: Have you shown soundness and completeness for the extended systems?
3: Have you shown soundness and completeness for the extended systems?
\begin{answer}
Not for the record types. However, as we say in the submission
(right after the first definition of [AbsInf+]),
for what concerns the inference of the intersection of arrows,
re-typing ensures the soundness of the new rule.
\end{answer}
\item pg 27: ``the the function''
\begin{answer}
Done.
\end{answer}
\end{itemize}
\subsection*{References used in this review:}
\mbox{}
{[}1{]} https://dl.acm.org/doi/abs/10.1145/1481848.1481853
{[}2{]}
......
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