language2.tex 45.7 KB
 Giuseppe Castagna committed Jun 29, 2019 1 In this section we formalize the ideas we outlined in the introduction. We start by the definition of types followed by the language and its reduction semantics. The static semantics is the core of our work: we first present a declarative type system that deduces (possibly many) types for well-typed expressions and then the algorithms to decide whether according to it an expression is well typed or not.  Giuseppe Castagna committed Jun 24, 2019 2 3 4  \subsection{Types}  Giuseppe Castagna committed Jun 26, 2019 5 \begin{definition}[Types]\label{def:types} The set of types \types{} is formed by the terms $t$ coinductively produced by the following grammar  Giuseppe Castagna committed Jun 25, 2019 6 7 8 9 10 11 12 $\begin{array}{lrcl} \textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty \end{array}$ and that satisfy the following conditions \begin{itemize}  Giuseppe Castagna committed Jul 01, 2019 13 14 15 \item (regularity) every term has a finite number of different sub-terms; \item (contractivity) every infinite branch of a term contains an infinite number of occurrences of the arrow or product type constructors.  Giuseppe Castagna committed Jun 25, 2019 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 \end{itemize} \end{definition} We use the following abbreviations for types: $t_1 \land t_2 \eqdef \neg (\neg t_1 \vee \neg t_2)$, $t_ 1 \setminus t_2 \eqdef t_1 \wedge \neg t_2$, $\Any \eqdef \neg \Empty$. In the definition, $b$ ranges over basic types (\emph{eg}, \Int, \Bool), $\Empty$ and $\Any$ respectively denote the empty (that types no value) and top (that types all values) types. Coinduction accounts for recursive types and the condition on infinite branches bars out ill-formed types such as $t = t \lor t$ (which does not carry any information about the set denoted by the type) or $t = \neg t$ (which cannot represent any set). It also ensures that the binary relation $\vartriangleright \,\subseteq\!\types^{2}$ defined by $t_1 \lor t_2 \vartriangleright t_i$, $t_1 \land t_2 \vartriangleright  Giuseppe Castagna committed Jul 01, 2019 33 t_i$, $\neg t \vartriangleright t$ is Noetherian.  Giuseppe Castagna committed Jun 25, 2019 34 This gives an induction principle on $\types$ that we  Giuseppe Castagna committed Jul 01, 2019 35 will use without any further explicit reference to the relation.\footnote{In a nutshell, we can do proofs by induction on the structure of unions and negations---and, thus, intersections---but arrows, products, and basic types are the base cases for the induction.}  Giuseppe Castagna committed Jun 25, 2019 36 37 38 39 40 We refer to $b$, $\times$, and $\to$ as \emph{type constructors} and to $\lor$, $\land$, $\lnot$, and $\setminus$ as \emph{type connectives}. The subtyping relation for these types, noted $\leq$, is the one defined  Giuseppe Castagna committed Jun 26, 2019 41 by~\citet{Frisch2008} to which the reader may refer for more details. Its formal definition is recalled in Appendix~\ref{} and a detailed description of the algorithm to decide it can be found in~\cite{Cas15}.  Giuseppe Castagna committed Jun 25, 2019 42 43 44 For this presentation it suffices to consider that types are interpreted as sets of \emph{values} ({\emph{ie}, either constants, $\lambda$-abstractions, or pair of values: see  Giuseppe Castagna committed Jun 25, 2019 45 Section~\ref{sec:syntax} right below) that have that type, and that subtyping is set  Giuseppe Castagna committed Jun 25, 2019 46 47 48 containment (\emph{ie}, a type $s$ is a subtype of a type $t$ if and only if $t$ contains all the values of type $s$). In particular, $s\to t$ contains all $\lambda$-abstractions that when applied to a value of  Giuseppe Castagna committed Jun 28, 2019 49 type $s$, if their computation terminates, then they return a result of  Giuseppe Castagna committed Jun 25, 2019 50 51 52 53 54 55 56 type $t$ (\emph{eg}, $\Empty\to\Any$ is the set of all functions\footnote{\label{allfunctions}Actually, for every type $t$, all types of the form $\Empty{\to}t$ are equivalent and each of them denotes the set of all functions.} and $\Any\to\Empty$ is the set of functions that diverge on every argument). Type connectives (\emph{ie}, union, intersection, negation) are interpreted as the corresponding set-theoretic operators (\emph{eg},~$s\vee t$ is the  Giuseppe Castagna committed Jun 26, 2019 57 58 union of the values of the two types). We use $\simeq$ to denote the symmetric closure of $\leq$: thus $s\simeq t$ means that $s$ and $t$ denote the same set of values and, as such, they are semantically the same type.  Giuseppe Castagna committed Jun 25, 2019 59 60 61 62  \subsection{Syntax}\label{sec:syntax} The expressions $e$ and values $v$ of our language are the terms inductively generated by the following grammars: \label{expressions}  Giuseppe Castagna committed Jun 25, 2019 63 64 65 \begin{array}{lrclr} \textbf{Expr} &e &::=& c\alt x\alt ee\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt \pi_i e\alt(e,e)\alt\tcase{e}{t}{e}{e}\$1mm] \textbf{Values} &v &::=& c\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt (v,v)  Giuseppe Castagna committed Jun 25, 2019 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 \end{array} for i=1,2. In~\eqref{expressions}, c ranges over constants (\emph{eg}, \texttt{true}, \texttt{false}, \texttt{1}, \texttt{2}, ...) which are values of basic types (we use \basic{c} to denote the basic type of the constant c); x ranges over variables; (e,e) denote pairs and \pi_i e their projections; \tcase{e}{t}{e_1}{e_2} denotes the type-case expression that evaluates either e_1 or e_2 according to whether the value returned by e (if any) is of type t or not; \lambda^{\wedge_{i\in I}s_i\to t_i} x.e is a value of type \wedge_{i\in I}s_i\to t_i and denotes the function of parameter x and body e. An expression has an intersection type if and only if it has all the types that compose the intersection. Therefore, intuitively, \lambda^{\wedge_{i\in I}s_i\to t_i} x.e is a well-typed value if for all i{\in} I the hypothesis that x is of type s_i implies that the body e has type t_i, that is to say, it is well typed if \lambda^{\wedge_{i\in I}s_i\to t_i} x.e has type s_i\to  Giuseppe Castagna committed Jun 28, 2019 83 84 t_i for all i\in I. Every value is associated to a type: the type of c is \basic c; the type of \lambda^{\wedge_{i\in I}s_i\to t_i} x.e is \wedge_{i\in I}s_i\to t_i; and, inductively,  Giuseppe Castagna committed Jun 25, 2019 85 86 the type of a pair of values is the product of the types of the values.  Giuseppe Castagna committed Jun 24, 2019 87 88 89   Giuseppe Castagna committed Jun 26, 2019 90 \subsection{Dynamic semantics}\label{sec:opsem}  Giuseppe Castagna committed Jun 24, 2019 91   Giuseppe Castagna committed Jul 01, 2019 92 The dynamic semantics is defined as a classic left-to-right call-by-value reduction for a \lambda-calculus with pairs, enriched with specific rules for type-cases. We have the following notions of reduction:  Giuseppe Castagna committed Jun 25, 2019 93 94 95 96 97 98 99 100 101 102 \[ \begin{array}{rcll} (\lambda^{\wedge_{i\in I}s_i\to t_i} x.e)v &\reduces& e\subst x v\\ \pi_i(v_1,v_2) &\reduces& v_i & i=1,2\\ \tcase{v}{t}{e_1}{e_2} &\reduces& e_1 &v\in t\\ \tcase{v}{t}{e_1}{e_2} &\reduces& e_2 &v\not\in t\\ \end{array}$ The semantics of type-cases uses the relation $v\in t$ that we informally defined in the previous section. We delay its formal  Giuseppe Castagna committed Jul 01, 2019 103 definition to Section~\ref{sec:type-schemes} (where it deals with some corner cases for functional values). Context reductions are  Giuseppe Castagna committed Jun 25, 2019 104 105 106 107 108 109 110 defined by the following reduction contexts: $\Cx[] ::= [\,]\alt \Cx e\alt v\Cx \alt (\Cx,e)\alt (v,\Cx)\alt \pi_i\Cx\alt \tcase{\Cx}tee$ As usual we denote by $\Cx[e]$ the term obtained by replacing $e$ for the hole in the context $\Cx$ and we have that $e\reduces e'$ implies $\Cx[e]\reduces\Cx[e']$.  Giuseppe Castagna committed Jun 24, 2019 111 112 113  \subsection{Static semantics}  Giuseppe Castagna committed Jun 28, 2019 114 While the syntax and reduction semantics are, on the whole, pretty  Giuseppe Castagna committed Jun 25, 2019 115 116 standard, for the type system we will have to introduce several unconventional features that we anticipated in  Giuseppe Castagna committed Jun 26, 2019 117 Section~\ref{sec:challenges} and are at the core of our work. Let  Giuseppe Castagna committed Jun 25, 2019 118 119 120 121 122 123 124 125 126 127 us start with the standard part, that is the typing of the functional core and the use of subtyping given by the following typing rules: \begin{mathpar} \Infer[Const] { } {\Gamma\vdash c:\basic{c}} { } \quad \Infer[App] {  Giuseppe Castagna committed Jun 25, 2019 128  \Gamma \vdash e_1: \arrow {t_1}{t_2}\quad  Giuseppe Castagna committed Jun 25, 2019 129 130 131 132 133 134  \Gamma \vdash e_2: t_1 } { \Gamma \vdash {e_1}{e_2}: t_2 } { } \quad \Infer[Abs+]  Giuseppe Castagna committed Jun 25, 2019 135  {{\scriptstyle\forall i\in I}\quad\Gamma,x:s_i\vdash e:t_i}  Giuseppe Castagna committed Jun 25, 2019 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164  { \Gamma\vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle \bigwedge_{i\in I}\arrow {s_i} {t_i} } { } % \Infer[If] % {\Gamma\vdash e:t_0\\ % %t_0\not\leq \neg t \Rightarrow % \Gamma \cvdash + e t e_1:t'\\ % %t_0\not\leq t \Rightarrow % \Gamma \cvdash - e t e_2:t'} % {\Gamma\vdash \ite {e} t {e_1}{e_2}: t'} % { } \\ \Infer[Proj] {\Gamma \vdash e:\pair{t_1}{t_2}} {\Gamma \vdash \pi_i e:t_i} { } \qquad \Infer[Pair] {\Gamma \vdash e_1:t_1 \and \Gamma \vdash e_2:t_2} {\Gamma \vdash (e_1,e_2):\pair {t_1} {t_2}} { } \qquad \Infer[Subs] { \Gamma \vdash e:t\\t\leq t' } { \Gamma \vdash e: t' } { } \qquad \end{mathpar}  Giuseppe Castagna committed Jun 26, 2019 165 These rules are quite standard and do not need any particular explanation besides those already given in Section~\ref{sec:syntax}. Just notice that we used a classic subsumption rule (\emph{ie}, \Rule{Subs}) to embed subtyping in the type system. Let us next focus on the unconventional aspects of our system, from the simplest to the hardest.  Giuseppe Castagna committed Jun 25, 2019 166   Giuseppe Castagna committed Jun 26, 2019 167 The first one is that, as explained in  Giuseppe Castagna committed Jun 26, 2019 168 169 170 Section~\ref{sec:challenges}, our type assumptions are about expressions. Therefore, the type environments in our rules, ranged over by $\Gamma$, map \emph{expressions}---rather than just variables---into  Giuseppe Castagna committed Jun 26, 2019 171 types. This explains why the classic typing rule for variables is replaced by a more general \Rule{Env} rule defined below:\beppe{Changed the name of Occ into Env since it seems more appropriate}  Giuseppe Castagna committed Jun 25, 2019 172 173 174 175 176 177 \begin{mathpar} \Infer[Env] { } { \Gamma \vdash e: \Gamma(e) } { e\in\dom\Gamma } \qquad  Giuseppe Castagna committed Jun 28, 2019 178  \Infer[Inter]  Giuseppe Castagna committed Jun 25, 2019 179 180 181 182  { \Gamma \vdash e:t_1\\\Gamma \vdash e:t_2 } { \Gamma \vdash e: t_1 \wedge t_2 } { } \end{mathpar}  Giuseppe Castagna committed Jun 28, 2019 183 The \Rule{Env} rule is coupled with the standard intersection introduction rule \Rule{Inter}  Giuseppe Castagna committed Jul 01, 2019 184 which allows us to deduce for a complex expression the intersection of  Giuseppe Castagna committed Jun 25, 2019 185 186 187 188 the types recorded by the occurrence typing analysis in the environment $\Gamma$ with the static type deduced for the same expression by using the other typing rules. This same intersection rule is also used to infer the second unconventional aspect of our  Giuseppe Castagna committed Jun 26, 2019 189 system, that is, the fact that $\lambda$-abstractions can have negated  Giuseppe Castagna committed Jul 01, 2019 190 arrow types, as long as these negated types do not make the type deduced for the function empty:  Giuseppe Castagna committed Jun 25, 2019 191 192 193 \begin{mathpar} \Infer[Abs-] {\Gamma \vdash \lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:t}  Giuseppe Castagna committed Jun 25, 2019 194  { \Gamma \vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\neg(t_1\to t_2) }  Giuseppe Castagna committed Jun 25, 2019 195 196  { (t\wedge\neg(t_1\to t_2))\not\simeq\Empty } \end{mathpar}  Giuseppe Castagna committed Jul 04, 2019 197 198 199 200 201 202 203 %\beppe{I have doubt: is this safe or should we play it safer and % deduce $t\wedge\neg(t_1\to t_2)$? In other terms is is possible to % deduce two separate negation of arrow types that when intersected % with the interface are non empty, but by intersecting everything % makes the type empty? It should be safe since otherwise intersection % would not be admissible in semantic subtyping (see Theorem 6.15 in % JACM), but I think we should doube ckeck it.}  Giuseppe Castagna committed Jun 26, 2019 204 As explained in Section~\ref{sec:challenges}, we need to be able to  Giuseppe Castagna committed Jun 25, 2019 205 206 207 208 209 210 211 deduce for, say, the function $\lambda^{\Int\to\Int} x.x$ a type such as $(\Int\to\Int)\wedge\neg(\Bool\to\Bool)$ (in particular, if this is the term $e$ in equation \eqref{bistwo} we need to deduce for it the type $(\Int\to\Int)\wedge\neg(\Int\to\neg\Int)$, that is, $(\Int\to\Int)\setminus(\Int\to\neg\Int)$ ). But the rule \Rule{Abs+} above does not allow us to deduce negations of arrows for abstractions: the rule \Rule{Abs-} makes this possible. As an aside, note that this kind  Giuseppe Castagna committed Jun 26, 2019 212 of deduction was already present in the system by~\citet{Frisch2008}  Giuseppe Castagna committed Jun 28, 2019 213 though it that system this deduction was motivated by the semantics of types rather than, as in our case,  Giuseppe Castagna committed Jun 25, 2019 214 215 216 217 218 by the soundness of the type system. Rules \Rule{Abs+} and \Rule{Abs-} are not enough to deduce for $\lambda$-abstractions all the types we wish. In particular, these rules alone are not enough to type general overloaded functions. For  Giuseppe Castagna committed Jun 26, 2019 219 instance, consider this simple example of a function that applied to an  Giuseppe Castagna committed Jun 25, 2019 220 integer returns its successor and applied to anything else returns  Giuseppe Castagna committed Jun 26, 2019 221 \textsf{true}:  Giuseppe Castagna committed Jun 25, 2019 222 $ Giuseppe Castagna committed Jun 26, 2019 223 \lambda^{(\Int\to\Int)\wedge(\neg\Int\to\Bool)} x\,.\,\tcase{x}{\Int}{x+1}{\textsf{true}}  Giuseppe Castagna committed Jun 25, 2019 224 $  Giuseppe Castagna committed Jun 26, 2019 225 Clearly, the expression above is well typed, but the rule \Rule{Abs+} alone  Giuseppe Castagna committed Jun 25, 2019 226 is not enough to type it. In particular, according to \Rule{Abs+} we  Giuseppe Castagna committed Jun 25, 2019 227 have to prove that under the hypothesis that $x$ is of type $\Int$ the expression  Giuseppe Castagna committed Jun 26, 2019 228 $(\tcase{x}{\Int}{x+1}{\textsf{true}})$ is of type $\Int$, too. That is, that under the  Giuseppe Castagna committed Jun 25, 2019 229 hypothesis that x has type $\Int\wedge\Int$ (we apply occurrence  Giuseppe Castagna committed Jun 26, 2019 230 typing) the expression $x+1$ is of type \Int{} (which holds) and that under the  Giuseppe Castagna committed Jun 25, 2019 231 hypothesis that $x$ has type $\Int\setminus\Int$, that is $\Empty$  Giuseppe Castagna committed Jun 26, 2019 232 233 (we apply once more occurrence typing), \textsf{true} is of type \Int{} (which \emph{does not} hold). The problem is that we are trying to type the  Giuseppe Castagna committed Jun 28, 2019 234 second case of a type-case even if we know that there is no chance that, when $x$ is bound to an integer,  Giuseppe Castagna committed Jun 26, 2019 235 236 that case will be ever selected. The fact that it is never selected is witnessed by the presence of a type hypothesis with $\Empty$ type. To  Giuseppe Castagna committed Jun 25, 2019 237 avoid this problem (and type the term above) we add the rule  Giuseppe Castagna committed Jun 26, 2019 238 239 240 \Rule{Efq} (\emph{ex falso quodlibet}) that allows the system to deduce any type for an expression that will never be selected, that is, for an expression whose type environment contains an empty assumption:  Giuseppe Castagna committed Jun 25, 2019 241 242 243 244 245 246 \begin{mathpar} \Infer[Efq] { } { \Gamma, (e:\Empty) \vdash e': t } { } \end{mathpar}  Giuseppe Castagna committed Jun 26, 2019 247 248 249 Once more, this kind of deduction was already present in the system by~\citet{Frisch2008} to type full fledged overloaded functions, though it was embedded in the typing rule for the type-case. Here we  Giuseppe Castagna committed Jun 26, 2019 250 need the rule \Rule{Efq}, which is more general, to ensure the  Giuseppe Castagna committed Jun 26, 2019 251 property of subject reduction.\beppe{Example?}  Giuseppe Castagna committed Jun 25, 2019 252   Giuseppe Castagna committed Jun 26, 2019 253 254 255 Finally, there is one last rule in our type system, the one that implements occurrence typing, that is, the rule for the type-case:\beppe{Changed to \Rule{If} to \Rule{Case}}  Giuseppe Castagna committed Jun 25, 2019 256 257 258 259 260  \begin{mathpar} \Infer[Case] {\Gamma\vdash e:t_0\\ %t_0\not\leq \neg t \Rightarrow  Mickael Laurent committed Jun 27, 2019 261  \Gamma \evdash e t \Gamma_1 \\ \Gamma_1 \vdash e_1:t'\\  Giuseppe Castagna committed Jun 25, 2019 262  %t_0\not\leq t \Rightarrow  Mickael Laurent committed Jun 27, 2019 263  \Gamma \evdash e {\neg t} \Gamma_2 \\ \Gamma_2 \vdash e_2:t'}  Giuseppe Castagna committed Jun 25, 2019 264 265  {\Gamma\vdash \tcase {e} t {e_1}{e_2}: t'} { }  Giuseppe Castagna committed Jun 25, 2019 266 \end{mathpar}  Giuseppe Castagna committed Jun 28, 2019 267 268 269 270 271 272 273 274 275 276 277 278 The rule \Rule{Case} checks whether the expression $e$, whose type is being tested, is well-typed and then performs the occurrence typing analysis that produces the environments $\Gamma_i$'s under whose hypothesis the expressions $e_i$'s are typed. The production of these environments is represented by the judgments $\Gamma \evdash e {(\neg)t} \Gamma_i$. The intuition is that when $\Gamma \evdash e t \Gamma_1$ is provable then $\Gamma_1$ is a version of $\Gamma$ extended with type hypotheses for all expressions occurring in $e$, type hypotheses that can be deduced assuming that the test $e\in t$ succeeds. Likewise, $\Gamma \evdash e {\neg t} \Gamma_2$ (notice the negation on $t$) extends $\Gamma$ with the hypothesis deduced assuming that $e\in\neg t$, that is, for when the test $e\in t$ fails.  Giuseppe Castagna committed Jun 25, 2019 279   Giuseppe Castagna committed Jun 26, 2019 280 All it remains to do is to show how to deduce judgments of the form  Mickael Laurent committed Jun 27, 2019 281 $\Gamma \evdash e t \Gamma'$. For that we first have to define how  Giuseppe Castagna committed Jun 26, 2019 282 283 to denote occurrences of an expression. These are identified by paths in the syntax tree of the expressions, that is, by possibly empty strings of  Giuseppe Castagna committed Jun 26, 2019 284 285 286 287 288 289 290 characters denoting directions starting from the root of the tree (we use $\epsilon$ for the empty string/path, which corresponds to the root of the tree). Let $e$ be an expression and $\varpi\in\{0,1,l,r,f,s\}^*$ a \emph{path}; we denote $\occ e\varpi$ the occurrence of $e$ reached by the path $\varpi$, that is  Giuseppe Castagna committed Jun 25, 2019 291 $ Giuseppe Castagna committed Jun 28, 2019 292 \begin{array}{l}  Giuseppe Castagna committed Jun 25, 2019 293 294 295 296 297 298 299 \begin{array}{r@{\downarrow}l@{\quad=\quad}l} e&\epsilon & e\\ e_0e_1& i.\varpi & \occ{e_i}\varpi\qquad i=0,1\\ (e_0,e_1)& l.\varpi & \occ{e_0}\varpi\\ (e_0,e_1)& r.\varpi & \occ{e_1}\varpi\\ \pi_1 e& f.\varpi & \occ{e}\varpi\\ \pi_2 e& s.\varpi & \occ{e}\varpi\\  Giuseppe Castagna committed Jun 28, 2019 300 301 \end{array}\\ \text{undefined otherwise}  Giuseppe Castagna committed Jun 25, 2019 302 303 \end{array}$  Giuseppe Castagna committed Jun 28, 2019 304   Giuseppe Castagna committed Jun 25, 2019 305   Giuseppe Castagna committed Jun 25, 2019 306 307 To ease our analysis we used different directions for each kind of term. So we have $0$ and $1$ for the function and argument of an  Giuseppe Castagna committed Jun 28, 2019 308 application, $l$ and $r$ for the $l$eft and $r$ight expressions forming a pair,  Giuseppe Castagna committed Jul 01, 2019 309 310 and $f$ and $s$ for the argument of a $f$irst or of a $s$econd projection. Note also that we do not consider occurrences under $\lambda$'s (since their type is frozen in their annotations) and type-cases (since they reset the analysis).\beppe{Is it what I wrote here true?}  Giuseppe Castagna committed Jun 28, 2019 311   Mickael Laurent committed Jun 27, 2019 312 The judgments $\Gamma \evdash e t \Gamma'$ are then deduced by the following two rules:  Giuseppe Castagna committed Jun 25, 2019 313 314 315 316 317 318 319 320 321 322 323 324 \begin{mathpar} % \Infer[Base] % { \Gamma \vdash e':t' } % { \Gamma \cvdash p e t e':t' } % { } % \qquad % \Infer[Path] % { \pvdash \Gamma p e t \varpi:t_1 \\ \Gamma,(\occ e \varpi:t_1) \cvdash p e t e':t_2 } % { \Gamma \cvdash p e t e':t_2 } % { } \Infer[Base] { }  Mickael Laurent committed Jun 27, 2019 325  { \Gamma \evdash e t \Gamma }  Giuseppe Castagna committed Jun 25, 2019 326 327 328  { } \qquad \Infer[Path]  Mickael Laurent committed Jun 27, 2019 329 330  { \pvdash {\Gamma'} e t \varpi:t' \\ \Gamma \evdash e t \Gamma' } { \Gamma \evdash e t \Gamma',(\occ e \varpi:t') }  Giuseppe Castagna committed Jun 25, 2019 331  { }  Giuseppe Castagna committed Jun 25, 2019 332 \end{mathpar}  Giuseppe Castagna committed Jun 26, 2019 333 334 335 336 337 338 These rules describe how to produce by occurrence typing the type environments while checking that an expression $e$ has type $t$. They state that $(i)$ we can deduce from $\Gamma$ all the hypothesis already in $\Gamma$ (rule \Rule{Base}) and that $(ii)$ if we can deduce a given type $t'$ for a particular occurrence $\varpi$ of the expression $e$ being checked, than we can add this hypothesis to the produced type environment (rule \Rule{Path}). The rule  Giuseppe Castagna committed Jun 28, 2019 339 \Rule{Path} uses a (last) auxiliary judgement $\pvdash {\Gamma} e t  Giuseppe Castagna committed Jun 26, 2019 340 \varpi:t'$ to deduce the type $t'$ of the occurrence $\occ e \varpi$ when  Giuseppe Castagna committed Jun 26, 2019 341 342 343 344 345 checking $e$ against $t$ under the hypotheses $\Gamma$. This rule \Rule{Path} is subtler than it may appear at first sight, insofar as the deduction of the type for $\varpi$ may already use some hypothesis on $\occ e \varpi$ (in $\Gamma'$) and, from an algorithmic viewpoint, this will imply the computation of a fix-point (see Section~\ref{sec:typenv}). The last ingredient for our type system is the deduction of the  Giuseppe Castagna committed Jun 28, 2019 346 judgements of the form $\pvdash {\Gamma} e t \varpi:t'$ where  Giuseppe Castagna committed Jun 26, 2019 347 $\varpi$ is a path to an expression occurring in $e$. This is given by the following set  Giuseppe Castagna committed Jun 25, 2019 348 349 350 351 of rules. \begin{mathpar} \Infer[PSubs]  Mickael Laurent committed Jun 27, 2019 352 353  { \pvdash \Gamma e t \varpi:t_1 \\ t_1\leq t_2 } { \pvdash \Gamma e t \varpi:t_2 }  Giuseppe Castagna committed Jun 25, 2019 354  { }  Giuseppe Castagna committed Jun 26, 2019 355  \qquad  Giuseppe Castagna committed Jun 28, 2019 356  \Infer[PInter]  Mickael Laurent committed Jun 27, 2019 357 358  { \pvdash \Gamma e t \varpi:t_1 \\ \pvdash \Gamma e t \varpi:t_2 } { \pvdash \Gamma e t \varpi:t_1\land t_2 }  Giuseppe Castagna committed Jun 26, 2019 359  { }  Giuseppe Castagna committed Jun 25, 2019 360 361 362  \\ \Infer[PTypeof] { \Gamma \vdash \occ e \varpi:t' }  Mickael Laurent committed Jun 27, 2019 363  { \pvdash \Gamma e t \varpi:t' }  Giuseppe Castagna committed Jun 25, 2019 364 365  { } \qquad  Mickael Laurent committed Jun 27, 2019 366  \Infer[PEps]  Giuseppe Castagna committed Jun 25, 2019 367  { }  Mickael Laurent committed Jun 27, 2019 368  { \pvdash \Gamma e t \epsilon:t }  Giuseppe Castagna committed Jun 25, 2019 369 370 371 372  { } \qquad \\ \Infer[PAppR]  Mickael Laurent committed Jun 27, 2019 373 374  { \pvdash \Gamma e t \varpi.0:\arrow{t_1}{t_2} \\ \pvdash \Gamma e t \varpi:t_2'} { \pvdash \Gamma e t \varpi.1:\neg t_1 }  Giuseppe Castagna committed Jun 26, 2019 375  { t_2\land t_2' \simeq \Empty }  Giuseppe Castagna committed Jun 25, 2019 376 377  \\ \Infer[PAppL]  Mickael Laurent committed Jun 27, 2019 378 379  { \pvdash \Gamma e t \varpi.1:t_1 \\ \pvdash \Gamma e t \varpi:t_2 } { \pvdash \Gamma e t \varpi.0:\neg (\arrow {t_1} {\neg t_2}) }  Giuseppe Castagna committed Jun 25, 2019 380 381 382  { } \qquad \Infer[PPairL]  Mickael Laurent committed Jun 27, 2019 383 384  { \pvdash \Gamma e t \varpi:\pair{t_1}{t_2} } { \pvdash \Gamma e t \varpi.l:t_1 }  Giuseppe Castagna committed Jun 25, 2019 385 386 387  { } \\ \Infer[PPairR]  Mickael Laurent committed Jun 27, 2019 388 389  { \pvdash \Gamma e t \varpi:\pair{t_1}{t_2} } { \pvdash \Gamma e t \varpi.r:t_2 }  Giuseppe Castagna committed Jun 25, 2019 390 391 392  { } \qquad \Infer[PFst]  Mickael Laurent committed Jun 27, 2019 393 394  { \pvdash \Gamma e t \varpi:t' } { \pvdash \Gamma e t \varpi.f:\pair {t'} \Any }  Giuseppe Castagna committed Jun 25, 2019 395 396 397  { } \qquad \Infer[PSnd]  Mickael Laurent committed Jun 27, 2019 398 399  { \pvdash \Gamma e t \varpi:t' } { \pvdash \Gamma e t \varpi.s:\pair \Any {t'} }  Giuseppe Castagna committed Jun 25, 2019 400 401 402  { } \qquad \end{mathpar}  Giuseppe Castagna committed Jun 26, 2019 403 404 405 These rules implement the analysis described in Section~\ref{sec:ideas} for functions and extend it to products. Let us comment each rule in detail. \Rule{PSubs} is just subsumption for  Giuseppe Castagna committed Jun 28, 2019 406 the deduction $\vdashp$. The rule \Rule{PInter} combined with  Giuseppe Castagna committed Jun 26, 2019 407 408 \Rule{PTypeof} allows the system to deduce for an occurrence $\varpi$ the intersection of the static type of $\occ e \varpi$ (deduced by  Giuseppe Castagna committed Jun 28, 2019 409 410 411 \Rule{PTypeof}) with the type deduced for $\varpi$ by the other $\vdashp$ rules. The rule \Rule{PEps} is the starting point of the analysis: if we are assuming that the test $e\in t$ succeeds, then we can assume that $e$ (\emph{ie}, $\occ e\epsilon$) has type $t$ (recall that assuming that the test $e\in t$ fails corresponds to having $\neg t$ at the index of the turnstyle).  Mickael Laurent committed Jun 27, 2019 412 The rule \Rule{PApprR} implements occurrence typing for  Giuseppe Castagna committed Jun 26, 2019 413 414 415 416 417 418 419 420 the arguments of applications, since it states that if a function maps arguments of type $t_1$ in results of type $t_2$ and an application of this function yields results (in $t'_2$) that cannot be in $t_2$ (since $t_2\land t_2' \simeq \Empty$), then the argument of this application cannot be of type $t_1$. \Rule{PAppR} performs the occurrence typing analysis for the function part of an application, since it states that if an application has type $t_2$ and the argument of this application has type $t_1$, then the function in this application cannot have type $t_1\to\neg t_2$. Rules \Rule{PPair\_}  Giuseppe Castagna committed Jun 28, 2019 421 are straightforward since they state that the $i$-th projection of a pair  Giuseppe Castagna committed Jul 01, 2019 422 that is of type $\pair{t_1}{t_2}$ must be of type $t_i$. So are the last two  Giuseppe Castagna committed Jun 26, 2019 423 424 425 426 427 428 rules that essentially state that if $\pi_1 e$ (respectively, $\pi_2 e$) is of type $t'$, then the type of $e$ must be of the form $\pair{t'}\Any$ (respectively, $\pair\Any{t'}$). This concludes the presentation of our type system, which satisfies the property of soundness, deduced, as customary, from the properties  Giuseppe Castagna committed Jul 05, 2019 429 of progress and subject reduction, whose proofs are given in Appendix~\ref{app:soundness}.  Giuseppe Castagna committed Jun 26, 2019 430 \begin{theorem}[soundness]  Giuseppe Castagna committed Jun 26, 2019 431 432 433 For every expression $e$ such that $\varnothing\vdash e:t$ either $e$ diverges or there exists a value $v$ of type $t$ such that $e\reduces^* v$.  Giuseppe Castagna committed Jun 26, 2019 434 \end{theorem}  Giuseppe Castagna committed Jun 25, 2019 435 436 437 438 439   Giuseppe Castagna committed Jun 24, 2019 440 441 442  \subsection{Algorithmic system}  Giuseppe Castagna committed Jun 26, 2019 443 444 445 446 447 The system we defined in the previous section implements the ideas we illustrated in the introduction and it is sound. Now the problem is to decide whether an expression is well typed or not, that is, to find an algorithm that given a type environment $\Gamma$ and an expression $e$ decides whether there exists a type $t$ such that $\Gamma\vdash e:t$  Giuseppe Castagna committed Jun 28, 2019 448 449 is provable. For that we need to solve essentially two problems: $(i)$~how to handle the fact that it is possible to deduce several  Giuseppe Castagna committed Jun 29, 2019 450 types for the same well-typed expression and $(ii)$~how to compute the  Giuseppe Castagna committed Jun 26, 2019 451 452 453 454 455 456 457 458 auxiliary deduction system for paths. Multiple types have two distinct origins each requiring a distinct technical solution. The first origin is the rule \Rule{Abs-} by which it is possible to deduce for every well-typed lambda abstractions infinitely many types, that is the annotation of the function intersected with as many negations of arrow types as it is possible without making the type empty. To handle this multiplicity we use and  Giuseppe Castagna committed Jun 29, 2019 459 adapt the technique of \emph{type schemes} defined  Giuseppe Castagna committed Jun 28, 2019 460 by~\citet{Frisch2008}. Type schemes---whose definition we recall in Section~\ref{sec:type-schemes}---are canonical representations of  Giuseppe Castagna committed Jun 29, 2019 461 the infinite sets of types of $\lambda$-abstractions. The second origin is due  Giuseppe Castagna committed Jun 28, 2019 462 to the presence of structural rules\footnote{\label{fo:rules}In logic, logical rules  Giuseppe Castagna committed Jun 26, 2019 463 464 465  refer to a particular connective (here, a type constructor, that is, either $\to$, or $\times$, or $b$), while identity rules (e.g., axioms and cuts) and structural rules (e.g., weakening and  Giuseppe Castagna committed Jun 28, 2019 466  contraction) do not.} such as \Rule{Subs} and \Rule{Inter}. We  Giuseppe Castagna committed Jun 26, 2019 467 handle it in the classic way: we define an algorithmic system that  Giuseppe Castagna committed Jun 29, 2019 468 tracks the miminum type---actually, the minimum \emph{type scheme}---of an  Giuseppe Castagna committed Jun 28, 2019 469 470 expression; this system is obtained from the original system by eliminating the two structural rules and by distributing suitable checks of the subtyping  Giuseppe Castagna committed Jun 26, 2019 471 relation in the remaining rules. To do that in the presence of  Giuseppe Castagna committed Jun 28, 2019 472 473 set-theoretic types we need to define some operators on types, which are given in Section~\ref{sec:typeops}.  Giuseppe Castagna committed Jun 26, 2019 474 475  For what concerns the use of the auxiliary derivation for the   Giuseppe Castagna committed Jun 28, 2019 476 477 478 479 judgments, we present in Section~\ref{sec:typenv} an algorithm for which we prove the property of soundness and a limited form of completeness. All these notions are then used in the algorithmic typing system given in Section~\ref{sec:algorules}.  Giuseppe Castagna committed Jun 24, 2019 480   Giuseppe Castagna committed Jun 26, 2019 481 482 483 %% \beppe{\begin{enumerate} %% \item type of functions -> type schemes %% \item elimination rules (app, proj,if) ->operations on types and how to compute them  Giuseppe Castagna committed Jun 28, 2019 484 %% \item not syntax directed: rules Subs, Inter, Env.  Giuseppe Castagna committed Jun 26, 2019 485 486 487 %% \item Compute the environments for occurrence typing. Algorithm to compute $\Gamma\vdash\Gamma$ %% \end{enumerate} %% }  Giuseppe Castagna committed Jun 24, 2019 488 489   Giuseppe Castagna committed Jun 25, 2019 490 \subsubsection{Type schemes}\label{sec:type-schemes}  Giuseppe Castagna committed Jun 29, 2019 491 We introduce the new syntactic category of \emph{types schemes} which are the terms~$\ts$ inductively produced by the following grammar.  Giuseppe Castagna committed Jun 26, 2019 492 493 494 495 496 $\begin{array}{lrcl} \textbf{Type schemes} & \ts & ::= & t \alt \tsfun {\arrow t t ; \cdots ; \arrow t t} \alt \ts \tstimes \ts \alt \ts \tsor \ts \alt \tsempty \end{array}$  Giuseppe Castagna committed Jun 27, 2019 497 Type schemes denote sets of types, as formally stated by the following definition:  Giuseppe Castagna committed Jun 26, 2019 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 \begin{definition}[Interpretation of type schemes] We define the function $\tsint {\_}$ that maps type schemes into sets of types. \begin{align*} \begin{array}{lcl} \tsint t &=& \{s\alt t \leq s\}\\ \tsint {\tsfunone {t_i} {s_i}_{i=1..n}} &=& \{s\alt \exists s_0 = \bigwedge_{i=1..n} \arrow {t_i} {s_i} \land \bigwedge_{j=1..m} \neg (\arrow {t_j'} {s_j'}).\ \Empty \not\simeq s_0 \leq s \}\\ \tsint {\ts_1 \tstimes \ts_2} &=& \{s\alt \exists t_1 \in \tsint {\ts_1}\ \exists t_2 \in \tsint {\ts_2}.\ \pair {t_1} {t_2} \leq s\}\\ \tsint {\ts_1 \tsor \ts_2} &=& \{s\alt \exists t_1 \in \tsint {\ts_1}\ \exists t_2 \in \tsint {\ts_2}.\ {t_1} \vee {t_2} \leq s\}\\ \tsint \tsempty &=& \varnothing \end{array} \end{align*} \end{definition} Note that $\tsint \ts$ is closed under subsumption and intersection  Giuseppe Castagna committed Jun 29, 2019 516  and that $\tsempty$, which denotes the  Giuseppe Castagna committed Jun 27, 2019 517 empty set of types is different from $\Empty$ whose interpretation is  Giuseppe Castagna committed Jun 26, 2019 518 519 the set of all types.  Giuseppe Castagna committed Jun 28, 2019 520 \begin{lemma}[\cite{Frisch2008}]  Giuseppe Castagna committed Jun 26, 2019 521 522 523 524 525 526 527 528 529 530 531 532 533  Let $\ts$ be a type scheme and $t$ a type. It is possible to decide the assertion $t \in \tsint \ts$, which we also write $\ts \leq t$. \end{lemma} We can now formally define the relation $v\in t$ used in Section~\ref{sec:opsem} to define the dynamic semantics of the language. First, we associate each (possibly, not well-typed) value to a type schema representing the best type information about the value. By induction on the definition of values: $\tyof c {} = \basic c$, $\tyof {\lambda^{\wedge_{i\in I}s_i\to t_i} x.e}{}= \tsfun{s_i\to t_i}_{i\in I}$, $\tyof {(v_1,v_2)}{} = \tyof {v_1}{}\tstimes\tyof {v_1}{}$. Then we have $v\in t\iffdef \tyof v{}\leq t$.  Giuseppe Castagna committed Jun 26, 2019 534   Giuseppe Castagna committed Jun 27, 2019 535 We also need to perform intersections of type schemes so as to intersect the static type of an expression (\emph{ie}, the one deduced by conventional rules) with the one deduced by occurrence typing (\emph{ie}, the one derived by $\vdashp$). For our algorithmic system (see \Rule{Env$_{\scriptscriptstyle\mathcal{A}}$} in Section~\ref{sec:algorules}) all we need to define is the intersection of a type scheme with a type:  Giuseppe Castagna committed Jun 28, 2019 536 \begin{lemma}[\cite{Frisch2008}]  Giuseppe Castagna committed Jun 26, 2019 537 538 539  Let $\ts$ be a type scheme and $t$ a type. We can compute a type scheme, written $t \tsand \ts$, such that $$\tsint {t \tsand \ts} = \{s \alt \exists t' \in \tsint \ts.\ t \land t' \leq s \}$$ \end{lemma}  Giuseppe Castagna committed Jun 27, 2019 540 Finally, given a type schema it is straightforward to choose in its interpretation a type which serves as the canonical representative of the set:  Giuseppe Castagna committed Jun 26, 2019 541 542 543 544 545 546 547 548 549 550 551 552 553 554 \begin{definition}[Representative] We define a function $\tsrep {\_}$ that maps every non-empty type scheme into a type, \textit{representative} of the set of types denoted by the scheme. \begin{align*} \begin{array}{lcl} \tsrep t &=& t\\ \tsrep {\tsfunone {t_i} {s_i}_{i\in I}} &=& \bigwedge_{i\in I} \arrow {t_i} {s_i}\\ \tsrep {\ts_1 \tstimes \ts_2} &=& \pair {\tsrep {\ts_1}} {\tsrep {\ts_2}}\\ \tsrep {\ts_1 \tsor \ts_2} &=& \tsrep {\ts_1} \vee \tsrep {\ts_2}\\ \tsrep \tsempty && \textit{undefined} \end{array} \end{align*} \end{definition} Note that $\tsrep \ts \in \tsint \ts$.  Giuseppe Castagna committed Jun 26, 2019 555   Giuseppe Castagna committed Jun 24, 2019 556   Giuseppe Castagna committed Jun 29, 2019 557 \beppe{The explaination that follows is redundant with Section~\ref{sec:ideas}. Harmonize!}  Giuseppe Castagna committed Jun 24, 2019 558   Giuseppe Castagna committed Jun 26, 2019 559 \subsubsection{Operators for type constructors}\label{sec:typeops}  Giuseppe Castagna committed Jun 27, 2019 560 561  In order to define the algorithmic typing of expressions like  Giuseppe Castagna committed Jun 28, 2019 562 applications and projections we need to define the operators on  Giuseppe Castagna committed Jun 27, 2019 563 564 565 566 567 568 569 570 571 572 573 574 575 576 types we used in Section~\ref{sec:ideas}. Consider the rule \Rule{App} for applications. It essentially does three things: $(1)$ it checks that the function has functional type; $(2)$ it checks that the argument is in the domain of the function, and $(3)$ it returns the type of the application. In systems without set-theoretic types these operations are quite straightforward: $(1)$ corresponds to checking that the function has an arrow type, $(2)$ corresponds to checking that the argument is in the domain of the arrow deduced for the function and $(3)$ corresponds to returning the codomain of that same arrow. With set-theoretic types things are more difficult since a function can be typed by, say, a union of intersection of arrows and negations of types. Checking that the function has a functional type is easy since it corresponds to checking that it has a type subtype of $\Empty\to\Any$. Determining its domain and the type of the application is more complicated. For  Giuseppe Castagna committed Jun 28, 2019 577 instance, imagine we have a function of type \code{$$t=(\Int \to \Int)$$ $$\wedge$$ $$(\Bool \to \Bool)$$}, which  Giuseppe Castagna committed Jun 27, 2019 578 579 580 581 denotes functions that will return an integer if applied to an integer, and will return a Boolean if applied to a Boolean. It is possible to compute the domain of such a type (i.e., of the functions of this type), denoted by  Giuseppe Castagna committed Jul 01, 2019 582 $$\dom{t} = \Int \vee \Bool$$,  Giuseppe Castagna committed Jun 27, 2019 583 584 585 586 587 588 589 590 591 592 that is the union of all the possible input types. But what is the precise return type of such a function? It depends on what the argument of such a function is: either an integer or a Boolean---or both, denoted by the union type $$\Int\vee\Bool$$. This is computed by an operator we denote by $$\circ$$. More precisely, we denote by $$t_1\circ t_2$$ the type of an application of a function of type $$t_1$$ to an argument of type $$t_2$$. In the example with \code{$$t=(\Int \to \Int)$$ $$\wedge$$ $$(\Bool \to \Bool)$$}, it gives \code{$$t \circ \Int = \Int$$}, \code{$$t \circ \Bool = \Bool$$}, and  Giuseppe Castagna committed Jun 28, 2019 593 \code{$$t \circ (\Int\vee\Bool) = \Int \vee \Bool$$}. In summary, given a functional type $t$ (\emph{ie}, a type $t$ such that $t\leq\Empty\to\Any$) our algorithms will use the following three operators  Giuseppe Castagna committed Jun 26, 2019 594 595 596 \begin{eqnarray} \dom t & = & \max \{ u \alt t\leq u\to \Any\} \\  Giuseppe Castagna committed Jun 29, 2019 597 \apply t s & = &\,\min \{ u \alt t\leq s\to u\}  Giuseppe Castagna committed Jun 26, 2019 598 \\  Giuseppe Castagna committed Jun 29, 2019 599 \worra t s & = &\,\min\{u \alt t\circ(\dom t\setminus u)\leq \neg s\}\label{worra}  Giuseppe Castagna committed Jun 26, 2019 600 \end{eqnarray}  Giuseppe Castagna committed Jun 27, 2019 601 602  The first two operators belongs to the theory of semantic subtyping while the last one is new and we described it in Section~\ref{sec:ideas}  Giuseppe Castagna committed Jun 26, 2019 603   Giuseppe Castagna committed Jun 27, 2019 604 We need similar operators for projections since the type $t$ of $e$ in $\pi_i e$ may not be a single product type but, say, a union of products: all we know is that $t$ must be a subtype of $\pair\Any\Any$. So let $t$ be a type such that $t\leq\pair\Any\Any$, then we define:  Giuseppe Castagna committed Jun 26, 2019 605 606 607 608 \begin{eqnarray} \bpl t & = & \min \{ u \alt t\leq \pair u\Any\}\\ \bpr t & = & \min \{ u \alt t\leq \pair \Any u\} \end{eqnarray}  Giuseppe Castagna committed Jun 29, 2019 609 610 611 612 613 614 615 616 617 618 619 620 All the operators above but $\worra{}{}$ are already present in the theory of semantic subtyping: the reader can find how to compute them and how to extend their definition to type schemes in~\cite[Section 6.11]{Frisch2008}. Below we just show the formula that computes $\worra t s$ for a $t$ subtype of $\Empty\to\Any$. For that, we use a result of semantic subtyping that states that every type $t$ is equivalent to a type in disjunctive normal form and that if furthermore $t\leq\Empty\to\Any$, then $t \simeq \bigvee_{i\in I}\left(\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n')\right)$ with $\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n') \not\simeq \Empty$ for all $i$ in $I$. For such a $t$ and any type $s$ then we have:  Giuseppe Castagna committed Jun 27, 2019 621 622 623 624 625 % \worra t s = \dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P\subset P_i\alt s\leq \bigvee_{p \in P} \neg t_p\}}\left(\bigvee_{p \in P} \neg s_p\right) \right) \beppe{Explain the formula?}  Giuseppe Castagna committed Jul 05, 2019 626 The proof that this type satisfies \eqref{worra} is given in the Appendix~\ref{app:worra}.  Giuseppe Castagna committed Jun 26, 2019 627 628 629   Giuseppe Castagna committed Jun 26, 2019 630 \subsubsection{Type environments for occurrence typing}\label{sec:typenv}  Giuseppe Castagna committed Jun 24, 2019 631   Giuseppe Castagna committed Jun 28, 2019 632 633 The last step for our presentation is to define the algorithm for the deduction of $\Gamma \evdash e t \Gamma'$, that is an algorithm that  Giuseppe Castagna committed Jun 29, 2019 634 takes as input $\Gamma$, $e$, and $t$, and returns an environment that  Giuseppe Castagna committed Jun 28, 2019 635 636 637 extends $\Gamma$ with hypotheses on the occurrences of $e$ that are the most general that can be deduced by assuming that $e\in t$ succeeds.  Mickael Laurent committed Jul 01, 2019 638 639 640 The notation $\tyof{e}{\Gamma}$ denotes the type that can be deduced for the occurence $e$ under the type environment $\Gamma$ in the algorithmic type system given in Section~\ref{sec:algorules}. That is, $\tyof{e}{\Gamma}=\ts$ if and only if $\Gamma\vdashA e:\ts$ is provable.  Giuseppe Castagna committed Jul 01, 2019 641 We start by defining the algorithm for each single occurrence, that is for the deduction of $\pvdash \Gamma e t \varpi:t'$. This is obtained by defining two mutually recursive functions $\constrf$ and $\env{}{}$:  Giuseppe Castagna committed Jun 28, 2019 642 643 644 645 646 647 648 649 650 651 652 653 \newlength{\sk} \setlength{\sk}{-1.3pt} \begin{eqnarray} \constr\epsilon{\Gamma,e,t} & = & t\$\sk]\label{uno} \constr{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\env {\Gamma,e,t}{(\varpi.1)}}{\neg \env {\Gamma,e,t} (\varpi)})\\[\sk]\label{due} \constr{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\env {\Gamma,e,t} (\varpi)}\\[\sk]\label{tre} \constr{\varpi.l}{\Gamma,e,t} & = & \bpl{\env {\Gamma,e,t} (\varpi)}\\[\sk]\label{quattro} \constr{\varpi.r}{\Gamma,e,t} & = & \bpr{\env {\Gamma,e,t} (\varpi)}\\[\sk]\label{cinque} \constr{\varpi.f}{\Gamma,e,t} & = & \pair{\env {\Gamma,e,t} (\varpi)}\Any\\[\sk]\label{sei} \constr{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\env {\Gamma,e,t} (\varpi)}\\[1.5mm]\label{sette} \env {\Gamma,e,t} (\varpi) & = & \constr \varpi {\Gamma,e,t} \land \tsrep {\tyof {\occ e \varpi} \Gamma}\label{otto} \end{eqnarray}  Giuseppe Castagna committed Jun 24, 2019 654   Giuseppe Castagna committed Jun 28, 2019 655   Giuseppe Castagna committed Jun 26, 2019 656 657   Giuseppe Castagna committed Jun 28, 2019 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 %% \[ %% \begin{array}{lcl} %% \typep+\epsilon{\Gamma,e,t} & = & t\\ %% \typep-\epsilon{\Gamma,e,t} & = & \neg t\\ %% \typep{p}{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\Gp p{\Gamma,e,t}{(\varpi.1)}}{\neg \Gp p {\Gamma,e,t} (\varpi)})\\ %% \typep{p}{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\Gp p {\Gamma,e,t} (\varpi)}\\ %% \typep{p}{\varpi.l}{\Gamma,e,t} & = & \bpl{\Gp p {\Gamma,e,t} (\varpi)}\\ %% \typep{p}{\varpi.r}{\Gamma,e,t} & = & \bpr{\Gp p {\Gamma,e,t} (\varpi)}\\ %% \typep{p}{\varpi.f}{\Gamma,e,t} & = & \pair{\Gp p {\Gamma,e,t} (\varpi)}\Any\\ %% \typep{p}{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\Gp p {\Gamma,e,t} (\varpi)}\\ \\ %% \Gp p {\Gamma,e,t} (\varpi) & = & \typep p \varpi {\Gamma,e,t} \land \tsrep {\tyof {\occ e \varpi} \Gamma}\\ %% %\underbrace{\land \tyof {\occ e \varpi} {\Gamma\setminus\{\occ e \varpi\}}}_{\text{if \occ e \varpi is not a variable}}}\\ %% \end{array} %%$ %% \begin{align*} %% &(\RefineStep p {e,t} (\Gamma))(e') = %% \left\{\begin{array}{ll} %% %\tyof {e'} \Gamma \tsand %% \bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}} %% \Gp p {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\ %% \Gamma(e') & \text{otherwise, if } e' \in \dom \Gamma\\ %% \text{undefined} & \text{otherwise} %% \end{array}\right.\\ %% &\Refine p {e,t} \Gamma=\fixpoint_\Gamma (\RefineStep p {e,t})\qquad \text{(for the order $\leq$ on environments, defined in the proofs section)} %% \end{align*}  Mickael Laurent committed Jul 01, 2019 687 688 All the functions above are defined if and only if the initial path $\varpi$ is valid for $e$ (i.e. $\occ e{\varpi}$ is defined) and $e$ is well-typed (so that all $\tyof {\occ e{\varpi}} \Gamma$ encountered are defined).  Giuseppe Castagna committed Jun 28, 2019 689   Giuseppe Castagna committed Jul 01, 2019 690 Each case of the definition of the $\constrf$ function corresponds to the  Giuseppe Castagna committed Jun 28, 2019 691 692 693 694 application of a logical rule (\emph{cf.} Footnote~\ref{fo:rules}) in the deduction system for $\vdashp$: case \eqref{uno} corresponds to the application of \Rule{PEps}; case \eqref{due} implements \Rule{Pappl} straightforwardly; the implementation of rule \Rule{PAppR} is subtler:  Giuseppe Castagna committed Jun 28, 2019 695 696 instead of finding the best $t_1$ to subtract (by intersection) from the static type of the argument, \eqref{tre} finds directly the best type for the argument by  Giuseppe Castagna committed Jun 29, 2019 697 applying the $\worra{}{}$ operator to the static types of the function  Giuseppe Castagna committed Jun 28, 2019 698 and the refined type of the application. The remaining (\ref{quattro}--\ref{sette})  Giuseppe Castagna committed Jun 28, 2019 699 700 701 702 cases are the straightforward implementations of the rules \Rule{PPairL}, \Rule{PPairR}, \Rule{PFst}, and \Rule{PSnd}, respectively.  Giuseppe Castagna committed Jun 29, 2019 703 The other recursive function, $\env{}{}$, implements the two structural  Giuseppe Castagna committed Jun 28, 2019 704 705 rules \Rule{PInter} and \Rule{PTypeof} by intersecting the type obtained for $\varpi$ by the logical rules, with the static type  Giuseppe Castagna committed Jul 01, 2019 706 deduced by the type system of the expression occurring at $\varpi$. The  Giuseppe Castagna committed Jun 28, 2019 707 remaining structural rule, \Rule{Psubs}, is accounted for by the use  Giuseppe Castagna committed Jun 29, 2019 708 of the operators $\worra{}{}$ and $\boldsymbol{\pi}_i$ in  Giuseppe Castagna committed Jul 01, 2019 709 the definition of $\constrf$.  Giuseppe Castagna committed Jun 28, 2019 710 711 712 713  \footnote{Note that the definition is well-founded. This can be seen by analyzing the rule \Rule{Case\Aa}: the definition of $\Refine {e,t} \Gamma$ and $\Refine {e,\neg t} \Gamma$ use $\tyof{\occ e{\varpi}}\Gamma$, and this is defined for all $\varpi$ since the first premisses of \Rule{Case\Aa} states that  Giuseppe Castagna committed Jul 01, 2019 714 $\Gamma\vdash e:\ts_0$ (and this is possible only if we were able to deduce under the hypothesis $\Gamma$ the type of every occurrence of $e$.)} It extends the corresponding notation we gave for values in Section~\ref{sec:type-schemes}.  Giuseppe Castagna committed Jun 26, 2019 715   Giuseppe Castagna committed Jun 29, 2019 716 717 718 719 720 721 722 723 724 725 726 727 It remains to explain how to compute the environment $\Gamma'$ produced from $\Gamma$ by the deduction system for $\Gamma \evdash e t \Gamma'$. Alas, this is the most delicate part of our algorithm. In a nutshell what we want to do is to define a function $\Refine{\_,\_}{\_}$ that takes a type environment $\Gamma$, an expression $e$ and a type $t$ and returns the best type environment $\Gamma'$ such that $\Gamma \evdash e t \Gamma'$ holds. By the best environment we mean the one in which the occurrences of $e$ are associated to the largest possible types (type environments are hypotheses so they are contravariant: the larger the type the better the hypothesis). Recall that in Section~\ref{sec:challenges} we said that we want our analysis to be able to capture all the information available from nested checks. If we gave up such a kind of precision  Giuseppe Castagna committed Jul 01, 2019 728 then the definition of $\Refinef$ would be pretty easy: it must map  Giuseppe Castagna committed Jun 29, 2019 729 730 731 732 733 734 735 736 737 738 739 740 741 742 each subexpression of $e$ to the intersection of the types deduced by $\vdashp$ (\emph{ie}, by $\env{}{}$) for each of its occurrences. That is, for each expression $e'$ occurring in $e$, $\Refine {e,t}\Gamma$ is a type environment that maps $e'$ into $\bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}} \env {\Gamma,e,t} (\varpi)$. As we explained in Section~\ref{sec:challenges} the intersection is needed to apply occurrence typing to expression such as $\tcase{(x,x)}{\pair{t_1}{t_2}}{e_1}{e_2}$ where some expressions---here $x$---occur multiple times. In order to capture most of the type information from nested queries the rule \Rule{Path} allows the deduction of the type of some occurrence $\varpi$ to use a type environment $\Gamma'$ that may contain information about some suboccurrences of $\varpi$. On the  Giuseppe Castagna committed Jul 01, 2019 743 744 algorithm this would correspond to apply the $\Refinef$ defined above to a result of $\Refinef$, and so on. Therefore, ideally our  Giuseppe Castagna committed Jun 29, 2019 745 algorithm should compute the type environment as a fixpoint of the  Giuseppe Castagna committed Jul 01, 2019 746 function $X\mapsto\Refine{e,t}{X}$. Unfortunately, an iteration of $\Refinef$ may  Giuseppe Castagna committed Jun 29, 2019 747 not converge. As an example consider the (dumb) expression $\tcase  Giuseppe Castagna committed Jul 01, 2019 748 749 {x_1x_2}{\Any}{e_1}{e_2}$: if $x_1:\Any\to\Any$, then every iteration of $\Refinef$ yields for $x_1$ a type strictly more precise than the type deduced in the  Giuseppe Castagna committed Jun 29, 2019 750 751 752 previous iteration. The solution we adopt here is to bound the number of iterations to some number $n_o$.  Giuseppe Castagna committed Jul 01, 2019 753 754 755 756 757 From a formal point of view, this means to give up the completeness of the algorithm: $\Refinef$ will be complete (\emph{ie}, it will find all solutions) for the deductions of $\Gamma \evdash e t \Gamma'$ of depth at most $n_o$. This is obtained by the following definition of $\Refinef$ $\begin{array}{rcl} \Refinef_{e,t} \eqdef (\RefineStep{e,t})^{n_o}\\ \text{where }\RefineStep {e,t}(\Gamma)(e') &=& \left\{\begin{array}{ll}  Giuseppe Castagna committed Jun 28, 2019 758 759 760  %\tyof {e'} \Gamma \tsand \bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}} \env {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\  Mickael Laurent committed Jul 01, 2019 761 762  \Gamma(e') & \text{otherwise, if } e'\in\dom\Gamma\\ \text{undefined} & \text{otherwise}  Giuseppe Castagna committed Jul 01, 2019 763 764 765  \end{array}\right. \end{array}$  Giuseppe Castagna committed Jul 01, 2019 766 767 Note in particular that $\Refine{e,t}\Gamma$ extends $\Gamma$ with hypotheses on the expressions occurring in $e$, since $\dom{\Refine{e,t}\Gamma} = \dom{\RefineStep {e,t}(\Gamma)} = \dom{\Gamma} \cup \{e' \alt \exists \varpi.\ \occ e \varpi \equiv e'\}$.  Giuseppe Castagna committed Jul 01, 2019 768 769 770 771 772 773  In other terms, we try to find a fixpoint of $\RefineStep{e,t}$ but we bound our search to $n_o$ iterations. Since $\RefineStep {e,t}$ is monotone\footnote{\beppe{explain here the order on $\Gamma$.}}, then every iteration yields a better solution. \beppe{Does it make sense?}  Giuseppe Castagna committed Jun 29, 2019 774 775 776 777 778  While this is unsatisfactory from a formal point of view, in practice the problem is a very mild one. Divergence may happen only when refining the type of a function in an application: not only such a refinement is meaningful only when the function is typed by a union  Giuseppe Castagna committed Jul 01, 2019 779 780 781 782 783 784 type (which is quite rare in practice)\footnote{The only impact of adding a negated arrow type to the type of a function is when we test whether the function has a given arrow type: in practice this never happens since programming languages test whether a value \emph{is} a function, rather than the type of a given function.}, but also we had to build the expression that causes the divergence in  Giuseppe Castagna committed Jul 01, 2019 785 quite an \emph{ad hoc} way which makes divergence even more unlikely: setting  Giuseppe Castagna committed Jul 01, 2019 786 an $n_o$ twice the depth of the syntax tree of the outermost type case  Giuseppe Castagna committed Jul 01, 2019 787 788 should be enough to capture all realistic cases \beppe{can we give an estimate based on benchmarking the prototype?}  Giuseppe Castagna committed Jun 29, 2019 789   Giuseppe Castagna committed Jun 26, 2019 790 791 792   Giuseppe Castagna committed Jul 04, 2019 793 \subsubsection{Algorithmic typing rules}\label{sec:algorules}  Giuseppe Castagna committed Jul 01, 2019 794 We now have all notions needed for our typing algorithm, which is defined by the following rules.  Giuseppe Castagna committed Jun 26, 2019 795 \begin{mathpar}  Giuseppe Castagna committed Jun 28, 2019 796  \Infer[Efq\Aa]  Giuseppe Castagna committed Jun 26, 2019 797 798 799  { } { \Gamma, (e:\Empty) \vdashA e': \Empty } { \begin{array}{c}\text{\tiny with priority over}\\[-1.8mm]\text{\tiny all the other rules}\end{array}}  Mickael Laurent committed Jul 01, 2019 800 801 802 803 804  \qquad \Infer[Var\Aa] { } { \Gamma \vdashA x: \Gamma(x) } { x\in\dom\Gamma}  Giuseppe Castagna committed Jun 26, 2019 805  \\  Giuseppe Castagna committed Jun 28, 2019 806  \Infer[Env\Aa]  Giuseppe Castagna committed Jun 26, 2019 807 808  { \Gamma\setminus\{e\} \vdashA e : \ts } { \Gamma \vdashA e: \Gamma(e) \tsand \ts }  Giuseppe Castagna committed Jul 01, 2019 809  { \begin{array}{c}e\in\dom\Gamma \text{ and }\\[-1mm] e \text{ not a variable}\end{array}}  Giuseppe Castagna committed Jun 26, 2019 810  \qquad  Giuseppe Castagna committed Jun 28, 2019 811  \Infer[Const\Aa]  Giuseppe Castagna committed Jun 26, 2019 812 813 814 815  { } {\Gamma\vdashA c:\basic{c}} {c\not\in\dom\Gamma} \\  Giuseppe Castagna committed Jun 28, 2019 816  \Infer[Abs\Aa]  Giuseppe Castagna committed Jun 26, 2019 817 818 819 820 821 822  {\Gamma,x:s_i\vdashA e:\ts_i'\\ \ts_i'\leq t_i} { \Gamma\vdashA\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle\tsfun {\arrow {s_i} {t_i}}_{i\in I} } {\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e\not\in\dom\Gamma} \\  Giuseppe Castagna committed Jun 28, 2019 823  \Infer[App\Aa]  Giuseppe Castagna committed Jun 26, 2019 824 825 826 827 828 829 830 831 832  { \Gamma \vdashA e_1: \ts_1\\ \Gamma \vdashA e_2: \ts_2\\ \ts_1 \leq \arrow \Empty \Any\\ \ts_2 \leq \dom {\ts_1} } { \Gamma \vdashA {e_1}{e_2}: \ts_1 \circ \ts_2 } { {e_1}{e_2}\not\in\dom\Gamma} \\  Giuseppe Castagna committed Jun 28, 2019 833  \Infer[Case\Aa]  Giuseppe Castagna committed Jun 26, 2019 834 835 836 837 838 839 840 841 842 843 844 845 846  {\Gamma\vdashA e:\ts_0\\ %\makebox{$\begin{array}{l} % \left\{ % \begin{array}{ll} %\Gamma, % \Refine + {e,t} \Gamma \vdashA e_1 : \ts_1 & \text{ if } \ts_0 \not\leq \neg t\\ % \ts_1 = \Empty & \text{ otherwise} % \end{array}\right.\\ % \left\{ % \begin{array}{ll} %\Gamma, % \Refine - {e,t} \Gamma \vdashA e_2 : \ts_2 & \text{ if } \ts_0 \not\leq t\\ % \ts_2 = \Empty & \text{ otherwise} % \end{array}\right. %\end{array}$}  Mickael Laurent committed Jun 27, 2019 847 848  \Refine {e,t} \Gamma \vdashA e_1 : \ts_1\\ \Refine {e,\neg t} \Gamma \vdashA e_2 : \ts_2}  Giuseppe Castagna committed Jun 27, 2019 849  {\Gamma\vdashA \tcase {e} t {e_1}{e_2}: \ts_1\tsor \ts_2}  Giuseppe Castagna committed Jun 26, 2019 850  %{\ite {e} t {e_1}{e_2}\not\in\dom\Gamma}  Giuseppe Castagna committed Jun 27, 2019 851  { \tcase {e} {t\!} {\!e_1\!}{\!e_2}\not\in\dom\Gamma}  Giuseppe Castagna committed Jun 26, 2019 852  \\  Giuseppe Castagna committed Jun 28, 2019 853  \Infer[Proj\Aa]  Giuseppe Castagna committed Jun 26, 2019 854 855 856 857  {\Gamma \vdashA e:\ts\and \ts\leq\pair\Any\Any} {\Gamma \vdashA \pi_i e:\bpi_{\mathbf{i}}(\ts)} {\pi_i e\not\in\dom\Gamma}  Giuseppe Castagna committed Jun 28, 2019 858  \Infer[Pair\Aa]  Giuseppe Castagna committed Jun 26, 2019 859 860 861 862  {\Gamma \vdashA e_1:\ts_1 \and \Gamma \vdashA e_2:\ts_2} {\Gamma \vdashA (e_1,e_2):{\ts_1}\tstimes{\ts_2}}%\pair{t_1}{t_2}} {(e_1,e_2)\not\in\dom\Gamma} \end{mathpar}  Giuseppe Castagna committed Jul 01, 2019 863 864 865 The side conditions of the rules ensure that the system is syntax directed, that is, that at most one rule applies when typing a term: priority is given to \Rule{Eqf\Aa} over all the other rules and to  Giuseppe Castagna committed Jul 01, 2019 866 \Rule{Env\Aa} over all remaining logical rules. Type schemes are  Giuseppe Castagna committed Jul 01, 2019 867 868 869 870 871 used to account the type multiplicity stemming from $\lambda$-abstractions as shown in particular by rule \Rule{Abs\Aa} (in what follows we use the word type'' also for type schemes). The subsumption rule is no longer in the system. It is replaced by: $(i)$ using a union type in \Rule{Case\Aa}, $(ii)$ checking in \Rule{Abs\Aa}  Giuseppe Castagna committed Jul 01, 2019 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 that the body of the function is typed by a subtype of the type declared in the annotation, and $(iii)$ using type operators and checking subtyping in the elimination rules \Rule{App\Aa,Proj\Aa}. In particular, for \Rule{App\Aa} notice that it checks that the type of the function is a functional type, that the type of the argument is a subtype of the domain of the function, and then returns the result type of the application of the two types. The intersection rule is replaced by the use of type schemes in \Rule{Abs\Aa} and by the rule \Rule{Env\Aa}. The latter intersects the type deduced for an expression $e$ by occurrence typing and stored in $\Gamma$ with the type deduced for $e$ by the logical rules: this is simply obtained by removing any hypothesis about $e$ from $\Gamma$, so that the deduction of the type $\ts$ for $e$ cannot but end by a logical rule. Of course this does not apply when the expression $e$ is a variable, since an hypothesis in $\Gamma$ is the only way to deduce the type of a variable, which is a why the algorithm reintroduces the classic rules for variables.  Giuseppe Castagna committed Jul 01, 2019 889 890 891  The system above satisfies the following properties:\beppe{State here soundness and partial completeness}  Giuseppe Castagna committed Jun 28, 2019 892