related.tex 23 KB
 Kim Nguyễn committed Jul 09, 2019 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 committed Jul 03, 2019 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.  Kim Nguyễn committed Jul 09, 2019 11 }  Kim Nguyễn committed Feb 26, 2020 12 13 14 \kim{Need to clean-up and insert at the right place. }  Giuseppe Castagna committed Jul 09, 2019 15   Giuseppe Castagna committed Jul 10, 2019 16   Kim Nguyễn committed Jul 09, 2019 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 committed Jul 10, 2019 20 \citet{THF10} define $\lambda_{\textit{TR}}$, a core calculus for  Giuseppe Castagna committed Sep 20, 2021 21 Typed Racket. In this language types are annotated by two logical  Giuseppe Castagna committed Jul 10, 2019 22 propositions that record the type of the input depending on the  Kim Nguyễn committed Jul 09, 2019 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 committed Sep 20, 2021 25 the argument has type {\tt Number}, and when the output is {\tt false}, the  Kim Nguyễn committed Jul 09, 2019 26 argument does not. Such information is used selectively  Giuseppe Castagna committed Jul 10, 2019 27 in the then'' and else'' branches of a test. One area where their  Giuseppe Castagna committed Jul 10, 2019 28 work goes further than ours is that the type information also flows  Kim Nguyễn committed Jul 09, 2019 29 outside of the tests to the surrounding context. In contrast, our type  Giuseppe Castagna committed Jul 10, 2019 30 system only refines the type of variables strictly in the branches of a  Giuseppe Castagna committed Sep 20, 2021 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  Kim Nguyễn committed Jul 09, 2019 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 committed Sep 20, 2021 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 committed Jul 10, 2019 67 allows us to type all but two of their key examples (the notable  Giuseppe Castagna committed Sep 20, 2021 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 committed Feb 26, 2020 75 $(\texttt{number}\times(\texttt{number}\cup\texttt{bool}))\cup  Giuseppe Castagna committed Sep 20, 2021 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  Kim Nguyễn committed Feb 26, 2020 81 types, we also type precisely the deletion of labels, which, as far as  Giuseppe Castagna committed Feb 26, 2020 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  Kim Nguyễn committed Feb 26, 2020 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  Kim Nguyễn committed Jul 09, 2019 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 committed Jul 10, 2019 92 write predicates over list types (e.g., test whether the input  Kim Nguyễn committed Jul 09, 2019 93 is a list of integers), which we can easily do thanks to our support  Kim Nguyễn committed Feb 26, 2020 94 for recursive types.}  Giuseppe Castagna committed Jul 11, 2019 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 committed Jul 10, 2019 98   Giuseppe Castagna committed Sep 15, 2021 99 100 101  \rev{%%% For what concerns the first work by~\citet{THF08} it is interesting to  Giuseppe Castagna committed Sep 15, 2021 102 compare it with our work because the comparison shows two rather  Giuseppe Castagna committed Sep 15, 2021 103 different approaches to deal with the property of type  Giuseppe Castagna committed Sep 15, 2021 104 preservation. \citet{THF08} define a first type system that does not  Giuseppe Castagna committed Sep 15, 2021 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 committed Sep 15, 2021 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 committed Sep 15, 2021 118 system does not have the problem of the first system of~\cite{THF08}  Giuseppe Castagna committed Sep 15, 2021 119 thanks to the  Giuseppe Castagna committed Sep 15, 2021 120 presence of the \Rule{Efq} rule, that we included for that very purpose,  Giuseppe Castagna committed Sep 15, 2021 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 committed Sep 15, 2021 144 different language designs and arguing about their usefulness.  Giuseppe Castagna committed Sep 15, 2021 145 146 }%%%rev  Giuseppe Castagna committed Sep 20, 2021 147 148 149 150  \rev{%%%  Giuseppe Castagna committed Sep 21, 2021 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 committed Sep 21, 2021 154 subtyping~\cite{Frisch2008}. Kent's work builds on the approach  Giuseppe Castagna committed Sep 21, 2021 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 committed Sep 21, 2021 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 committed Sep 21, 2021 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 committed Sep 21, 2021 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 committed Sep 21, 2021 175 yields false, then the logical proposition \texttt{x${\in}\neg$Bool} holds true. The definition  Giuseppe Castagna committed Sep 21, 2021 176 of our \emph{worra} operator that we gave in equation~\eqref{worra} is, in  Giuseppe Castagna committed Sep 21, 2021 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 committed Sep 21, 2021 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 committed Sep 21, 2021 184 of worra, given in~\eqref{worralgo}, works for any function, in  Giuseppe Castagna committed Sep 21, 2021 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 committed Sep 21, 2021 191 holistic approach since, not only our analysis strives to infer type  Giuseppe Castagna committed Sep 21, 2021 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 committed Sep 22, 2021 195 196 restricted set of expressions). For instance, we use the operator worra also to refine the type of the function in an application (see  Giuseppe Castagna committed Sep 23, 2021 197 discussion in Section~\ref{sec:ideas}) while in Kent's approach  Giuseppe Castagna committed Sep 21, 2021 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 committed Sep 22, 2021 201 test, such as in \texttt{number?\,(f\,x)}, then in Kent's approach it is no longer possible  Giuseppe Castagna committed Sep 21, 2021 202 to refine the information on the argument \texttt{x}. The latter is  Giuseppe Castagna committed Sep 22, 2021 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 committed Sep 21, 2021 205 206 207 208 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).  Giuseppe Castagna committed Sep 23, 2021 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 That said the very fact of focusing on truthy vs.\ false results may make Kent's analysis fail even for pure Boolean tests where it would be expected to work---e.g., if a result must be true rather than just truthy. For example, consider the polymophic function that when applied to two integers returns whether they have the same parity and false otherwise: \code{have\_same\_parity:$(\Int\To\Int\To\Bool)\land(\neg\Int\To\ANY\To\False)\land(\ANY\To\neg\Int\To\False)$}. We can imagine to use this function to implicitly test whether two arguments are both integers, as in the body of the following function: }%%%rev \begin{alltt}\color{darkblue} let f = fun (x : Any) -> fun (y : Any) -> if have\_same\_parity x y is True then add x y else 0 \end{alltt} \rev{%%% 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 function \code{true} only if \code{x} is an integer.  Giuseppe Castagna committed Sep 21, 2021 228 229 230 231 232 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 committed Sep 20, 2021 233 234 235 }%%%rev  Kim Nguyễn committed Feb 28, 2020 236 237 238 239 240 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 committed Feb 26, 2020 241 language featuring a {\tt SELECT}-like construct over  Kim Nguyễn committed Feb 28, 2020 242 243 collections. Types are mapped to first order formulæ and an SMT-solver is then used to (try to) prove their satisfiability. The refinement  Kim Nguyễn committed Feb 26, 2020 244 245 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 committed Mar 03, 2020 246 types). However, the system forgoes any notion (or just characterization) of completeness  Kim Nguyễn committed Feb 28, 2020 247 and the  Giuseppe Castagna committed Jul 08, 2020 248 subtyping algorithm is largely dependent on the subtle behavior of  Giuseppe Castagna committed Feb 26, 2020 249 the SMT solver (which may timeout or give an incorrect model that  Kim Nguyễn committed Feb 26, 2020 250 251 252 253 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 committed Mar 03, 2020 254 (resp. $\lnot e$) is true in $e_1$ (resp. $e_2$) and this information  Kim Nguyễn committed Feb 26, 2020 255 is not propagated to the outer context.  Giuseppe Castagna committed Feb 26, 2020 256 A similar approach is taken in \cite{Chugh12}, and extended to so-called nested refinement types. In these types, an arrow type may  Kim Nguyễn committed Feb 26, 2020 257 appear in a logical formula (where previous work only allowed formulae  Giuseppe Castagna committed Feb 26, 2020 258 on base types''). This is done in the context of a dynamic  Kim Nguyễn committed Feb 26, 2020 259 language and their approach is extended with polymorphism, dynamic  Kim Nguyễn committed Feb 28, 2020 260 dispatch and record types.  Kim Nguyễn committed Sep 22, 2021 261 262 263 264 265 266 267 268 269 270 \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 committed Sep 22, 2021 271 in \emph{administrative normal form} (\cite{F92}). Using a program  Kim Nguyễn committed Sep 22, 2021 272 273 274 275 276 277 278 279 280 281 282 283 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 ?}  Kim Nguyễn committed Feb 26, 2020 284   Giuseppe Castagna committed Jul 08, 2020 285 \citet{Kent16} bridge the gap between prior work on occurrence typing  Kim Nguyễn committed Feb 28, 2020 286 287 288 289 290 291 292 293 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 committed Mar 02, 2020 294 295 296 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  Kim Nguyễn committed Feb 28, 2020 297 in type predicates are verified by the SMT solver.  Giuseppe Castagna committed Jul 11, 2019 298 299 300  \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 committed Jul 11, 2019 301 implementation, they must account for aspects that we could afford to  Giuseppe Castagna committed Jul 11, 2019 302 303 304 305 306 307 308 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 committed Mar 03, 2020 309 we showed in \eqref{foo2}) which are used in \emph{ad hoc} manner by the type  Giuseppe Castagna committed Jul 11, 2019 310 311 312 313 314 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 committed Mar 03, 2020 315 rules look like classic ones and are easy to understand, unions are  Giuseppe Castagna committed Jul 11, 2019 316 317 318 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 committed Mar 02, 2020 319 solving). This is the reason why our system seems more adapted to study  Giuseppe Castagna committed Jul 11, 2019 320 321 322 323 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 committed Jul 11, 2019 324 325 \nocite{typescript,flow}  Giuseppe Castagna committed Sep 21, 2021 326 327 \rev{%%% We end this presentation of related work with a discussion on side  Giuseppe Castagna committed Sep 22, 2021 328 effects. Although in our system we did not take into account  Giuseppe Castagna committed Sep 22, 2021 329 330 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 committed Sep 22, 2021 331 332 333 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 committed Sep 22, 2021 334 noticed, one can distinguish the approaches that use types to reason about  Giuseppe Castagna committed Sep 22, 2021 335 the dynamic behavior of programs according to the set of expressions  Giuseppe Castagna committed Sep 22, 2021 336 337 338 339 340 341 342 343 344 345 346 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 committed Sep 22, 2021 347 348 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 committed Sep 22, 2021 349 350 351 352 353 354 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 committed Sep 22, 2021 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 (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.  Giuseppe Castagna committed Sep 21, 2021 390 }%%%rev