Commit 82fcb58e authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

more review

parent 1a82d3f4
......@@ -62,7 +62,8 @@ by~\citet{Frisch2008}
and detailed description of the algorithm to
decide this relation can be found in~\cite{Cas15}. For the reader's
convenience we succintly recall the definition of the subtyping
relation in the next subsection but it is possible to skip this subsection at first reading andjump directly to Subsection~\ref{sec:syntax}, since to understand
relation in the next subsection but it is possible to skip this
subsection at first reading and jump directly to Subsection~\ref{sec:syntax}, since to understand
the rest of the paper
\else
to which the reader may refer for the formal
......@@ -265,7 +266,18 @@ $(\Int\to t)\setminus(\Int\to\neg\Bool)$, that is, $(\Int\to t)\wedge\neg(\Int\t
}%%%rev
But the sole rule \Rule{Abs+}
above does not allow us to deduce negations of
arrows for $\lambda$-abstractions: the rule \Rule{Abs-} makes this possible. As an aside, note that this kind
arrows for $\lambda$-abstractions: the rule \Rule{Abs-} makes this
possible.
\rev{%%%%
This rule ensures that given a function $\lambda^t x.e$ (where $t$
is an intersection type), for every type $t_1\to t_2$, either
$t_1\to t_2$ can be obtained by subsumption from $t$ or $\neg(t_1\to
t_2)$ can be added to the intersection $t$. In turn this ensures
that, for any function and any type $t$ either the function has type
$t$ or it has type $\neg t$ (see~\citet[Sections 3.3.2 and
3.3.3]{Pet19phd} for a thorough discussion on this rule).
}%%%rev
As an aside, note that this kind
of deduction is already present in the system by~\citet{Frisch2008}
though in that system this presence was motivated by the semantics of types rather than, as in our case,
by the soundness of the type system.
......
......@@ -211,6 +211,18 @@ url={http://www.cduce.org/papers/frisch_phd.pdf}
publisher = {ACM},
}
@PhdThesis{Pet19phd,
author = {Tommaso Petrucciani},
title = {Polymorphic Set-Theoretic Types for Functional Languages},
school = {Joint Ph.D.\ Thesis, Università di Genova and Université Paris Diderot},
month = mar,
url = {https://tel.archives-ouvertes.fr/tel-02119930},
year = 2019,
note = {Available at \url{https://tel.archives-ouvertes.fr/tel-02119930}},
}
@article{castagna2019gradual,
AUTHOR = {Giuseppe Castagna and Victor Lanvin and Tommaso Petrucciani and Jeremy G.~Siek},
TITLE = {Gradual Typing: a New Perspective},
......
......@@ -303,7 +303,7 @@ system cannot directly capture. It can be written in our syntax as:
let example14 = fun (input : Int|String) ->
fun (extra : (Any, Any)) ->
if and2_(is_int input , is_int(fst extra)) is True then
add input (fst extra)
add input (fst extra) \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{ex14}
else if is_int(fst extra) is True then
add (strlen input) (fst extra)
else 0
......@@ -357,6 +357,9 @@ Table~\ref{tab:implem2}, type that is equivalent to $\Int\vee\String \to ((\Int,
Lifting this limitation through a control-flow
analysis is part of our future work.
Although these experiments are still preliminary, they show how the
combination of occurrence typing and set-theoretic types, together
with the type inference for overloaded function types presented in
......
......@@ -589,15 +589,30 @@ the new contributions.
``Compositional reasoning and decidable checking for dependent
contract types'' by Knowles and Flanagan {[}1{]} address the problem
of refined types appearing in arbitrary places, which is very similar
to the first contribution of this work. \textgreater\textgreater{} Kim
to the first contribution of this work.
\begin{answer}
Kim
\end{answer}
An alternative approach followed by refinement type systems is to
ANF-transform the programs. A discussion is missing on how these two
alternatives related to the proposed solution. It appears that the
proposed solution leads to non-terminating, algorithmic checking,
while the two alternatives used by refinement types preserve
decidability. \textgreater\textgreater{} ANF, say that it is a
completely different work that we explore in a different work (not
published yet \ldots{} which is why we did not comment on it)
decidability.
\begin{answer}
Using some normal forms similar to ANF is a completely different
solution that requires very different algorithmic solutions, even
though it reuses some of the results we obtained here (in
particular the definition of the worra operator). We know it for
sure since we explore this solution in a different work where we
define some normal forms that we call maximal sharing canonical
forms. In a nutshell, instead of adding expressions in a
type-environment we bind them in let expressions. We did not
comment on it since the work is currently under submission and it
is not available on line. We may add a comment on it when/if the
other work will at least available on line
\end{answer}
\item
Intersection and refinement types has been extensively studied
{[}e.g., in 2 - 4{]}. Even thought the set-up and the goals of such
......@@ -605,11 +620,17 @@ the new contributions.
not aim for inferences) there are many similarities (e.g., {[}3{]}
also presents a set theoretic interpretation), thus a comparison is
missing.
\begin{answer}
Kim
\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.
{[}5{]} studies the integration of liquid with gradual types while
preserving the gradual guarantees.
\begin{answer}
Victor
\end{answer}
\end{itemize}
......@@ -782,41 +803,100 @@ is, or with small adjustments.
\subsection*{Detailed comments:}
\indent
\begin{itemize}
\item
p3,10, `generic expressions': You have used this phrase a couple of
times at this point, please define it.
\done{(at its first occurrence)}
\begin{answer}
Done {(at its first occurrence)}
\end{answer}
\item
p5,11, `intersect it with': Surely the next term $(t^+ \to\neg t)$ should be negated.
\item
p7,44, typo: `andjump'
\begin{answer}
Done.
\end{answer}
\item
p8,33, `$\partial \in {[}[t_2]{]}$': It seems likely that the codomain of
{[}{[}\_{]}{]} is a subset of \{\cal D\}. Wouldn't this prevent any
{[}{[}\_{]}{]} is a subset of $\mathcal{D}$. Wouldn't this prevent any
function that diverges on any argument from the domain t\_1 from
belonging to {[}{[}t1 -\textgreater{} t2{]}{]}, for any t2? I would
expect that any function in {[}{[}t1 -\textgreater{} t2{]}{]} would be
belonging to {[}{[}t1$\to$t2{]}{]}, for any $t_2$? I would
expect that any function in {[}{[}$t_1\to t_2${]}{]} would be
allowed to diverge on any input.
\begin{answer}
We are not completely sure to understand the remark of the reviewer.
\begin{itemize}
\item The codomain of the interpretation ${[}{[}\_{]}{]}$ is
$\mathcal{P}(\mathcal D)$ (see Definition 2.3), that is
${[}{[}\_{]}{]}$ maps types into subsets of $\mathcal D$.
\item The function that diverges on all arguments
(i.e. $\mathtt{z}(\lambda^{(\any\to\empt)\to(\any\to\empt)} x.x)$ with
$\mathtt{z}$ defined as in Section 4) is interpreted as the empty
relation in
$\mathcal{P}_{\text{\tiny fin}}(\Domain\times\Domain_\Omega)$.
As such it belongs to $\semantic{t_1\to t_2}$ for \emph{every}
type $t_1$ and $t_2$. This is also the reason why the intersection of
two arrow types is never empty.
\item For what concerns the specific question of the reviewer, a
function of type $t_1\to t_2$ that diverges on, say, some
spcific constant $c \in t_1$ will be interpreted as an infinite set of
finite relations $\{R_i\}_{i\in I}$ such that $\forall i\in I.\forall
(d,\partial)\in R_i. d\not= c$. This of course does not preclude
$R_i\in\semantic{t_1\to t_2}$ for all $i\in I$, as the example of the ever
diverging function shows.
\end{itemize}
Does this answer the question?
\end{answer}
\item
p8,47: Same problem, looks like a function cannot have a function type
if it diverges on any argument in the domain. Is that really intended?
\begin{answer}
Same answer as above, a function that diverges on any argument of
the domain $t$ will surely be in the interpretation of the type
$t\to t'$ (whatever $t'$) since the implication vacously holds.
\end{answer}
\item
p9: It seems likely that your calculus is somewhat similar to a simply
typed lambda calculus (assuming that the type that is used to annotate
each $\lambda$ can't be infinite). So maybe all that non-termination stuff
doesn't matter because all well-typed programs terminate. What do you
think?
\begin{answer}
Please see the definition of a fixpoint combinator \texttt{z} in Section
4 and the term
$\mathtt{z}(\lambda^{(\any\to\empt)\to(\any\to\empt)} x.x)$ two
answers above. Our types include recursive types (cf. Section 2.1), so it is possible
to type every pure $\lambda$-term by the type $\mu X.X\to X$, including
the diverging ones.
\end{answer}
p10,17: It would be nice if you could say something about why ${[}Abs-{]}$
should be sound. In general, if you know that $x \in A$ and $(A \land B)
\not= \emptyset$, then you certainly can't conclude that $x \in \not B$.
\item
p10,17: It would be nice if you could say something about why {[}Abs-{]}
should be sound. In general, if you know that $x \in A$ and $(A \land
\neg B)
\not= \emptyset$, then you certainly can't conclude that $x \in \neg B$.
\begin{answer}
We added an explaination and given a reference for a thorough
discussion (lines ??-??)
\end{answer}
\item
p16,41: If the main application of occurrence typing is dynamic
languages, how would you describe the relationship between occurrence
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.
languages use a mostly sound static type system, and smart-casts / type-promotion play a big role in practice.
\begin{answer}
ANYBODY? Victor?!!!
\end{answer}
\item
p27: Having read the implementation section, I noted that it is dealing
with several different things: There are a few sentences about the
implementation. Then we have a small evaluation (coming up with
......@@ -830,6 +910,6 @@ discussion (about the relationship to other work)?
Kim
\end{answer}
\end{itemize}
\end{document}
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