Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Giuseppe Castagna
occurrence-typing
Commits
a26e7df9
Commit
a26e7df9
authored
Sep 28, 2021
by
Giuseppe Castagna
Browse files
typos
parent
da6baca7
Changes
1
Hide whitespace changes
Inline
Side-by-side
scp-reviews-2108.tex
View file @
a26e7df9
...
...
@@ -183,7 +183,7 @@ subtyping. Probably a consequence of the pandemic.
Of course, the new version of the related work section includes now a
detailed comparison with the (indeed highly related) chapter 5 of the
dissertations, see
lines (
??-??) and, yes, the function application
dissertations,
(
see
: p30l
??-??) and, yes, the function application
inversion of Kent is, in the spirit, the same as our worra operator
(we do not know whether the reviewers noticed that ``worra'' is an
inverted ``arrow'': read it from right to left).
...
...
@@ -195,8 +195,8 @@ should be an intersection instead. As it is stated the current
definition seems unsound as the following example shows:
\[
\begin
{
array
}{
l
}
inv
(((
\True\to\False
)
\land
(
\False\to\True
))
\lor
((
\True\to\True
)
\land
(
\False\to\False
))
\;
,
\;\True
)=
\\
\qquad\Bool\setminus
(
\True\lor\False
)=
\\
\qquad\Empty\\
\qquad
=
\Bool\setminus
(
\True\lor\False
)=
\\
\qquad
=
\Empty\\
\end
{
array
}
\]
That is, we have applied the formula
$
inv
(
\tau
_
f,
\sigma
_{
our
}
)
=
...
...
@@ -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}
Done
. See lines (
???-???)
Done
(see: p32l
???-???)
\end{answer}
Similarly the need for an explosion rule in order to circumvent
...
...
@@ -319,7 +319,7 @@ difficulties in proofs of type soundness is discussed in {[}22{]}.
\begin{answer}
We added a long discussion on this point, namely how to
handle the type preservation property, in the related work section when
comparing with
{
[
}
22
{
]
}
(see
lines:
??-??)
comparing with
{
[
}
22
{
]
}
(see
: p29l
??-??)
More generally, we also went more in depth in the comparison with the
logical approach by THF, to highlight further limitations of our
...
...
@@ -363,7 +363,7 @@ paper clearer.
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
??-??)
the presence of impure expressions. (
see: p32l
??-??)
\end{answer}
...
...
@@ -382,7 +382,7 @@ unneeded:
\begin{answer}
We added a long discussion to explain the reasons of our
choice. It is in the related work section (
lines
??-??) when
choice. It is in the related work section (
see: p29l
??-??) when
comparing with
{
[
}
22
{
]
}
(i.e. Tobin-Hochstadt
\&
Felleisen
2008). In a nutshell we prefer starting with a system that
satisfies type preservation, define a sound but not-complete
...
...
@@ -501,7 +501,7 @@ 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
comment in
lines
???-???
comment in
p28l
???-???
\end{answer}
...
...
@@ -565,8 +565,8 @@ type preservation). We rewrote the sentence to be more clear.
Section 2.2
$
\semantic
{
\neg\empt
}
=
\Domain\setminus\semantic
{
\empt
}
=
\Domain
$
. So
$
\semantic
{
\empt
}$
is empty and undef is not in (the
interpretation of)
\any
. We added an explanation (see
lines
???-???). In short
\texttt
{
Undef
}
is a special singleton type
interpretation of)
\any
. We added an explanation (see
:
p17l
???-???). In short
\texttt
{
Undef
}
is a special singleton type
whose interpretation contains only a the
constant
\texttt
{
undef
}
which is not in
$
\Domain
$
.
\end{answer}
...
...
@@ -659,7 +659,7 @@ the new contributions.
of refined types appearing in arbitrary places, which is very similar
to the first contribution of this work.
\begin{answer}
Done (
lines ??-
??)
Done (
page 31
??)
\end{answer}
An alternative approach followed by refinement type systems is to
ANF-transform the programs. A discussion is missing on how these two
...
...
@@ -668,7 +668,7 @@ the new contributions.
while the two alternatives used by refinement types preserve
decidability.
\begin{answer}
Done (
lines ??-
??)
Done (
page 31
??)
\end{answer}
\item
...
...
@@ -679,7 +679,7 @@ the new contributions.
also presents a set theoretic interpretation), thus a comparison is
missing.
\begin{answer}
Done (
lines ??-
??)
Done (
page 31
??)
\end{answer}
\item
In 3.3 it is mentioned that ``we are not aware of any study in this
...
...
@@ -691,15 +691,12 @@ the new contributions.
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
Inference'' (OOPSLA 2018). We were aware of this work
,
of course
,
but we would not define it an example of integration of gradual
and occurrence typing
..
.
and occurrence typing
. The connection between them seems incidental
.
\end{answer}
\end{itemize}
\begin{answer}
We have further developed the our section of the related work on
refinement types, using the given references has a starting point.
\end{answer}
\item
\textbf
{
Meta-theory Clarifications:
}
...
...
@@ -735,7 +732,7 @@ refinement types, using the given references has a starting point.
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. We also added at the end of
Section 4 a new example th
e we
capture and for which Flow and
Section 4 a new example th
at our system
capture
s
and for which Flow and
TypeScript fail.
For what concern the first question, viz., whether the presented
...
...
@@ -749,7 +746,8 @@ refinement types, using the given references has a starting point.
Racket, by admission of the authors themselves (reviewer 1 can
contradict us if we are wrong) uses some not very well documented
typing features and heuristics. In any case our proof-of-concept
implementation constitute a very poor yardstick in this respect.
implementation constitutes a very poor yardstick in this respect,
but it never meant to be one.
What we can say is how we expect some characteristics of our
system to impact on the complexity of the inference. For instance
...
...
@@ -760,7 +758,7 @@ refinement types, using the given references has a starting point.
corresponds to one pass on the function for each arrow in the
intersection.(shall we add such a sentence somewhere?)
Likewise ... TO BE CONTINUED BY KIM.
Likewise ... TO BE CONTINUED BY KIM
(fixpoint, memoization ...)
.
\end{answer}
...
...
@@ -781,7 +779,7 @@ refinement types, using the given references has a starting point.
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
}$
(
see p15l
??-??)
\end{answer}
\item
Section
...
...
@@ -938,7 +936,7 @@ 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 (
???-???
)
by enriching it with the comments above. See
p32l
???-???
.
\end{answer}
...
...
@@ -1059,7 +1057,7 @@ should be sound. In general, if you know that $x \in A$ and $(A \land
\not
=
\emptyset
$
, then you certainly can't conclude that
$
x
\in
\neg
B
$
.
\begin{answer}
We added an explanation and given a reference for a thorough
discussion (
lines
??-??)
discussion (
see p10l
??-??)
\end{answer}
\item
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment