related.tex 22.1 KB
Newer Older
1
2
3
4
\kim{
I don't really know about these:\\
Occurrence typing is for variables in TypeScript, also paths in Flow. STRESS THE USE OF INTERSECTIONS AND UNIONS. ACTUALLY SPEAK OF UNION AND NEGATION (UNION FOR ALTERNATIVES, NEGATION FOR TYPING THE ELSE BRANCH AND THEREFORE WE GET INTERSECTION FOR FREE)
 extend to selectors, logical connectives, paths, and user
Giuseppe Castagna's avatar
Giuseppe Castagna committed
5
6
7
8
9
10
defined predicates.

[IMPORTANT: check the differences with what we do here]


State what we capture already, for instance lists since we have product and recursive types.
11
}
Kim Nguyễn's avatar
Kim Nguyễn committed
12
13
14
\kim{Need to clean-up and insert at the right place.
}

15

Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
16

17
18
19
Occurrence typing was introduced by \citet{THF08} and further advanced
in \cite{THF10} in the context of the Typed Racket language. This
latter work in particular is close to ours, with some key differences.
Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
20
\citet{THF10} define $\lambda_{\textit{TR}}$, a core calculus for
Giuseppe Castagna's avatar
Giuseppe Castagna committed
21
Typed Racket. In this language types are annotated by two logical
Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
22
propositions that record the type of the input depending on the
23
24
(Boolean) value of the output. For instance, the type of the
{\tt number?} function states that when the output is {\tt true}, then
Giuseppe Castagna's avatar
Giuseppe Castagna committed
25
the argument has type {\tt Number}, and when the output is {\tt false}, the
26
argument does not. Such information is used selectively
Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
27
in the ``then'' and ``else'' branches of a test. One area where their
Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
28
work goes further than ours is that the type information also flows
29
outside of the tests to the surrounding context. In contrast, our type
Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
30
system only refines the type of variables strictly in the branches of a
Giuseppe Castagna's avatar
Giuseppe Castagna committed
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
test.
\rev{This is particularly beneficial when typing functions since the
logical propositions of Tobin-Hochstadt and Felleisen can record
dependencies on expressions other than the input of a
function. Consider for instance the following example (due
to~\cite{kent19phd}) in JavaScript \code{function
is-y-a-number(x) \{ return(typeof(y)\,===\,"number") \}} which defines
a functions that
disregards its argument and returns whether the variable \code{y} is
an integer or not.\footnote{Although such a function may appear
nonsensical, Kent~\cite{kent19phd} argues that it corresponds a programming
patter that may occurr in Typed Racked due to the the expansion of some
sophisticated macro definitions.} While our approach cannot deduce for this function but the
type $\Any\to\Bool$, the logical approach of Tobin-Hochstadt and
Felleisen can record in the type of \code{is-y-a-number} that fact
when the function returns \texttt{true} then \code{y} is a number, and
the opposite when it returns \texttt{false}. In our approach, the only
possibility to track such a dependency is that the variable \code{y}
is the parameter of an outer function to which our analysis could give
an overloaded type by splitting the type \texttt{Any} of \texttt{y}
into \texttt{Number} and \texttt{$\neg$Number}. Under the hypothesis
of \texttt{y} being of type \texttt{Number} the type inferred
for \code{is-y-a-number} will then be $\Any\to\True$, and
$\Any\to\False$ otherwise, thus capturing the wanted dependency.
%
Although the approach of using logical proposition has the undeniable
advantage over ours of providing more a flow sensitive analysis, we
believe that using semantic subtyping as a foundation as we do
has also several merits over the logical proposition approach.
}%%%rev
First, in our case, type
62
63
predicates are not built-in. A user may define any type predicate she
wishes by using an overloaded function, as we have shown in
Giuseppe Castagna's avatar
Giuseppe Castagna committed
64
65
66
Section~\ref{sec:practical}. Second, in our setting, {\em types\/}
play the role of formulæ. Using set-theoretic types, we can express
the complex types of variables without resorting to a meta-logic. This
Kim Nguyễn's avatar
.    
Kim Nguyễn committed
67
allows us to type all but two of their key examples (the notable
Giuseppe Castagna's avatar
Giuseppe Castagna committed
68
69
70
71
72
73
74
exceptions being Example~9 and 14 in their paper, which use the
propagation of type information outside of the branches of a
test). While Typed Racket supports structured data types such as pairs
and records only unions of such types can be expressed at the level of
types, and even for those, subtyping is handled axiomatically. For
instance, for pairs, the subtyping rule presented in \cite{THF10} is
unable to deduce that
Kim Nguyễn's avatar
Kim Nguyễn committed
75
$(\texttt{number}\times(\texttt{number}\cup\texttt{bool}))\cup
Giuseppe Castagna's avatar
Giuseppe Castagna committed
76
77
78
79
80
(\texttt{bool}\times (\texttt{number}\cup\texttt{bool}))$ is a subtype
of (and actually equal to)
$((\texttt{number}\cup\texttt{bool})\times\texttt{number})\cup
((\texttt{number}\cup\texttt{bool})\times\texttt{bool})$ (and likewise
for other type constructors combined with union types). For record
81
types, we also type precisely the deletion of labels, which, as far as
Giuseppe Castagna's avatar
Giuseppe Castagna committed
82
83
we know no other system can do. On the other hand, the propagation of
logical properties defined in \cite{THF10} is a powerful tool, that
84
85
86
87
88
can be extended to cope with sophisticated language features such as
the multi-method dispatch of the Closure language \cite{Bonn16}.

\kim{Remove or merge :
Also, while they
89
90
91
extend their core calculus with pairs, they only provide a simple {\tt
cons?} predicate that allows them to test whether some value is a
pair. It is therefore unclear whether their systems allows one to
Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
92
write predicates over list types (e.g., test whether the input
93
is a list of integers), which we can easily do thanks to our support
94
for recursive types.}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
95
96
97
%Further, as far as we know, a code analysis such as the
%one performed by Code 8 for extensible records is not handled by the
%current typing systems.
Kim Nguyễn's avatar
.    
Kim Nguyễn committed
98

Giuseppe Castagna's avatar
Giuseppe Castagna committed
99
100
101

\rev{%%%
For what concerns the first work by~\citet{THF08} it is interesting to
Giuseppe Castagna's avatar
Giuseppe Castagna committed
102
compare it with our work because the comparison shows two rather
Giuseppe Castagna's avatar
Giuseppe Castagna committed
103
different approaches to deal with the property of type
Giuseppe Castagna's avatar
Giuseppe Castagna committed
104
preservation. \citet{THF08} define a first type system that does not
Giuseppe Castagna's avatar
Giuseppe Castagna committed
105
106
satisfy type-preservation. The reason for that is that this first type
system checks all the branches of a type-case expression,
Giuseppe Castagna's avatar
Giuseppe Castagna committed
107
108
109
110
111
112
113
114
115
116
117
independently from whether they are selectable or not; this may
result in a well-typed expression to reduce to an expression that 
is not well-typed because it contains a type-case expression with
a branch that, due to the reduction, became both non-selectable
and ill-typed (see \cite[Section 3.3]{THF08}). To obviate this problem
they introduce a \emph{second} type system that extends the previous
one with some auxiliary typing rules that type type-case expressions
by skipping the typing of non-selectable branches. They use this
second type system only to prove type preservation and obtain, thus,
the soundness of their type system. In our work, instead, we prefer to
start directly with a system that satisfies type preservation. Our
Giuseppe Castagna's avatar
typeos    
Giuseppe Castagna committed
118
system does not have the problem of the first system of~\cite{THF08}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
119
thanks to the
Giuseppe Castagna's avatar
typeos    
Giuseppe Castagna committed
120
presence of the \Rule{Efq} rule, that we included for that very purpose,
Giuseppe Castagna's avatar
Giuseppe Castagna committed
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
that is, to skip non-selectable branches during typing. The choice of one
or the other approach is mostly a matter of taste and, in this specific case,
boils down to deciding whether some typing problems must be
signaled at compile time by an error or a warning. The approach
of~\citet{THF08} ensures that every subexpression of a program is
well-typed and, if not, it generates a type-error. Our approach allows
some subexpressions of a program to be ill-typed, but only if they
occur in dead branches of type-cases: in that case any reasonable
implementation would flag a warning to signal the presence of the dead
branches. The very same reasons that explain the presence in our system
of \Rule{Eqf}, explain why from the beginning we included in our
system the typing rule \Rule{Abs-} that deduces negated arrow types:
we wanted a system that satisfied type preservation (albeit, for a
parallel reduction: cf: \Appendix\ref{app:parallel}). We then defined
an algorithmic system that is not \emph{complete} with respect to the
type-system but from which it inherits its soundness. Of course, we
could have proceeded as~\citet{THF08} did: start directly with a
type-system corresponding to the algorithm (i.e., omit the
rule \Rule{Abs-}) and later extend this system with the rule to infer
negated arrows, the only purpose of this extension being to prove type preservation. We preferred not
to, not only because we favor type preserving systems, but also
because in this way we were able to characterize different subsystems that
are complete with respect to the algorithmic system, thus exploring
Giuseppe Castagna's avatar
typeos    
Giuseppe Castagna committed
144
different language designs and arguing about their usefulness.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
145
146
}%%%rev

Giuseppe Castagna's avatar
Giuseppe Castagna committed
147
148
149
150



\rev{%%%
Giuseppe Castagna's avatar
Giuseppe Castagna committed
151
152
153
Highly related to our work is Andrew M.\ Kent's PhD.\
dissertation~\cite{kent19phd}, in particular its Chapter 5 whose title
is ``A set-theoretic foundation for occurrence typing'' where he endows the logical techniques of~\cite{THF10} with the set-theoretic types of semantic
Giuseppe Castagna's avatar
Giuseppe Castagna committed
154
subtyping~\cite{Frisch2008}. Kent's work builds on the approach
Giuseppe Castagna's avatar
Giuseppe Castagna committed
155
156
developed for Typed Racket that, as recalled above, consists in enriching the
types of the expressions with information to track under which hypotheses an expression
Giuseppe Castagna's avatar
Giuseppe Castagna committed
157
158
159
160
161
162
163
164
165
166
167
168
169
170
returns false or not (it considers every non false value to be
``truthy''). This tracking is performed by recording in the type of
the expression two logical propositions that hold when the expression
evaluates to false or not, respectively. The work in~\citet[Chapter
5]{kent19phd} uses set-theoretic types to express type predicates (a
predicate that holds only for a type $t$ has type
$p:(t\to\texttt{True})\land(\neg t\to\texttt{False})$) as well as to
express in a more compact (and, sometimes, more precise) way the types
of several built-in Typed Racket functions. It also uses the
properties of set-theoretic types to deduce the logical types (i.e.,
the propositions that hold when an expressions produces \texttt{false}
or not) of arguments of function applications.  To do that it defines
a type operator called \emph{function application inversion}, that
determines the largest subset of the domain of a function for which an
Giuseppe Castagna's avatar
Giuseppe Castagna committed
171
172
application yields a result of a given type $t$, and then uses it for
the special cases when the type $t$ is either \texttt{False} or \texttt{$\lnot$False} so
Giuseppe Castagna's avatar
Giuseppe Castagna committed
173
174
as to determine the logical type of the argument. For instance, this
operator can be used to deduce that if the application \texttt{boolean?\,x}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
175
yields false, then the logical proposition \texttt{x${\in}\neg$Bool} holds true. The definition
Giuseppe Castagna's avatar
Giuseppe Castagna committed
176
of our \emph{worra} operator that we gave in equation~\eqref{worra} is, in
Giuseppe Castagna's avatar
Giuseppe Castagna committed
177
178
its spirit, the same as Kent's \emph{function application inversion}
operator (more precisely, the same as the operator \textsf{pred} Kent defines in Figure
Giuseppe Castagna's avatar
Giuseppe Castagna committed
179
180
181
182
183
5.7 of his dissertation), even though the two operators were defined independently from
each other. The exact definitions however are slightly different, since
the algorithm given in~\citet[Figure 5.2]{kent19phd}
for \emph{function application inversion} works only for functions
whose type is an intersection of arrows, whereas our definition
Giuseppe Castagna's avatar
Giuseppe Castagna committed
184
of worra, given in~\eqref{worralgo}, works for any function, in
Giuseppe Castagna's avatar
Giuseppe Castagna committed
185
186
187
188
189
190
particular, for functions that have a union type, too. The main
difference of Kent's approach with respect to ours is that, since it
builds on the logical propositions approach, then it focus the use of
set-theoretic types and of the worra (or application inversion)
operator to determine when an expression yields a result of
type \texttt{False} or \texttt{$\lnot$False}. We have instead a more
Giuseppe Castagna's avatar
Giuseppe Castagna committed
191
holistic approach since, not only our analysis strives to infer type
Giuseppe Castagna's avatar
Giuseppe Castagna committed
192
193
194
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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
195
196
197
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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
198
199
200
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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
201
test, such as in \texttt{number?\,(f\,x)}, then in Kent's approach it is no longer possible
Giuseppe Castagna's avatar
Giuseppe Castagna committed
202
to refine the information on the argument \texttt{x}. The latter is
Giuseppe Castagna's avatar
Giuseppe Castagna committed
203
204
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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
205
206
207
208
209
210
211
212
213
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
applications do not belong to this set since they can be be impure).
Finally, Kent's approach inherits all the advantages and
disadvantages that the logical propositions approach has with respect
to ours (e.g., flow sensitive analysis vs.\ user defined type
predicates) that we already discussed at the beginning of this
section.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
214
215
216
}%%%rev


Giuseppe Castagna's avatar
Giuseppe Castagna committed
217
218
219
220
\rev{HERE STRESS THAT THE WORK ON SOLVERS IS IN THE SAME VEIN AS THE
WORK OF TYPED RACKET THAT TRACKS FOR EXPRESSIONS WHEN THEY RETURN
FALSE AND WHEN NOT.
}
221
222
223
224
225
Another direction of research related to ours is the one of semantic
types. In particular, several attempts have been made recently to map
types to first order formul\ae. In that setting, subtyping between
types translates to logical implication between formul\ae.
\citet{Bierman10} introduce Dminor, a data-oriented
Giuseppe Castagna's avatar
Giuseppe Castagna committed
226
language featuring a {\tt SELECT}-like construct over
227
228
collections.  Types are mapped to first order formulæ and an SMT-solver is
then used to (try to) prove their satisfiability. The refinement
229
230
types they present go well beyond what can be expressed with the set-theoretic
types we use (as they allow almost any pure expression to occur in
Giuseppe Castagna's avatar
Giuseppe Castagna committed
231
types). However, the system forgoes any notion (or just characterization) of completeness
232
and the
Giuseppe Castagna's avatar
Giuseppe Castagna committed
233
subtyping algorithm is largely dependent on the subtle behavior of
Giuseppe Castagna's avatar
Giuseppe Castagna committed
234
the SMT solver (which may timeout or give an incorrect model that
235
236
237
238
cannot be used as a counter-example to explain the type-error).
As with our work, the typing rule for the {\tt if~$e$ then $e_1$ else
$e_2$} construct
of Dminor refines the type of each branch by remembering that $e$
Giuseppe Castagna's avatar
Giuseppe Castagna committed
239
(resp. $\lnot e$) is true in $e_1$ (resp. $e_2$) and this information
240
is not propagated to the outer context.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
241
A similar approach is taken in \cite{Chugh12}, and extended to so-called nested refinement types. In these types, an arrow type may
242
appear in a logical formula (where previous work only allowed formulae
Giuseppe Castagna's avatar
Giuseppe Castagna committed
243
on  ``base types''). This is done in the context of a dynamic
244
language and their approach is extended with polymorphism, dynamic
245
dispatch and record types.
246
247
248
249
250
251
252
253
254
255
\rev{A problem that is faced by refinement type systems is the one of
propagating in the branches of a test the information learned on
a \emph{sub-expression} of a tested expression. A solution
e.g. choosen by \cite{OTMW04} and \cite{KF09} is to devise a
meta-function that recursively explores both a type and an expression
and propagates the type information on the sub-expressions. This
process (called \emph{selfification} in the cited works) roughly
corresponds to our $\constrf$ function (see Section~\ref{sec:typenv}).
Another approach is the one followed by \cite{RKJ08} is based purely
on a program transformation, namely putting the the term
Kim Nguyễn's avatar
Kim Nguyễn committed
256
in \emph{administrative normal form} (\cite{F92}). Using a program
257
258
259
260
261
262
263
264
265
266
267
268
transformation, every destructor application (function application,
projection, \ldots) is given a name through a let-binding. The problem
of tracking precise type information for every sub-expression is
therefore reduced to the one of keeping precise typing information for
a variable.  While this solution seems appealing, it is not as
straightforward in our case. Indeed, to retain the same degree of
precision, we would need to identify alpha equivalent sub-expressions
and share the same binding, something that a plain A-normalisation
does not provide.
}
\rev{TODO Intersection + refinement}
\rev{TODO refinement + gradual ?}
269

Giuseppe Castagna's avatar
Giuseppe Castagna committed
270
\citet{Kent16} bridge the gap between prior work on occurrence typing
271
272
273
274
275
276
277
278
and SMT based (sub) typing. It introduces the $\lambda_{RTR}$ core calculus, an
extension of $\lambda_{TR}$ where the logical formulæ embedded in
types are not limited to built-in type predicates, but accept
predicates of arbitrary theories. This allows them to provide some
form of dependent typing (and in particular they provide an
implementation supporting bitvector and linear arithmetic theories).
The cost of this expressive power in types is however paid by the
programmer, who has to write logical
Giuseppe Castagna's avatar
Giuseppe Castagna committed
279
280
281
annotations (to help the external provers). Here, types and formul{\ae}
remain segregated. Subtyping of ``structural'' types is checked by
syntactic rules (as in \cite{THF10}) while logical formul{\ae} present
282
in type predicates are verified by the SMT solver.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
283
284
285

\citet{Cha2017} present the design and implementation of Flow by formalizing a relevant
fragment of the language. Since they target an industrial-grade
Giuseppe Castagna's avatar
typo    
Giuseppe Castagna committed
286
implementation, they must account for aspects that we could afford to
Giuseppe Castagna's avatar
Giuseppe Castagna committed
287
288
289
290
291
292
293
postpone to future work, notably side effects and responsiveness of
the type checker on very large code base. The degree of precision of
their analysis is really impressive and they achieve most of what we
did here and, since they perform flow analysis and use an effect
system (to track mutable variables), even more. However, this results
in a specific and very complex system. Their formalization includes
only union types (though, Flow accepts also intersection types as
Giuseppe Castagna's avatar
Giuseppe Castagna committed
294
we showed in \eqref{foo2}) which are used in \emph{ad hoc} manner by the type
Giuseppe Castagna's avatar
Giuseppe Castagna committed
295
296
297
298
299
system, for instance to type record types. This allows Flow to perform
an analysis similar to the one we did for Code 8 in
Table~\ref{tab:implem}, but also has as a consequence that in some
cases unions do not behave as expected. In contrast, our approach is
more classic and foundational: we really define a type system, typing
Giuseppe Castagna's avatar
Giuseppe Castagna committed
300
rules look like classic ones and are easy to understand, unions are
Giuseppe Castagna's avatar
Giuseppe Castagna committed
301
302
303
unions of values (and so are intersections and negations), and the
algorithmic part is---excepted for fix points---relatively simple
(algorithmically Flow relies on constraint generation and
Giuseppe Castagna's avatar
Giuseppe Castagna committed
304
solving). This is the reason why our system seems more adapted to study
Giuseppe Castagna's avatar
Giuseppe Castagna committed
305
306
307
308
and understand occurrence typing and to extend it with additional
features (e.g., gradual typing and polymorphism) and we are eager to
test how much of their analysis we can capture and enhance by
formalizing it in our system.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
309
310
\nocite{typescript,flow}
 
311
312
\rev{%%%
We end this presentation of related work with a discussion on side
Giuseppe Castagna's avatar
Giuseppe Castagna committed
313
effects. Although in our system we did not take into account
Giuseppe Castagna's avatar
Giuseppe Castagna committed
314
315
side-effects---and actually our system works because all the expressions
of our language are pure---it is interesting to see how the different
Giuseppe Castagna's avatar
Giuseppe Castagna committed
316
317
318
approaches of occurrence typing position themselves with respect to the problem of
handling side effects, since this helps to better place our work in the taxonomy
of the current literature. As Sam Tobin-Hochstadt insightfully
Giuseppe Castagna's avatar
Giuseppe Castagna committed
319
noticed, one can distinguish the approaches that use types to reason about
Giuseppe Castagna's avatar
Giuseppe Castagna committed
320
the dynamic behavior of programs according to the set of expressions
Giuseppe Castagna's avatar
Giuseppe Castagna committed
321
322
323
324
325
326
327
328
329
330
331
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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
332
333
to be adapted to handle impure expressions as well, by adopting existing
solutions or proposing new ones. For instance, it is not hard to
Giuseppe Castagna's avatar
Giuseppe Castagna committed
334
335
336
337
338
339
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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
(instead of extending it for all subexpressions of $e$, \emph{tout court}).
However, such a solution would be marginally interesting since by excluding
from the analysis all applications we would lose most of the
advantages of our approach with respect to the one with logical
propositions. Thus a more interesting solution would be to use some
external static analysis tools---e.g., to graft
the effect system of~\citet{Cha2017} on ours---to detect impure
expressions. The idea would be to mark different occurrences of a same
impure expression using different marks. These marks would essentially
be used to verify the presence of type hypotheses for a given
expression in a type environment $\Gamma$; the idea being that
expressions with different marks are to be considered as different
expressions and, therefore, would not share the same type
hypothesis. For instance, consider the test
$\ifty{f\,x}\Int{\,...\,}{\,...}$: if $f x$ were flagged as impure
then the occurrence of $f x$ in the ``then'' branch would not be
supposed to be of type $\Int$ since it would be typed in an
environment $\Gamma$ containing a binding for an $f\,x$ expression
having a mark different from the one in the ``then'' branch: the
regular typing rules would apply for $f\, x$ in that case. This
would certainly improve our analysis, but we believe that ultimately
our system should not resort to external static analysis tools to detect
impure expressions but, rather, it should integrate this analysis with
the typing one, so as to mark \emph{only} those impure expression
whose side-effects may affect the semantics of some type-cases. For
instance, consider a JavaScript object \code{obj} that we modify as
follows \code{obj["key"] = 3}. If the field \code{"key"} is already
present in \code{obj} with type \Int{} and we do not test it more than
about this type, then it is not necessary to mark different
occurrences of \code{obj} with different marks, since the result of
the type-case would not be changed by the assignment; the same holds
true if the field is absent but type-cases do not discriminate on its
presence. Otherwise, some occurrences of \code{obj} must use different
marks: the analysis will determine which ones. We leave this study for
future work.
375
}%%%rev