language2.tex 25.9 KB
 Giuseppe Castagna committed Jun 26, 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 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 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 $\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} \item (regularity) the term has a finite number of different sub-terms; \item (contractivity) every infinite branch of a type contains an infinite number of occurrences of the arrow type constructor. \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 t_i$, $\neg t \vartriangleright t$ is Noetherian. This gives an induction principle on $\types$ that we will use without any further explicit reference to the relation. 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 49 50 51 52 53 54 55 56 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 type $s$, if the computation terminates, then they return a result of 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 26, 2019 83 84 t_i for all i\in I. Every value is associated to a type: we described above the types of constants and abstractions 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 Jun 26, 2019 92 The dynamic semantics is defined as a classic left-to-right cbv reduction for a \lambda-calculus with pairs enriched with a specific rule 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 103 104 105 106 107 108 109 110 \[ \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 definition to Section~\ref{sec:type-schemes}. Context reductions are 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 25, 2019 114 115 116 While the syntax and reduction semantics are on the whole pretty 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 178 179 180 181 182 \begin{mathpar} \Infer[Env] { } { \Gamma \vdash e: \Gamma(e) } { e\in\dom\Gamma } \qquad \Infer[Intersect] { \Gamma \vdash e:t_1\\\Gamma \vdash e:t_2 } { \Gamma \vdash e: t_1 \wedge t_2 } { } \end{mathpar}  Giuseppe Castagna committed Jun 26, 2019 183 The \Rule{Env} rule is coupled with the classic intersection introduction rule  Giuseppe Castagna committed Jun 25, 2019 184 185 186 187 188 which allow us to deduce for a complex expression the intersection of 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 Jun 26, 2019 190 arrow types, as long as these negated types do not make their type 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 Jun 26, 2019 197 As explained in Section~\ref{sec:challenges}, we need to be able to  Giuseppe Castagna committed Jun 25, 2019 198 199 200 201 202 203 204 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 205 206 of deduction was already present in the system by~\citet{Frisch2008} though it that system this deduction was motivated by the semantics of types rather than  Giuseppe Castagna committed Jun 25, 2019 207 208 209 210 211 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 212 instance, consider this simple example of a function that applied to an  Giuseppe Castagna committed Jun 25, 2019 213 integer returns its successor and applied to anything else returns  Giuseppe Castagna committed Jun 26, 2019 214 \textsf{true}:  Giuseppe Castagna committed Jun 25, 2019 215 $ Giuseppe Castagna committed Jun 26, 2019 216 \lambda^{(\Int\to\Int)\wedge(\neg\Int\to\Bool)} x\,.\,\tcase{x}{\Int}{x+1}{\textsf{true}}  Giuseppe Castagna committed Jun 25, 2019 217 $  Giuseppe Castagna committed Jun 26, 2019 218 Clearly, the expression above is well typed, but the rule \Rule{Abs+} alone  Giuseppe Castagna committed Jun 25, 2019 219 is not enough to type it. In particular, according to \Rule{Abs+} we  Giuseppe Castagna committed Jun 25, 2019 220 have to prove that under the hypothesis that $x$ is of type $\Int$ the expression  Giuseppe Castagna committed Jun 26, 2019 221 $(\tcase{x}{\Int}{x+1}{\textsf{true}})$ is of type $\Int$, too. That is, that under the  Giuseppe Castagna committed Jun 25, 2019 222 hypothesis that x has type $\Int\wedge\Int$ (we apply occurrence  Giuseppe Castagna committed Jun 26, 2019 223 typing) the expression $x+1$ is of type \Int{} (which holds) and that under the  Giuseppe Castagna committed Jun 25, 2019 224 hypothesis that $x$ has type $\Int\setminus\Int$, that is $\Empty$  Giuseppe Castagna committed Jun 26, 2019 225 226 (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 26, 2019 227 second case of a type-case even if we know that there is no chance that, when $x$ is bound to an $\Int$,  Giuseppe Castagna committed Jun 26, 2019 228 229 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 230 avoid this problem (and type the term above) we add the rule  Giuseppe Castagna committed Jun 26, 2019 231 232 233 \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 234 235 236 237 238 239 \begin{mathpar} \Infer[Efq] { } { \Gamma, (e:\Empty) \vdash e': t } { } \end{mathpar}  Giuseppe Castagna committed Jun 26, 2019 240 241 242 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 243 need the rule \Rule{Efq}, which is more general, to ensure the  Giuseppe Castagna committed Jun 26, 2019 244 property of subject reduction.\beppe{Example?}  Giuseppe Castagna committed Jun 25, 2019 245   Giuseppe Castagna committed Jun 26, 2019 246 247 248 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 249 250 251 252 253  \begin{mathpar} \Infer[Case] {\Gamma\vdash e:t_0\\ %t_0\not\leq \neg t \Rightarrow  Giuseppe Castagna committed Jun 25, 2019 254  \Gamma \evdash + e t \Gamma_1 \\ \Gamma_1 \vdash e_1:t'\\  Giuseppe Castagna committed Jun 25, 2019 255  %t_0\not\leq t \Rightarrow  Giuseppe Castagna committed Jun 25, 2019 256  \Gamma \evdash - e t \Gamma_2 \\ \Gamma_2 \vdash e_2:t'}  Giuseppe Castagna committed Jun 25, 2019 257 258  {\Gamma\vdash \tcase {e} t {e_1}{e_2}: t'} { }  Giuseppe Castagna committed Jun 25, 2019 259 \end{mathpar}  Giuseppe Castagna committed Jun 26, 2019 260 The rule \Rule{Case} checks whether the expression $e$, whose type is being tested, is  Giuseppe Castagna committed Jun 25, 2019 261 262 well-typed and then performs the occurrence typing analysis that produces the environments $\Gamma_i$'s under whose hypothesis the expressions  Giuseppe Castagna committed Jun 26, 2019 263 $e_i$'s are typed. The production of these environments is represented by the judgment  Giuseppe Castagna committed Jun 25, 2019 264 265 $\Gamma \evdash p e t \Gamma_i$ (with $p$ either $+$ or $-$). The intuition is that when $\Gamma \evdash p e t \Gamma_i$ is provable  Giuseppe Castagna committed Jun 26, 2019 266 267 then $\Gamma_i$ is a version of $\Gamma$ extended with type hypotheses for all expressions occurring in $e$, type hypotheses that can be deduced  Giuseppe Castagna committed Jun 25, 2019 268 269 270 assuming that the test $e\in t$ succeeds (for $p=+$) or fails (for $p=-$).  Giuseppe Castagna committed Jun 26, 2019 271 272 All it remains to do is to show how to deduce judgments of the form $\Gamma \evdash p e t \Gamma'$. For that we first have to define how  Giuseppe Castagna committed Jun 26, 2019 273 274 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 275 276 277 278 279 280 281 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 282 283 284 285 286 287 288 289 290 291 292 $\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\\ \end{array}$ undefined otherwise  Giuseppe Castagna committed Jun 25, 2019 293   Giuseppe Castagna committed Jun 25, 2019 294 295 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 26, 2019 296 application, $l$ and $r$ for the $l$eft and $r$ight expressions forming a pair  Giuseppe Castagna committed Jun 26, 2019 297 and $f$ and $s$ for the argument of a $f$irst or of a $s$econd projection. The judgments $\Gamma \evdash p e t \Gamma'$ are then deduced by the following two rules:  Giuseppe Castagna committed Jun 25, 2019 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 \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] { } { \Gamma \evdash p e t \Gamma } { } \qquad \Infer[Path] { \pvdash {\Gamma'} p e t \varpi:t' \\ \Gamma \evdash p e t \Gamma' } { \Gamma \evdash p e t \Gamma',(\occ e \varpi:t') } { }  Giuseppe Castagna committed Jun 25, 2019 317 \end{mathpar}  Giuseppe Castagna committed Jun 26, 2019 318 319 320 321 322 323 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 25, 2019 324 \Rule{Path} uses a (last) auxiliary judgement $\pvdash {\Gamma} p e t  Giuseppe Castagna committed Jun 26, 2019 325 \varpi:t'$ to deduce the type $t'$ of the occurrence $\occ e \varpi$ when  Giuseppe Castagna committed Jun 26, 2019 326 327 328 329 330 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 25, 2019 331 judgements of the form $\pvdash {\Gamma} p e t \varpi:t'$ where  Giuseppe Castagna committed Jun 26, 2019 332 $\varpi$ is a path to an expression occurring in $e$. This is given by the following set  Giuseppe Castagna committed Jun 25, 2019 333 334 335 336 337 338 339 of rules. \begin{mathpar} \Infer[PSubs] { \pvdash \Gamma p e t \varpi:t_1 \\ t_1\leq t_2 } { \pvdash \Gamma p e t \varpi:t_2 } { }  Giuseppe Castagna committed Jun 26, 2019 340 341 342 343 344  \qquad \Infer[PIntersect] { \pvdash \Gamma p e t \varpi:t_1 \\ \pvdash \Gamma p e t \varpi:t_2 } { \pvdash \Gamma p e t \varpi:t_1\land t_2 } { }  Giuseppe Castagna committed Jun 25, 2019 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361  \\ \Infer[PTypeof] { \Gamma \vdash \occ e \varpi:t' } { \pvdash \Gamma p e t \varpi:t' } { } \qquad \Infer[PEps+] { } { \pvdash \Gamma + e t \epsilon:t } { } \qquad \Infer[PEps-] { } { \pvdash \Gamma - e t \epsilon:\neg t } { } \\ \Infer[PAppR]  Giuseppe Castagna committed Jun 26, 2019 362  { \pvdash \Gamma p e t \varpi.0:\arrow{t_1}{t_2} \\ \pvdash \Gamma p e t \varpi:t_2'}  Giuseppe Castagna committed Jun 25, 2019 363  { \pvdash \Gamma p e t \varpi.1:\neg t_1 }  Giuseppe Castagna committed Jun 26, 2019 364  { t_2\land t_2' \simeq \Empty }  Giuseppe Castagna committed Jun 25, 2019 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 390 391  \\ \Infer[PAppL] { \pvdash \Gamma p e t \varpi.1:t_1 \\ \pvdash \Gamma p e t \varpi:t_2 } { \pvdash \Gamma p e t \varpi.0:\neg (\arrow {t_1} {\neg t_2}) } { } \qquad \Infer[PPairL] { \pvdash \Gamma p e t \varpi:\pair{t_1}{t_2} } { \pvdash \Gamma p e t \varpi.l:t_1 } { } \\ \Infer[PPairR] { \pvdash \Gamma p e t \varpi:\pair{t_1}{t_2} } { \pvdash \Gamma p e t \varpi.r:t_2 } { } \qquad \Infer[PFst] { \pvdash \Gamma p e t \varpi:t' } { \pvdash \Gamma p e t \varpi.f:\pair {t'} \Any } { } \qquad \Infer[PSnd] { \pvdash \Gamma p e t \varpi:t' } { \pvdash \Gamma p e t \varpi.s:\pair \Any {t'} } { } \qquad \end{mathpar}  Giuseppe Castagna committed Jun 26, 2019 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 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 the deduction $\vdashp$. The rule \Rule{PIntersect} combined with \Rule{PTypeof} allows the system to deduce for an occurrence $\varpi$ the intersection of the static type of $\occ e \varpi$ (deduced by \Rule{PTypeof}) and the type deduced for $\varpi$ by the other $\vdashp$ rules. The rules \Rule{PEps\,$p$} are the starting points of the analysis: when checking whether $e$ has type $t$ we can assume that $e$ (\emph{ie}, $\occ e\epsilon$) has type $t$ in the positive branch (rule \Rule{PEps+}) and type $\neg t$ in the negative branch (rule \Rule{PEps-}). The rule \Rule{PApprR} implements occurrence typing for 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\_} are straightforward since they state that $i$-th projection of a pair of type $\pair{t_1}{t_2}$ must be of type $t_i$. So are the last two 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 of progress and subject reduction, whose proof is given in the appendix. \begin{theorem}[soundness] For every expression $e$ such that $\varnothing\vdash e:t$ either there exists a value $v$ of type $t$ such that $e\reduces^* v$ or $e$ diverges. \end{theorem}  Giuseppe Castagna committed Jun 25, 2019 427 428 429 430 431   Giuseppe Castagna committed Jun 24, 2019 432 433 434  \subsection{Algorithmic system}  Giuseppe Castagna committed Jun 26, 2019 435 436 437 438 439 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 26, 2019 440 441 442 443 444 445 446 447 448 449 450 451 is probable. For that we need to solve essentially three problems: $(i)$ how to handle the fact that it is possible to deduce several types for the same well-typed expression $(ii)$ how to compute the 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 extend the technique of \emph{type schemes} defined  Giuseppe Castagna committed Jun 26, 2019 452 by~\citet{Frisch2004}. Type schemes are canonical representations of  Giuseppe Castagna committed Jun 26, 2019 453 the infinite set of types of $\lambda$-abstractions and they are  Giuseppe Castagna committed Jun 26, 2019 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 presented in Section~\ref{sec:type-schemes}. The second origin is due to the presence of structural rules\footnote{In logic, logical rules 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 contraction) do not.} such as \Rule{Subs} and \Rule{Intersect}. We handle it in the classic way: we define an algorithmic system that tracks the miminum type (actually, minimum type scheme) of an expression which is obtained from the original system by eliminating the two structural rules and distrubuting checks of the subtyping relation in the remaining rules. To do that in the presence of set-theoretic types we need to define some operators on types, given in section~\ref{sec:typeops}. For what concerns the use of the auxiliary derivation for the  judgments, we present in Section~\ref{sec:typenv} an algorithm that we prove sound \beppe{and complete?}. All these notions are used in the algorithmic typing system given in Section~\ref{sec:algorules}.  Giuseppe Castagna committed Jun 24, 2019 472   Giuseppe Castagna committed Jun 26, 2019 473 474 475 476 477 \beppe{\begin{enumerate} \item type of functions -> type schemes \item elimination rules (app, proj,if) ->operations on types and how to compute them \item not syntax directed: rules Subs, Intersect, Env. \item Compute the environments for occurrence typing. Algorithm to compute $\Gamma\vdash\Gamma$  Giuseppe Castagna committed Jun 24, 2019 478 \end{enumerate}  Giuseppe Castagna committed Jun 26, 2019 479 }  Giuseppe Castagna committed Jun 24, 2019 480 481   Giuseppe Castagna committed Jun 25, 2019 482 \subsubsection{Type schemes}\label{sec:type-schemes}  Giuseppe Castagna committed Jun 26, 2019 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 We introduce the new syntactic category of \emph{types schemes} which are the terms $\ts$ produced by the following grammar. $\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}$ type schemes denote sets of type, as formally stated by the following definition: \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 (straightforward induction) and that $\tsempty$, which denotes the empty set of types is different from $\empty$ whose interpretation is the set of all types. \begin{lemma} 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$. \beppe{Do we need the next definition and lemma here or they can go in the appendix? \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$. \begin{lemma} 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 24, 2019 548 549 550   Giuseppe Castagna committed Jun 26, 2019 551 \subsubsection{Operators on types}\label{sec:typeops}  Giuseppe Castagna committed Jun 24, 2019 552 553 554 555 556 557  \paragraph{Declarative version} \paragraph{Algorithmic version}  Giuseppe Castagna committed Jun 26, 2019 558 \subsubsection{Type environments for occurrence typing}\label{sec:typenv}  Giuseppe Castagna committed Jun 24, 2019 559 560 561   Giuseppe Castagna committed Jun 26, 2019 562 \subsection{Algorithmic typing rules}\label{sec:algorules}  Giuseppe Castagna committed Jun 24, 2019 563