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
1ea39487
Commit
1ea39487
authored
Sep 22, 2021
by
Giuseppe Castagna
Browse files
more on revision
parent
c8f29f22
Changes
3
Hide whitespace changes
Inline
Side-by-side
intro.tex
View file @
1ea39487
...
...
@@ -99,8 +99,9 @@ will also yield two important byproducts. First, to refine the type of the
variables we have to refine the type of the expressions they occur in and
we can use this information to improve our analysis. Therefore our
occurrence typing approach will refine not only the types of variables
but also the types of generic expressions (bypassing usual type
inference). Second, and most importantly, the result of our analysis can be used to infer
but also the types of generic expressions--i.e., any expression
whatever form it has---bypassing usual type
inference. Second, and most importantly, the result of our analysis can be used to infer
intersection types for functions, even in the absence of precise type
annotations such as the one in the definition of
\code
{
foo
}
in~
\eqref
{
foo2
}
: to put it simply, we are able to
infer the type~
\eqref
{
eq:inter
}
for the unannotated pure JavaScript
...
...
related.tex
View file @
1ea39487
...
...
@@ -192,14 +192,16 @@ holistic approach since, not only our analysis strives to infer type
information by analyzing all types of results (and not
just
\texttt
{
False
}
or
\texttt
{$
\lnot
$
False
}
), but also it tries to
perform this analysis for all possible expressions (and not just for a
restricted set of expressions). So, for instance, in Kent's approach
restricted set of expressions). For instance, we use the operator
worra also to refine the type of the function in an application (see
discussion in Section~
\ref
{
sec:ideas
}
while in Kent's approach
the analysis of an application
\texttt
{
f
\,
x
}
refines the properties of
the argument
\texttt
{
x
}
but not of the function
\texttt
{
f
}
(as our
approach does); and when such an application is the argument of a type
test, such as in
\texttt
{
number?
\,
(f
\,
x)
}
, then it is no longer possible
test, such as in
\texttt
{
number?
\,
(f
\,
x)
}
, then
in Kent's approach
it is no longer possible
to refine the information on the argument
\texttt
{
x
}
. The latter is
not is a flaw of the approach but a design choice: as we explain
l
at
er
on, the
Type Racket
approach
non only focus on the inference of two logical
not is a flaw of the approach but a design choice: as we explain at
the end of this section, the approach of
Type Racket non only focus on the inference of two logical
propositions according to the truthy or false value of an expression,
but it does it only for a selected set of
\emph
{
pure
}
expressions of
the language, to cope with the possible presence of side effects (and
...
...
@@ -286,11 +288,40 @@ formalizing it in our system.
\rev
{
%%%
We end this presentation of related work with a discussion on side
effects. Even if in our system we did not take into account
side-effects
and actually our system works because all the expressions
of our language are pure
,
it is interesting to see how the different
approaches of gradual typing position with respect to the problem of
handling side-effect since
i
t better position our work in the taxonomy
side-effects
---
and actually our system works because all the expressions
of our language are pure
---
it is interesting to see how the different
approaches of gradual typing position
themselves
with respect to the problem of
handling side-effect
s,
since t
his helps to
better position our work in the taxonomy
of the current litterature. As Sam Tobin-Hochstadt insightfully
noticed ...
noticed, one can distinguish the approaches that use types to reason about
the dynamic behaviour of programs according to the set of expressions
that are taken into account by the analysis. In the case of occurrence
typing, this set is often determined by the way impure expressions are
taken into account. On one end of the spectrum lies our approach: our
analysis takes into account
\emph
{
all
}
expressions but, in its current
formulation, it works only for pure languages. On the other end of the
spectrum we find the approach of Typed Racket whose analysis reasons
about a limited and predetermined set of
\emph
{
pure
}
operations (all data structure
accessors). Somewhere in-between lies the approach of the
Flow language which, as hinted above, implements a complex effect systems to determine
pure expressions. While the system presented here does not work for
impure languages, we argue that its foundational nature predisposes it
to be adapted to handle impure expression, by adopting existing
solutions or providing new ones. For instance, it is not hard to
modify our system so that it takes into account only a set of
predetermined pure expressions, as done by Typed Racket: it suffices
to modify the definition of
$
\Gamma
\evdash
e
{
(
\neg
)
t
}
\Gamma
'
$
(cf.
\
Section~
\ref
{
sec:static
}
) so that
$
\Gamma
'
$
extends
$
\Gamma
$
with type hypotheses for all expressions occurring in
$
e
$
that are also in the set of predetermined pure expressions
(instead of for all subexpressions of
$
e
$
, tout court).
However such a solution would be mildly interesting since by excluding
from the analysis all functions application we would lose most of the
advantages of our approach with respect to the one of logical
propositions.
}
%%%rev
scp-reviews-2108.tex
View file @
1ea39487
...
...
@@ -33,15 +33,24 @@
\providecommand
{
\tightlist
}{
%
\setlength
{
\itemsep
}{
0pt
}
\setlength
{
\parskip
}{
0pt
}}
\newcommand
{
\semantic
}
[1]
{{
\llbracket
#1
\rrbracket
}}
\newcommand
{
\done
}
[1]
{{
\color
{
darkblue
}
\paragraph
{
\sc
Done.
}
#1
\newline
}}
\newcommand
{
\notdone
}
[1]
{{
\color
{
darkblue
}
\paragraph
{
\sc
Not Done.
}
#1
\newline
}}
\author
{}
\date
{}
\begin{document}
\maketitle
\begin{abstract}
We reproduce in this document the reviews in their integrality 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
questions by the reviewers
\end{abstract}
\section
{
Handling Editor's Comments:
}
...
...
@@ -169,7 +178,9 @@ subtyping. Probably a consequence of the pandemic.
Of course, the new version of the related work section includes now a
detailed comparaison with the (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.
inversion of Kent is, in the spirit, the same as our worra operator
(we do not know whether the reviewer noticed that ``worra'' is an
inversed ``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
...
...
@@ -348,14 +359,15 @@ unneeded:
as the paper says is all that is really needed.
\begin{answer}
We added a long discussion about it in the related
work section (lines ??-??) when comparing with
{
[
}
22
{
]
}
(TH-Felleisen 2008). In a nutshell we prefer starting with a
system that satisfies type preservation, define a sound but
not-complete algorithm and explore subsystems for which
completeness holds rather than (as in
{
[
}
22
{
]
}
) start with a
systeme that does not satisfy type preservation and then add
auxiliary rules to prove type preservation.
We added a long discussion to explain the reasons of our
choice. It is in the related work section (lines ??-??) 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
algorithm and explore subsystems for which completeness holds
rather than (as in
{
[
}
22
{
]
}
) start with a system that does
not satisfy type preservation and then add auxiliary rules to
prove type preservation.
\end{answer}
\item
...
...
@@ -765,8 +777,10 @@ is, or with small adjustments.
\subsection*
{
Detailed comments:
}
\indent
p3,10, `generic expressions': You have used this phrase a couple of
times at this point, please define it.
\done
{
(at its first occurrence)
}
p5,11, `intersect it with': Surely the next term
$
(
t
^
+
\to\neg
t
)
$
should be negated.
...
...
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