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
48fbf168
Commit
48fbf168
authored
Sep 23, 2021
by
Giuseppe Castagna
Browse files
more revsion
parent
bc1057f4
Changes
4
Hide whitespace changes
Inline
Side-by-side
algorithm.tex
View file @
48fbf168
...
...
@@ -394,12 +394,22 @@ system $\vdashA$
is not complete w.r.t.
\
the language presented in
Section~
\ref
{
sec:syntax
}
because it cannot deduce negated arrow
types for functions.
However, no practical programming language would implement the full
However, no practical programming language
with structural subtyping
would implement the full
language of Section~
\ref
{
sec:syntax
}
, but rather restrict all
expressions of the form
$
\tcase
{
e
}{
t
}{
e
_
1
}{
e
_
2
}$
so that the type
$
t
$
tested in them is either
non functional (e.g., products, integer, a record type, etc.) or it is
$
\Empty\to\Any
$
(i.e., the expression can just test whether
$
e
$
returns a function
or not). There are multiple reasons to impose such a restriction, the
or not).
\footnote
{
%%%
\rev
{
%%%%%%
Of course, there exist languages in which it is
possible to check whether some value has a type that has functional
subcomponents---e.g., to test whether an object is of some class
that possess some given methods, but that is a case of nominal rather than
structural subtyping, which in our framework corresponds to testing
whether a value has some basic type.
}
%%%rev
}
There are multiple reasons to impose such a restriction, the
most important ones can be summarized as follows:
\begin{enumerate}
[left=0pt .. 12pt]
\item
For explicitly-typed languages it may yield conterintutive results,
...
...
conclusion.tex
View file @
48fbf168
...
...
@@ -45,10 +45,10 @@ made to converge and, foremost, whether it is of use in practice is among our ob
But the real challenges that lie ahead are the handling of side
effects and the addition of polymorphic types.
\rev
{
%%%
Our analysis works in
a
pure
system
and we already discussed at length at the end of the
Our analysis works in
pure
languages
and we already discussed at length at the end of the
previous section our plans to extend it to
cope with side-effects. However the
cope with side-effects. However
,
the
ultimate solution of integrating type and effect analysis in a unique tool
is not more defined than that.
}
%%%
...
...
related.tex
View file @
48fbf168
...
...
@@ -223,7 +223,7 @@ arguments are both integers, as in the body of the following function:
While our approach can correctly deduce for this function the type
$
\ANY\To\ANY\To\Int
$
, Kent's approach fails to type check it since
to type the ``then'' branch requires to deduce that the
application
\code
{
have
\_
same
\_
parity
\
,
x
}
returns the constant
application
\code
{
have
\_
same
\_
parity
\
;
x
}
returns the constant
function
\code
{
true
}
only if
\code
{
x
}
is an integer.
Finally, Kent's approach inherits all the advantages and
disadvantages that the logical propositions approach has with respect
...
...
scp-reviews-2108.tex
View file @
48fbf168
...
...
@@ -37,7 +37,7 @@
\newcommand
{
\done
}
[1]
{{
\color
{
darkblue
}
\paragraph
{
\sc
Done.
}
#1
\newline
}}
\newcommand
{
\notdone
}
[1]
{{
\color
{
darkblue
}
\paragraph
{
\sc
Not Done.
}
#1
\newline
}}
\newcommand
{
\To
}{{
\to
}}
\author
{}
...
...
@@ -47,9 +47,9 @@
\begin{document}
\maketitle
\begin{abstract}
We reproduce in this document the reviews in their
i
nt
egrali
ty and
We reproduce in this document the reviews in their
e
nt
ire
ty and
we add
\textcolor
{
darkblue
}{
\em
in blue and italics
}
how each part
was taken into account in our revision, or the answer to direct
was taken into account in our revision, or the answer
s
to direct
questions by the reviewers
\end{abstract}
...
...
@@ -180,11 +180,11 @@ in light of the topic and of the fact that it heavily relies on semantic
subtyping. Probably a consequence of the pandemic.
Of course, the new version of the related work section includes now a
detailed compar
a
ison with the (indeed highly related) chapter 5 of the
detailed comparison with the (indeed highly related) chapter 5 of the
dissertations, see lines (??-??) 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
inver
s
ed ``arrow'': read it from right to left).
inver
t
ed ``arrow'': read it from right to left).
About that, we take the opportunity that the reviewer disclosed the fact
that he is Kent's supervisor to signal a small error that we think we
may have spotted in the dissertation: in Figure 5.2, describing the
...
...
@@ -194,13 +194,23 @@ 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\Empty
\\
\end
{
array
}
\]
That is, we have applied the formula
$
inv
(
\tau
_
f,
\sigma
_{
our
}
)
=
domain
(
\tau
_
f
)
\setminus
\tau
_
a
$
with
\\
$
\begin
{
array
}{
rcl
}
\tau
_
f
&
=
&
((
\True\To\False
)
\land
(
\False\To\True
))
\lor
((
\True\To\True
)
\land
(
\False\To\False
))
\\
\sigma
_{
out
}
&
=
&
\True\\
domain
(
\tau
_
f
)
&
=
&
\Bool\\
\tau
_
a
&
=
&
\True\lor\False
\end
{
array
}$
However, a function with a type
$
((
\True\to\False
)
\land
(
\False\to\True
))
\lor
((
\True\to\True
)
\land
(
\False\to\False
))
$
may
definitively yield a result in
$
\True
$
or in
$
\False
$
. The correct result should be
\Bool
.
definitively yield a result in
$
\True
$
or in
$
\False
$
. The correct
result should be
\Bool
{}
rather than
\Empty
.
The proof in Coq of the soundness of this definition given in the
...
...
@@ -211,7 +221,9 @@ intersections of arrows and of negations thereof.
If we change the union at issue into an intersection, it becomes
equivalent to our algorithmic definition of
\emph
{
worra
}
(p13) as it can
be verified by a simple application of De Morgan's Laws.
be verified by a simple application of De Morgan's Laws. In that case
the formula yield
$
\tau
_
a
=
\True\land\False
=
\Empty
$
and we obtain the
correct result
$
\Bool\setminus\Empty
=
\Bool
$
.
We would be grateful if the reviewer could confirm that we did not
misinterpret the definition in the dissertation. If it is so, was the
...
...
@@ -307,7 +319,7 @@ 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: ??-??)
More generally, we also went more in depth in the compar
a
ison with the
More generally, we also went more in depth in the comparison with the
logical approach by THF, to highlight further limitations of our
approach as requested by the reviewers.
\end{answer}
...
...
@@ -384,13 +396,13 @@ unneeded:
\begin{answer}
We agree with the reviewer on the fact that
interdepedent tests do not seem to appear in real
examples. The ex
e
mple we give page 6 to justify the need of
interdepe
n
dent tests do not seem to appear in real
examples. The ex
a
mple 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 theorical point of view, we think that it is
Still, in a theor
et
ical 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
...
...
@@ -456,7 +468,7 @@ system (the only one that can reconstruct intersection types for
functions) cannot do it.
If we explicitly annotate the function with this intersection type
then the function type-checks in all system
e
s.
then the function type-checks in all systems.
If we rewrite the function so that it has just a single argument of type
\texttt
{
(Int,Int)
$
\lor
$
(String,String)
}
, that is
...
...
@@ -476,7 +488,7 @@ Flow and in TypeScript.
So we do not really understand the purpose of the example, unless 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 re
a
mark of the reviewer,we added a
correct interpretation of the remark of the reviewer,we added a
comment in lines ???-???
\end{answer}
...
...
@@ -518,8 +530,9 @@ type preservation). We rewrote the sentence to be more clear.
``counterintutive result'' happen but this seem not so
counter-intutitive in a nominal type system.
\begin{answer}
Kim: Yes, indeed, in case of nominal typing
you can test values (e.g., objects) with functional components
We gave for granted that we were speaking of systems with structural
subtyping and not, as evoked by the reviewer, nominal subtyping. We
added a footnote to remove any possible ambiguity
\end{answer}
\item
on p17, Undef is chosen to be a constant not in
\any
. But
\any
was
...
...
@@ -532,9 +545,9 @@ 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 expla
i
nation (see lines
interpretation of)
\any
. We added an explanation (see lines
???-???). In short
\texttt
{
Undef
}
is a special singleton type
whose intepretation contains only a the
whose inte
r
pretation contains only a the
constant
\texttt
{
undef
}
which is not in
$
\Domain
$
.
\end{answer}
...
...
@@ -562,7 +575,7 @@ string).\]
removing the first arrow of the intersection would yield less a
precise type: applying the function to an argu
e
ment of type
precise type: applying the function to an argument of type
$
\texttt
{
number
}
\land
?
$
would yield a result of the same type which by a
cast could be used in every context where a strict subtype of
\texttt
{
number
}
is expected, which becomes impossible if we remove
...
...
@@ -585,7 +598,7 @@ The paper presents four extensions to occurrence typing. First, it
allows refinement of arbitrary expressions (thus removing the refined
variable can only be at top level). Second, it allows for inference of
intersection types. Third, it combines occurrence typing with dynamic
tests and particular, gradual typing. Finally, it formali
s
es these
tests and particular, gradual typing. Finally, it formali
z
es these
concepts in a language with records and proves meta-theoretical
properties.
...
...
@@ -603,7 +616,7 @@ system {[}23{]}.
\subsection*
{
Analysis of the submission
}
\label
{
analysis-of-the-submission
}
This is a very well written paper that addresses an interesting subject,
i.e., practical features of occurence typing. The work comes with both
i.e., practical features of occur
r
ence typing. The work comes with both
the metatheory (that shows soundness of the system) and the
implementation (that showcases the applicability of the new features).
But, as detailed below, existing related work in not compared against
...
...
@@ -671,8 +684,8 @@ the new contributions.
\end{answer}
\end{itemize}
\begin{answer}
We have further develop
p
ed the our section of the related work on
refinment types, using the given references has a starting point.
We have further developed the our section of the related work on
refin
e
ment types, using the given references has a starting point.
\end{answer}
\item
\textbf
{
Meta-theory Clarifications:
}
...
...
@@ -681,7 +694,7 @@ refinment types, using the given references has a starting point.
running time of the algorithmic type checking is missing. Of course,
the addressed problem (inference of intersections types) is difficult
and the proposed type checking can diverge. The authors state (at pg
14) that ``in practi
s
e the problem is a very mild one'' but some
14) that ``in practi
c
e the problem is a very mild one'' but some
discussion on the expected running time of the algorithm in practise
is missing.
\begin{answer}
...
...
@@ -693,36 +706,37 @@ refinment types, using the given references has a starting point.
Since the paper is motivated by the TypeScript and Flow
systems, I expected that their system would be evaluated against
these. Instead, section 4 evaluates against
{
[
}
23
{
]
}
and states that
the new system ``goes beyond what languages like TypeScipt and Flow
the new system ``goes beyond what languages like TypeSc
r
ipt and Flow
do''. Yet, the cost of the new features is not discussed. Is 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
We can surely answer to the second question, whet
h
er users are
required to write more annotations. The answer is an unambig
u
ous
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
that can be captured by our approach (e.g., that
do
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.
better comparison with related work. We also added at the end of
Section 4 a new example the we capture and for which Flow and
TypeScript fail.
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
such as the cited one
s
with what our system could give if
it
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.
instance, 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
(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
...
...
@@ -731,9 +745,9 @@ refinment types, using the given references has a starting point.
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?)
intersection.(shall we add such a sente
n
ce somewhere?)
Likewise ...
Likewise ...
TO BE CONTINUED
\end{answer}
...
...
@@ -860,7 +874,11 @@ languages seems to make at least some amount of mutation unavoidable in
practice.
\begin{answer}
Beppe: voire reponse sur side-effects
We added at the end of the section on related work (Section 5) a long
discussion on side-effects: how our approach positions on this aspect
w.r.t. the current literature, how it is already possible, by some
naive solutions, to cope with them and which are our future plans for
a better integration.
\end{answer}
It is also worth noting that the paper contains many different elements,
...
...
@@ -871,9 +889,6 @@ language would apply'', there is a brief discussion of an extension with
records, with (functional) field modification support, and all of this
amounts to several rather different language/calculus designs.
\begin{answer}
SKIP
\end{answer}
You could perhaps say that the type system is somewhat accidental:
Whenever something doesn't work, we'll fiddle with it. The outcome is a
...
...
@@ -883,7 +898,30 @@ but it may still be useful to consider how and to which degree it can be
refuted.
\begin{answer}
BOH????
Sincerely, in the context of the current research on occurrence typing
we believe that our work is an important step forward exactly in the
opposite direction you cite. We try to give a type-theoretic
foundation to occurrence typing. Let us just cut
\&
paste the words of
the first reviewer:
\emph
{
this is a big simplification of prior work
on occurrence typing [..] in a discipline where we can rarely re-use
theorems, [this work] does a nice job of extending prior work while
also keeping the prior results.
}
We couldn't have said better. Our
work is not satisfactory yet, in our opinion, because it still needs
non standard type-environments that map expressions rather than
variables to types. But all the rest is standard type-theory (and we
are confident that we can get rid also of the few last non-standard
features). Compare now this with existing work. The work of Typed
Racket does a really good job in giving a foundation to occurrence typing,
but still it uses types with logical predicates and pointers to type
environments (the latter akin to what we do), and tailors its analysis to a
predefined set of pure expressions and to truthy and false
results. But, hands down, it works on a real widely used programming
language. 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 failed and that after a couple of months were fixed
and magically worked in one or the other.
\end{answer}
Finally, the implementation section makes me think that the flow
...
...
@@ -894,8 +932,18 @@ typing/inference? (that is, would you still be able to produce the
function types which are intersections of arrow types?)
\begin{answer}
Beppe: one does not exclude the other
\ldots
{}
see answer about the
different approaches of reviewer 1
We believe that flow analysis will be probably necessary to handle
side-effects but also that the examples we currently fail to capture
are not a limitation of a type theoretic approach but rather of the
way we currently implemented it. The culprit is that we start and
limit occurrence typing only from/to type-case: every dependency
that comes from the context of a type-case is thus lost. But if we
can apply occurrence typing also on other expressions, by splitting
the types of these expressions not only because they are tested by a
type-case but also because it is interesting to do it 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.
\end{answer}
All in all, this is a very interesting paper, technically convincing,
...
...
@@ -949,7 +997,7 @@ allowed to diverge on any input.
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
sp
e
cific 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
...
...
@@ -965,7 +1013,7 @@ 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.
$
t
\to
t'
$
(whatever
$
t'
$
) since the implication vac
u
ously holds.
\end{answer}
\item
...
...
@@ -989,7 +1037,7 @@ 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 expla
i
nation and given a reference for a thorough
We added an explanation and given a reference for a thorough
discussion (lines ??-??)
\end{answer}
...
...
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