language.tex 22 KB
 Giuseppe Castagna committed Jul 09, 2019 1 \newlength{\sk}  Giuseppe Castagna committed Jul 10, 2019 2 \setlength{\sk}{-1.9pt}  Giuseppe Castagna committed Mar 01, 2020 3 \iflongversion  Giuseppe Castagna committed Jul 05, 2019 4 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 Mar 01, 2020 5 \fi  Giuseppe Castagna committed Jun 24, 2019 6 7 8  \subsection{Types}  Giuseppe Castagna committed Jul 10, 2019 9 \begin{definition}[Types]\label{def:types} The set of types \types{} is formed by the terms $t$ coinductively produced by the grammar:\vspace{-1.45mm}  Giuseppe Castagna committed Jun 25, 2019 10 11 12 13 14 $\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}$  Giuseppe Castagna committed Feb 27, 2020 15 16 and that satisfy the following conditions \begin{itemize}[nosep]  Giuseppe Castagna committed Jul 01, 2019 17 18 \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  Giuseppe Castagna committed Jul 08, 2019 19 arrow or product type constructors.\vspace{-1mm}  Giuseppe Castagna committed Jun 25, 2019 20 21 \end{itemize} \end{definition}  Giuseppe Castagna committed Jul 08, 2019 22 We use the following abbreviations: $ Giuseppe Castagna committed Jun 25, 2019 23 24  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$.  Giuseppe Castagna committed Jul 08, 2019 25 $b$ ranges over basic types  Giuseppe Castagna committed Jul 05, 2019 26 (e.g., \Int, \Bool),  Giuseppe Castagna committed Jun 25, 2019 27 28 29 30 31 32 33 34 35 36 $\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 37 t_i$, $\neg t \vartriangleright t$ is Noetherian.  Giuseppe Castagna committed Jun 25, 2019 38 This gives an induction principle on $\types$ that we  Giuseppe Castagna committed Jul 01, 2019 39 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 40 41 42 43 44 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 Jul 03, 2020 45 46 by~\citet{Frisch2008} to which the reader may refer for the formal definition (see~\cite{types18post} for a simpler alternative definition). A detailed description of the algorithm to decide it can be found in~\cite{Cas15}.  Giuseppe Castagna committed Jun 25, 2019 47 For this presentation it suffices to consider that  Giuseppe Castagna committed Jul 05, 2019 48 types are interpreted as sets of \emph{values} ({i.e., either  Victor Lanvin committed Jul 10, 2019 49 constants, $\lambda$-abstractions, or pairs of values: see  Giuseppe Castagna committed Jun 25, 2019 50 Section~\ref{sec:syntax} right below) that have that type, and that subtyping is set  Giuseppe Castagna committed Jul 05, 2019 51 containment (i.e., a type $s$ is a subtype of a type $t$ if and only if $t$  Giuseppe Castagna committed Jun 25, 2019 52 53 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 54 type $s$, if their computation terminates, then they return a result of  Giuseppe Castagna committed Jul 05, 2019 55 type $t$ (e.g., $\Empty\to\Any$ is the set of all  Giuseppe Castagna committed Jun 25, 2019 56 57 58 59 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  Giuseppe Castagna committed Jul 05, 2019 60 61 (i.e., union, intersection, negation) are interpreted as the corresponding set-theoretic operators (e.g.,~$s\vee t$ is the  Giuseppe Castagna committed Jun 26, 2019 62 union of the values of the two types). We use $\simeq$ to denote the  Giuseppe Castagna committed Jul 10, 2019 63 symmetric closure of $\leq$: thus $s\simeq t$ (read, $s$ is equivalent to $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 64 65  \subsection{Syntax}\label{sec:syntax}  Giuseppe Castagna committed Jul 10, 2019 66 The expressions $e$ and values $v$ of our language are inductively generated by the following grammars:\vspace{-1mm}  Giuseppe Castagna committed Jun 25, 2019 67 \label{expressions}  Giuseppe Castagna committed Jun 25, 2019 68 \begin{array}{lrclr}  Giuseppe Castagna committed Jul 10, 2019 69 70  \textbf{Expr} &e &::=& c\alt x\alt ee\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt \pi_j e\alt(e,e)\alt\tcase{e}{t}{e}{e}\$.3mm] \textbf{Values} &v &::=& c\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt (v,v)\\[-1mm]  Giuseppe Castagna committed Jun 25, 2019 71 72 \end{array}  Giuseppe Castagna committed Jul 07, 2019 73 for j=1,2. In~\eqref{expressions}, c ranges over constants  Giuseppe Castagna committed Jul 05, 2019 74 (e.g., \texttt{true}, \texttt{false}, \texttt{1}, \texttt{2},  Giuseppe Castagna committed Jun 25, 2019 75 76 ...) 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)  Kim Nguyễn committed Feb 28, 2020 77 denotes pairs and \pi_i e their projections; \tcase{e}{t}{e_1}{e_2}  Giuseppe Castagna committed Jun 25, 2019 78 79 80 81 82 83 84 85 86 87 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 Feb 26, 2020 88 t_i for all i\in I. Every value is associated to a most specific type (mst): the mst of c is \basic c; the mst of  Giuseppe Castagna committed Jun 28, 2019 89  \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 Feb 27, 2020 90 91 the mst of a pair of values is the product of the mst's of the values. We write v\in t if the most specific type of v is a subtype of t (see Appendix~\ref{app:typeschemes} for the formal definition of v\in t which deals with some corner cases for negated arrow types).  Giuseppe Castagna committed Jun 24, 2019 92 93 94   Giuseppe Castagna committed Jun 26, 2019 95 \subsection{Dynamic semantics}\label{sec:opsem}  Giuseppe Castagna committed Jun 24, 2019 96   Giuseppe Castagna committed Jul 10, 2019 97 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:\vspace{-1.2mm}  Giuseppe Castagna committed Jun 25, 2019 98 99 \[ \begin{array}{rcll}  Kim Nguyễn committed Feb 27, 2020 100  (\lambda^{\wedge_{i\in I}s_i\to t_i} x.e)\,v &\reduces& e\subst x v\\[-.4mm]  Giuseppe Castagna committed Jul 10, 2019 101 102  \pi_i(v_1,v_2) &\reduces& v_i & i=1,2\\[-.4mm] \tcase{v}{t}{e_1}{e_2} &\reduces& e_1 &v\in t\\[-.4mm]  Giuseppe Castagna committed Jul 10, 2019 103  \tcase{v}{t}{e_1}{e_2} &\reduces& e_2 &v\not\in t\\[-1.3mm]  Giuseppe Castagna committed Jun 25, 2019 104 105 \end{array}$  Giuseppe Castagna committed Feb 26, 2020 106 Contextual reductions are  Giuseppe Castagna committed Jul 10, 2019 107 108 109 defined by the following evaluation contexts:\$1mm] \centerline{$$%\[  Giuseppe Castagna committed Jun 25, 2019 110 \Cx[] ::= [\,]\alt \Cx e\alt v\Cx \alt (\Cx,e)\alt (v,\Cx)\alt \pi_i\Cx\alt \tcase{\Cx}tee  Giuseppe Castagna committed Jul 10, 2019 111 112 %$$$}\$1mm]  Giuseppe Castagna committed Jun 25, 2019 113 114 115 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 116   Giuseppe Castagna committed Jul 08, 2019 117 \subsection{Static semantics}\label{sec:static}  Giuseppe Castagna committed Jun 24, 2019 118   Giuseppe Castagna committed Jun 28, 2019 119 While the syntax and reduction semantics are, on the whole, pretty  Giuseppe Castagna committed Sep 18, 2019 120 standard, for what concerns the type system we will have to introduce several  Giuseppe Castagna committed Jun 25, 2019 121 unconventional features that we anticipated in  Giuseppe Castagna committed Jun 26, 2019 122 Section~\ref{sec:challenges} and are at the core of our work. Let  Giuseppe Castagna committed Jun 25, 2019 123 us start with the standard part, that is the typing of the functional  Giuseppe Castagna committed Jul 10, 2019 124 core and the use of subtyping, given by the following typing rules:\vspace{-1mm}  Giuseppe Castagna committed Jun 25, 2019 125 126 127 128 129 130 131 132 \begin{mathpar} \Infer[Const] { } {\Gamma\vdash c:\basic{c}} { } \quad \Infer[App] {  Giuseppe Castagna committed Jun 25, 2019 133  \Gamma \vdash e_1: \arrow {t_1}{t_2}\quad  Giuseppe Castagna committed Jun 25, 2019 134 135 136 137 138 139  \Gamma \vdash e_2: t_1 } { \Gamma \vdash {e_1}{e_2}: t_2 } { } \quad \Infer[Abs+]  Giuseppe Castagna committed Jun 25, 2019 140  {{\scriptstyle\forall i\in I}\quad\Gamma,x:s_i\vdash e:t_i}  Giuseppe Castagna committed Jun 25, 2019 141 142 143 144 145 146 147 148 149 150 151 152  { \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'} % { }  Giuseppe Castagna committed Mar 01, 2020 153 \end{mathpar}  Giuseppe Castagna committed Mar 01, 2020 154 \begin{mathpar}  Giuseppe Castagna committed Jul 06, 2019 155  \Infer[Sel]  Giuseppe Castagna committed Jun 25, 2019 156 157 158 159 160 161 162 163 164 165 166 167 168  {\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' } { }  Giuseppe Castagna committed Jul 10, 2019 169  \qquad\vspace{-3mm}  Giuseppe Castagna committed Jun 25, 2019 170 \end{mathpar}  Giuseppe Castagna committed Feb 27, 2020 171 These rules are quite standard and do not need any particular explanation besides those already given in Section~\ref{sec:syntax}. Just notice subtyping is embedded in the system by the classic \Rule{Subs} subsumption rule. Next we focus on the unconventional aspects of our system, from the simplest to the hardest.  Giuseppe Castagna committed Jun 25, 2019 172   Giuseppe Castagna committed Jul 08, 2019 173 The first unconventional aspect is that, as explained in  Giuseppe Castagna committed Jun 26, 2019 174 Section~\ref{sec:challenges}, our type assumptions are about  Giuseppe Castagna committed Jul 05, 2019 175 expressions. Therefore, in our rules the type environments, ranged over  Giuseppe Castagna committed Jun 26, 2019 176 by \Gamma, map \emph{expressions}---rather than just variables---into  Giuseppe Castagna committed Jul 10, 2019 177 types. This explains why the classic typing rule for variables is replaced by a more general \Rule{Env} rule defined below:\vspace{-1mm}  Giuseppe Castagna committed Jun 25, 2019 178 179 180 181 182 183 \begin{mathpar} \Infer[Env] { } { \Gamma \vdash e: \Gamma(e) } { e\in\dom\Gamma } \qquad  Giuseppe Castagna committed Jun 28, 2019 184  \Infer[Inter]  Giuseppe Castagna committed Jun 25, 2019 185 186  { \Gamma \vdash e:t_1\\\Gamma \vdash e:t_2 } { \Gamma \vdash e: t_1 \wedge t_2 }  Giuseppe Castagna committed Jul 10, 2019 187  { }\vspace{-3mm}  Giuseppe Castagna committed Jun 25, 2019 188 \end{mathpar}  Giuseppe Castagna committed Jun 28, 2019 189 The \Rule{Env} rule is coupled with the standard intersection introduction rule \Rule{Inter}  Giuseppe Castagna committed Jul 01, 2019 190 which allows us to deduce for a complex expression the intersection of  Giuseppe Castagna committed Jun 25, 2019 191 192 193 194 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 195 system, that is, the fact that \lambda-abstractions can have negated  Giuseppe Castagna committed Jul 10, 2019 196 arrow types, as long as these negated types do not make the type deduced for the function empty:\vspace{-.5mm}  Giuseppe Castagna committed Jun 25, 2019 197 198 \begin{mathpar} \Infer[Abs-]  Mickael Laurent committed Jul 10, 2019 199 200  {\Gamma \vdash \lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:t} { \Gamma \vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\neg(t_1\to t_2) }  Giuseppe Castagna committed Mar 02, 2020 201  { ((\wedge_{i\in I}\arrow {s_i} {t_i})\wedge\neg(t_1\to t_2))\not\simeq\Empty }\vspace{-1.2mm}  Giuseppe Castagna committed Jun 25, 2019 202 \end{mathpar}  Giuseppe Castagna committed Jul 04, 2019 203 204 205 206 207 208 209 %\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 210 As explained in Section~\ref{sec:challenges}, we need to be able to  Giuseppe Castagna committed Jun 25, 2019 211 212 213 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  Giuseppe Castagna committed Jul 05, 2019 214 215 type (\Int\to t)\wedge\neg(\Int\to\neg\Bool), that is, (\Int\to t)\setminus(\Int\to\neg\Bool) ). But the sole rule \Rule{Abs+}  Giuseppe Castagna committed Jun 25, 2019 216 217 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 218 of deduction was already present in the system by~\citet{Frisch2008}  Kim Nguyễn committed Jul 11, 2019 219 though in that system this presence was motivated by the semantics of types rather than, as in our case,  Giuseppe Castagna committed Jun 25, 2019 220 221 222 223 224 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 225 instance, consider this simple example of a function that applied to an  Giuseppe Castagna committed Jun 25, 2019 226 integer returns its successor and applied to anything else returns  Giuseppe Castagna committed Jul 10, 2019 227 228 229 \textsf{true}:\\[1mm] \centerline{$$%\[  Giuseppe Castagna committed Jun 26, 2019 230 \lambda^{(\Int\to\Int)\wedge(\neg\Int\to\Bool)} x\,.\,\tcase{x}{\Int}{x+1}{\textsf{true}}  Giuseppe Castagna committed Jul 10, 2019 231 %$  Giuseppe Castagna committed Mar 02, 2020 232 $$}\$.6mm]  Giuseppe Castagna committed Jun 26, 2019 233 Clearly, the expression above is well typed, but the rule \Rule{Abs+} alone  Giuseppe Castagna committed Jun 25, 2019 234 is not enough to type it. In particular, according to \Rule{Abs+} we  Giuseppe Castagna committed Jun 25, 2019 235 have to prove that under the hypothesis that x is of type \Int the expression  Giuseppe Castagna committed Jun 26, 2019 236 (\tcase{x}{\Int}{x+1}{\textsf{true}}) is of type \Int, too. That is, that under the  Giuseppe Castagna committed Jul 08, 2019 237 hypothesis that x has type \Int\wedge\Int (we apply occurrence  Giuseppe Castagna committed Jun 26, 2019 238 typing) the expression x+1 is of type \Int{} (which holds) and that under the  Giuseppe Castagna committed Jun 25, 2019 239 hypothesis that x has type \Int\setminus\Int, that is \Empty  Giuseppe Castagna committed Jun 26, 2019 240 241 (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 242 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 243 244 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 245 avoid this problem (and type the term above) we add the rule  Giuseppe Castagna committed Jun 26, 2019 246 247 248 \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 249 250 251 252 \begin{mathpar} \Infer[Efq] { } { \Gamma, (e:\Empty) \vdash e': t }  Giuseppe Castagna committed Jul 10, 2019 253  { }\vspace{-3mm}  Giuseppe Castagna committed Jun 25, 2019 254 \end{mathpar}  Giuseppe Castagna committed Jun 26, 2019 255 256 Once more, this kind of deduction was already present in the system by~\citet{Frisch2008} to type full fledged overloaded functions,  Giuseppe Castagna committed Mar 04, 2020 257 258 259 260 261 262 though it was embedded in the typing rule for the type-case.% \ifsubmission% ~\pagebreak \else \fi%  Giuseppe Castagna committed Mar 01, 2020 263 Here we  Giuseppe Castagna committed Jun 26, 2019 264 need the rule \Rule{Efq}, which is more general, to ensure the  Giuseppe Castagna committed Jul 08, 2019 265 266 property of subject reduction. %\beppe{Example?}  Giuseppe Castagna committed Jun 25, 2019 267   Giuseppe Castagna committed Jul 10, 2019 268 Finally, there remains one last rule in our type system, the one that  Giuseppe Castagna committed Jun 26, 2019 269 implements occurrence typing, that is, the rule for the  Giuseppe Castagna committed Jul 10, 2019 270 type-case:\vspace{-1mm}  Giuseppe Castagna committed Jun 25, 2019 271 272 273 274 \begin{mathpar} \Infer[Case] {\Gamma\vdash e:t_0\\ %t_0\not\leq \neg t \Rightarrow  Mickael Laurent committed Jun 27, 2019 275  \Gamma \evdash e t \Gamma_1 \\ \Gamma_1 \vdash e_1:t'\\  Giuseppe Castagna committed Jun 25, 2019 276  %t_0\not\leq t \Rightarrow  Mickael Laurent committed Jun 27, 2019 277  \Gamma \evdash e {\neg t} \Gamma_2 \\ \Gamma_2 \vdash e_2:t'}  Giuseppe Castagna committed Jun 25, 2019 278  {\Gamma\vdash \tcase {e} t {e_1}{e_2}: t'}  Giuseppe Castagna committed Jul 10, 2019 279  { }\vspace{-3mm}  Giuseppe Castagna committed Jun 25, 2019 280 \end{mathpar}  Giuseppe Castagna committed Jun 28, 2019 281 282 283 284 285 286 287 288 289 290 291 292 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 293   Giuseppe Castagna committed Jun 26, 2019 294 All it remains to do is to show how to deduce judgments of the form  Giuseppe Castagna committed Jul 08, 2019 295 \Gamma \evdash e t \Gamma'. For that we first define how  Giuseppe Castagna committed Jun 26, 2019 296 297 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 298 299 300 301 302 303 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  Kim Nguyễn committed Feb 27, 2020 304 the path \varpi, that is (for i=0,1, and undefined otherwise)\vspace{-.4mm}  Giuseppe Castagna committed Jul 06, 2019 305 306 307 308 309 310 311 312 313 314 315 316 317 %% \[ %% \begin{array}{l} %% \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}\\ %% \text{undefined otherwise} %% \end{array} %%$  Giuseppe Castagna committed Jun 25, 2019 318 $ Giuseppe Castagna committed Jul 06, 2019 319 \begin{array}{r@{\downarrow}l@{\quad=\quad}lr@{\downarrow}l@{\quad=\quad}lr@{\downarrow}l@{\quad=\quad}l}  Kim Nguyễn committed Feb 27, 2020 320 321 e&\epsilon & e & (e_1,e_2)& l.\varpi & \occ{e_1}\varpi &\pi_1 e& f.\varpi & \occ{e}\varpi\\ e_0\,e_1& i.\varpi & \occ{e_i}\varpi \quad\qquad& (e_1,e_2)& r.\varpi & \occ{e_2}\varpi \quad\qquad&  Giuseppe Castagna committed Jul 10, 2019 322 \pi_2 e& s.\varpi & \occ{e}\varpi\\[-.4mm]  Giuseppe Castagna committed Jun 25, 2019 323 324 325 326 \end{array}$ 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 327 application, $l$ and $r$ for the $l$eft and $r$ight expressions forming a pair,  Giuseppe Castagna committed Jul 01, 2019 328 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  Giuseppe Castagna committed Jul 08, 2019 329 under $\lambda$'s (since their type is frozen in their annotations) and type-cases (since they reset the analysis).  Giuseppe Castagna committed Jul 10, 2019 330 331 % The judgments $\Gamma \evdash e t \Gamma'$ are then deduced by the following two rules:\vspace{-1mm} \begin{mathpar}  Giuseppe Castagna committed Jun 25, 2019 332 333 334 335 336 337 338 339 340 341 342 % \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 343  { \Gamma \evdash e t \Gamma }  Giuseppe Castagna committed Jun 25, 2019 344 345 346  { } \qquad \Infer[Path]  Mickael Laurent committed Jun 27, 2019 347 348  { \pvdash {\Gamma'} e t \varpi:t' \\ \Gamma \evdash e t \Gamma' } { \Gamma \evdash e t \Gamma',(\occ e \varpi:t') }  Giuseppe Castagna committed Jul 10, 2019 349  { }\vspace{-1.5mm}  Giuseppe Castagna committed Jun 25, 2019 350 \end{mathpar}  Giuseppe Castagna committed Jun 26, 2019 351 352 353 354 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  Giuseppe Castagna committed Jul 08, 2019 355 occurrence $\varpi$ of the expression $e$ being checked, then we can add this  Giuseppe Castagna committed Jun 26, 2019 356 hypothesis to the produced type environment (rule \Rule{Path}). The rule  Giuseppe Castagna committed Jun 28, 2019 357 \Rule{Path} uses a (last) auxiliary judgement $\pvdash {\Gamma} e t  Giuseppe Castagna committed Jun 26, 2019 358 \varpi:t'$ to deduce the type $t'$ of the occurrence $\occ e \varpi$ when  Giuseppe Castagna committed Jun 26, 2019 359 360 361 362 363 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 364 judgements of the form $\pvdash {\Gamma} e t \varpi:t'$ where  Giuseppe Castagna committed Jun 26, 2019 365 $\varpi$ is a path to an expression occurring in $e$. This is given by the following set  Giuseppe Castagna committed Jun 25, 2019 366 367 368 of rules. \begin{mathpar} \Infer[PSubs]  Mickael Laurent committed Jun 27, 2019 369 370  { \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 371  { }  Giuseppe Castagna committed Jul 10, 2019 372  \quad  Giuseppe Castagna committed Jun 28, 2019 373  \Infer[PInter]  Mickael Laurent committed Jun 27, 2019 374 375  { \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 376  { }  Giuseppe Castagna committed Jul 10, 2019 377  \quad  Giuseppe Castagna committed Jun 25, 2019 378 379  \Infer[PTypeof] { \Gamma \vdash \occ e \varpi:t' }  Mickael Laurent committed Jun 27, 2019 380  { \pvdash \Gamma e t \varpi:t' }  Giuseppe Castagna committed Jun 25, 2019 381  { }  Giuseppe Castagna committed Jul 10, 2019 382 \vspace{-1.2mm}\\  Mickael Laurent committed Jun 27, 2019 383  \Infer[PEps]  Giuseppe Castagna committed Jun 25, 2019 384  { }  Mickael Laurent committed Jun 27, 2019 385  { \pvdash \Gamma e t \epsilon:t }  Giuseppe Castagna committed Jun 25, 2019 386 387 388  { } \qquad \Infer[PAppR]  Mickael Laurent committed Jun 27, 2019 389 390  { \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 391  { t_2\land t_2' \simeq \Empty }  Giuseppe Castagna committed Mar 02, 2020 392 \end{mathpar}\begin{mathpar}\vspace{-2mm}  Giuseppe Castagna committed Jun 25, 2019 393  \Infer[PAppL]  Mickael Laurent committed Jun 27, 2019 394 395  { \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 396 397 398  { } \qquad \Infer[PPairL]  Mickael Laurent committed Jun 27, 2019 399 400  { \pvdash \Gamma e t \varpi:\pair{t_1}{t_2} } { \pvdash \Gamma e t \varpi.l:t_1 }  Giuseppe Castagna committed Jun 25, 2019 401  { }  Giuseppe Castagna committed Jul 10, 2019 402 \vspace{-1.2mm}\\  Giuseppe Castagna committed Jun 25, 2019 403  \Infer[PPairR]  Mickael Laurent committed Jun 27, 2019 404 405  { \pvdash \Gamma e t \varpi:\pair{t_1}{t_2} } { \pvdash \Gamma e t \varpi.r:t_2 }  Giuseppe Castagna committed Jun 25, 2019 406 407 408  { } \qquad \Infer[PFst]  Mickael Laurent committed Jun 27, 2019 409 410  { \pvdash \Gamma e t \varpi:t' } { \pvdash \Gamma e t \varpi.f:\pair {t'} \Any }  Giuseppe Castagna committed Jun 25, 2019 411 412 413  { } \qquad \Infer[PSnd]  Mickael Laurent committed Jun 27, 2019 414 415  { \pvdash \Gamma e t \varpi:t' } { \pvdash \Gamma e t \varpi.s:\pair \Any {t'} }  Giuseppe Castagna committed Mar 02, 2020 416  { }\vspace{-0.9mm}  Giuseppe Castagna committed Jun 25, 2019 417 \end{mathpar}  Giuseppe Castagna committed Jun 26, 2019 418 419 420 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 421 the deduction $\vdashp$. The rule \Rule{PInter} combined with  Giuseppe Castagna committed Jun 26, 2019 422 423 \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 424 \Rule{PTypeof}) with the type deduced for $\varpi$ by the other $\vdashp$ rules. The  Giuseppe Castagna committed Jul 05, 2019 425 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$ (i.e.,  Giuseppe Castagna committed Jun 28, 2019 426 $\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).  Giuseppe Castagna committed Feb 27, 2020 427 The rule \Rule{PAppR} implements occurrence typing for  Giuseppe Castagna committed Jun 26, 2019 428 429 430 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$  Giuseppe Castagna committed Feb 27, 2020 431 (since $t_2\land t_2' \simeq \Empty$), then the argument of this application cannot be of type $t_1$. \Rule{PAppL} performs the  Giuseppe Castagna committed Jun 26, 2019 432 433 434 435 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 436 are straightforward since they state that the $i$-th projection of a pair  Giuseppe Castagna committed Jul 01, 2019 437 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 438 439 440 441 442 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  Giuseppe Castagna committed Jul 08, 2019 443 the property of safety, deduced, as customary, from the properties  Giuseppe Castagna committed Mar 02, 2020 444 of progress and subject reduction (\emph{cf.} Appendix~\ref{app:soundness}).\vspace{-.5mm}  Giuseppe Castagna committed Jul 08, 2019 445 \begin{theorem}[type safety]  Giuseppe Castagna committed Jun 26, 2019 446 447 448 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 449 \end{theorem}  Giuseppe Castagna committed Mar 02, 2020 450 \vspace{-2.1mm}  Giuseppe Castagna committed Jun 25, 2019 451 452 453 454