Commit f8de7536 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Reworked the related work section.

parent da876c60
......@@ -19,7 +19,8 @@ respect to \Rule{AbsInf+} is that the typing of the body
is made under the hypothesis $x:s\setminus\bigvee_{s'\in\psi(x)}s'$,
that is, the domain of the function minus all the input types
determined by the $\psi$-analysis. This yields an even better refinement
of the function type that makes a difference for instance with the inference for the function \code{xor\_} (Code 3
of the function type that makes a difference for instance with the
inference for the function \code{xor\_} (see Code 3
in Table~\ref{tab:implem}): the old rule would have returned a less precise type. The rule above is defined for functions annotated by a single arrow type:
the extension to annotations with intersections of multiple arrows is similar to the one we did in the
simpler setting of Section~\ref{sec:refining}.
We have implemented the algorithmic system $\vdashA$ we presented in Section~\ref{sec:algorules}. Our
implementation is written in OCaml and uses CDuce as a library to
provide the semantic subtyping machinery. Besides the type-checking
\rev{We present in this section preliminary results obtained by our
implementation. After giving some technical highlights, we focus on
demonstrating the behaviour of our typing algorithm on meaningful
examples. We also provide an in-depth comparison with the fourteen
examples of \cite{THF10}}.
\subsection{Implementation details}
We have implemented the algorithmic system $\vdashA$ we presented in Section~\ref{sec:algorules}. Besides the type-checking
algorithm defined on the base language, our implementation supports
the record types and expressions of Section \ref{ssec:struct} and the refinement of
function types
......@@ -14,7 +20,18 @@ Appendix~\ref{app:optimize}.
\fi%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
The implementation is rather crude and consists of 2000 lines of OCaml code,
including parsing, type-checking of programs, and pretty printing of types. We
including parsing, type-checking of programs, and pretty printing of
types. \rev{CDuce is used as a library to provide set-theoretic types and
semantic subtyping. The implementation faithfully transcribe in OCaml
the algorithmic system $\vdashA$ as well as all the type operations
defined in this work. One optimization that our implementation
features (w.r.t to the formal presentation) is the use of a
memoization environment in the code of the $\Refine {e,t}{\Gamma}$
function, that allows to avoid several traversal of $e$.
}
\subsection{Experiments}
We
demonstrate the output of our type-checking implementation in
Table~\ref{tab:implem} and Table~\ref{tab:implem2}. Table~\ref{tab:implem} lists
some examples, none of which can be typed by current systems. Even though some
......@@ -23,9 +40,7 @@ explicit type annotations, the code 6, 7, 9, and 10 in Table~\ref{tab:implem}
and, even more, the \code{and\_} and \code{xor\_} functions given
in \eqref{and+} and \eqref{xor+} later in this
section are out of reach of current systems, even when using the right explicit
annotations. Table~\ref{tab:implem2} allows for a direct comparison of with
\cite{THF10} by giving the type inferred for the fourteen examples given in that
work.
annotations.
It should be noted that for all the examples we present, the
time for the type inference process is less than 5ms, hence we do not report
......@@ -38,7 +53,7 @@ online toplevel available at
\url{https://occtyping.github.io/}%
\input{code_table}
In both tables, the second column gives a code fragment and the third
In Table~1, the second column gives a code fragment and the third
column the type deduced by our implementation as is (we
pretty printed it but we did not alter the output). Code~1 is a
straightforward function similar to our introductory
......@@ -247,7 +262,7 @@ let get_property_l =
\end{alltt}
where \code{\textit{S}} is \code{Object} and \code{\textit{T}} is \code{Any}.
\subsection{Comparison with \cite{THF10}}
\input{code_table2}
In Table~\ref{tab:implem2}, we reproduce in our syntax the 14
......
......@@ -487,7 +487,7 @@ If we rewrite the function so that it has just a single argument of type
\begin{verbatim}
function (x : [string,string]|[number,number]) {
if (typeof x[0] === "string") {
return x[0].concat(x[1]);
return x[0].concat(x[1]);
} else {
return x[0] + x[1];
}
......@@ -679,8 +679,8 @@ the new contributions.
also presents a set theoretic interpretation), thus a comparison is
missing.
\begin{answer}
Kim: far fetched?
\end{answer}
Done (lines ??-??)
\end{answer}
\item
In 3.3 it is mentioned that ``we are not aware of any study in this
sense'', i.e., the integration of occurrence and gradual types.
......@@ -688,7 +688,7 @@ 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 ``Gradual Liquid Type
Inference'' (OOPSLA 2018). We were aware of this work of course
......@@ -762,10 +762,10 @@ refinement types, using the given references has a starting point.
Likewise ... TO BE CONTINUED BY KIM.
\end{answer}
\end{enumerate}
......@@ -776,14 +776,14 @@ refinement types, using the given references has a starting point.
\begin{answer}
It is (syntactic) identity
\end{answer}
\item Theorem 2.7
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 ??-??)
mentions the ${n_o}$ (lines ??-??)
\end{answer}
\item Section
3: Have you shown soundness and completeness for the extended systems?
\begin{answer}
......@@ -792,7 +792,7 @@ refinement types, using the given references has a starting point.
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.
......@@ -961,7 +961,7 @@ function types which are intersections of arrow types?)
type-case but also because this yields more precise types, then we would
have solved the problem. We are pretty confident that we can have it
within a pure type-theoretic approach, without resorting to flow
analysis. We are currently working on it.
analysis. We are currently working on it.
\end{answer}
All in all, this is a very interesting paper, technically convincing,
......@@ -1089,7 +1089,9 @@ Couldn't you organize this section in a clearer way, perhaps splitting
it into an implementation section and an evaluation section and a
discussion (about the relationship to other work)?
\begin{answer}
Kim
Done. We kept in the Implementation section the direct comparison with
the examples {[}23{]} and moved and improved the more general aspects
of the comparison in the related work section.
\end{answer}
\end{itemize}
......
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