proofs-algo.tex 63.7 KB
 Giuseppe Castagna committed Mar 03, 2020 1 2 We give in this section a typing algorithm that uses types schemes and is more general than the one presented in the main body of the paper (that is, one whose completeness is not limited to  Giuseppe Castagna committed Mar 03, 2020 3 positive expressions). We start by defining how to compute the $\worra{}{}$'' operator and then we define type schemes and the algorithm. We prove that this algorithm (as well as the  Giuseppe Castagna committed Mar 03, 2020 4 5 6 one in the main body of the paper) is sound w.r.t.\ to the declarative type system and that, under certain restrictions it is also complete.  Giuseppe Castagna committed Mar 03, 2020 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 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142  \subsection{Operator $\worra {} {}$}\label{app:worra} In this section, we will use the algorithmic definition of $\worra {} {}$ and show that it is equivalent to its descriptive definition. \begin{eqnarray*} &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)\\ &\worra t s = \dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right) \end{eqnarray*} \begin{lemma}[Correctness of $\worra {} {}$] $\forall t, s.\ \apply t {(\dom t \setminus (\worra t s))} \leq \neg s$ \end{lemma} \begin{proof} Let $t$ an arrow type. $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)$\\ Let $s$ be any type. Let's prove that $\apply t {(\dom t \setminus (\worra t s))} \leq \neg s$ (with the algorithmic definition for $\worra {} {}$).\\ Equivalently, we want $(\apply t {(\dom t \setminus (\worra t s))}) \land s \simeq \Empty$.\\ Let $u$ be a type such that $u \leq \dom t$ and $(\apply t u) \land s \not\simeq \Empty$ (if such a type does not exist, we are done).\\ Let's show that $u \land (\worra t s) \not\simeq \Empty$ (we can easily deduce the wanted property from that, by the absurd).\\ For that, we should prove the following:\\ $\exists i \in I.\ u \land \bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right) \not\simeq \Empty$ From $(\apply t u) \land s \not\simeq \Empty$, we can take (using the algorithmic definition of $\circ$) $i \in I$ and $Q \subsetneq P_i$ such that:\\ $u \not\leq\bigvee_{q\in Q}s_q \text{\ \ \ and\ \ \ } (\bigwedge_{p\in P_i\setminus Q}t_p) \land s \not\simeq \Empty$ For any $P \subseteq P_i$ such that $s \leq \bigvee_{p \in P} \neg t_p$ (equivalently, $s \land \bigwedge_{p \in P} t_p \simeq \Empty$),\\ we have $P \cap Q \neq \varnothing$ (by the absurd, because $(\bigwedge_{p\in P_i\setminus Q}t_p) \land s \not\simeq \Empty$).\\ Consequently, we have: $\forall P \subseteq P_i.\ s \leq \bigvee_{p \in P} \neg t_p \Rightarrow \bigwedge_{p \in P} s_p \leq \bigvee_{q \in Q}s_q$ We can deduce that: $\bigvee_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigwedge_{p \in P} s_p\right) \leq \bigvee_{q \in Q}s_q$ Moreover, as $u \not\leq \bigvee_{q\in Q}s_q$, we have $u \not\leq \bigvee_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigwedge_{p \in P} s_p\right)$.\\ This is equivalent to the wanted result. \end{proof} \begin{lemma}[$\worra {} {}$ alternative definition] The following algorithmic definition for $\worra {} {}$ is equivalent to the previous one: $\forall t, s.\ \worra t s \simeq \bigvee_{i \in I} \left( \bigvee_{\{P \subseteq P_i\alt s \not\leq \bigvee_{p \in P} \neg t_p \} }\left( \dom t \land \bigwedge_{p\in P_i} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right)\right)$ \end{lemma} \begin{proof} \begingroup \allowdisplaybreaks \begin{align*} \worra t s & = \dom t \wedge\bigvee_{i\in I}\left( \bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\ & \simeq \bigvee_{i\in I} \left(\dom t \wedge \bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\ & \simeq \bigvee_{i\in I} \left(\left( \dom t \wedge \bigvee_{p \in P_i} s_p \right) \wedge \bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\ & \simeq \bigvee_{i\in I} \left(\left( \dom t \wedge \bigvee_{p \in P_i} \left(s_p \land \bigvee_{P \subseteq P_i \setminus \{p\}} \left(\bigwedge_{p \in P} s_p \land \bigwedge_{n \in (P_i \setminus \{p\}) \setminus P} \neg s_n \right) \right) \right) \wedge \bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\ & \simeq \bigvee_{i\in I} \left(\left( \dom t \wedge \bigvee_{p \in P_i} \left(\bigvee_{P \subseteq P_i \setminus \{p\}} \left( s_p \land \bigwedge_{p \in P} s_p \land \bigwedge_{n \in (P_i \setminus \{p\}) \setminus P} \neg s_n \right) \right) \right) \wedge \bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\ & \simeq \bigvee_{i\in I} \left(\left( \dom t \wedge \bigvee_{\substack{P \subseteq P_i\\P \neq \varnothing}} \left(\bigwedge_{p \in P} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right) \right) \wedge \bigwedge_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigvee_{p \in P} \neg s_p \right)\right)\\ & \simeq \bigvee_{i\in I} \left( \dom t \wedge \bigvee_{\substack{P \subseteq P_i\\P \neq \varnothing}} \left(\bigwedge_{p \in P} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right) \setminus \bigvee_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigwedge_{p \in P} s_p \right)\right)\\ & \simeq \bigvee_{i\in I} \left( \dom t \wedge \bigvee_{\substack{P \subseteq P_i\\P \neq \varnothing}} \left(\bigwedge_{p \in P} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right) \setminus \bigvee_{\{P \subseteq P_i\alt s \leq \bigvee_{p \in P} \neg t_p\}} \left(\bigwedge_{p \in P} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right)\right)\\ & \simeq \bigvee_{i \in I} \left( \dom t \land \bigvee_{\{P \subseteq P_i\alt s \not\leq \bigvee_{p \in P} \neg t_p \} }\left( \bigwedge_{p\in P_i} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right)\right)\\ & \simeq \bigvee_{i \in I} \left( \bigvee_{\{P \subseteq P_i\alt s \not\leq \bigvee_{p \in P} \neg t_p \} }\left( \dom t \land \bigwedge_{p\in P_i} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n \right)\right) \end{align*} \endgroup \end{proof} \begin{lemma}[Optimality of $\worra {} {}$] Let $t$, $s$, two types. For any $u$ such that $\apply t {(\dom t \setminus u)} \leq \neg s$, we have $\worra t s \leq u$. \end{lemma} \begin{proof} Let $t$ an arrow type. $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)$\\ Let $s$ be any type. Let $u$ be such that $\apply t {(\dom t \setminus u)} \leq \neg s$. We want to prove that $\worra t s \leq u$. We have: $\worra t s = \bigvee_{i \in I} \left(\bigvee_{\{P \subseteq P_i\alt s \not\leq \bigvee_{p \in P} \neg t_p \} } a_{i,P}\right)$ With: $a_{i,P}=\dom t \land \bigwedge_{p\in P_i} s_p \land \bigwedge_{n \in P_i \setminus P} \neg s_n$ Let $i \in I$ and $P \subseteq P_i$ such that $s \not\leq \bigvee_{p \in P} \neg t_p$ (equivalently, $s \land \bigwedge_{p \in P} t_p \not\simeq \Empty$) and such that $a_{i,P} \not\simeq \Empty$.\\ For convenience, let $a = a_{i,P}$. We just have to show that $a \leq u$. By the absurd, let's suppose that $a \setminus u \not\simeq \Empty$ and show that $(\apply t {(\dom t \setminus u)}) \land s \not\simeq \Empty$.\\ Let's recall the algorithmic definition of $\circ$: $\apply t {(\dom t \setminus u)} = \bigvee_{i\in I}\left(\bigvee_{\{Q\subsetneq P_i\alt \dom t \setminus u \not\leq\bigvee_{q\in Q}s_q\}}\left(\bigwedge_{p\in P_i\setminus Q}t_p\right)\right)$ Let's take $Q = P_i \setminus P$. We just have to prove that: $\dom t \setminus u \not\leq\bigvee_{q\in Q}s_q \text{\ \ \ and\ \ \ } s \land \bigwedge_{p\in P_i\setminus Q}t_p \not\simeq \Empty$ As $P_i \setminus Q = P$, we immediatly have $s \land \bigwedge_{p\in P_i\setminus Q}t_p \not\simeq \Empty$. Moreover, we know that $a \leq \bigwedge_{q \in Q} \neg s_q$ (definition of $a_{i,P}$), so we have: $a \land \bigwedge_{q\in Q} \neg s_q \simeq a$ Thus: $(a \setminus u) \land \bigwedge_{q\in Q} \neg s_q \simeq (a \land \bigwedge_{q\in Q} \neg s_q) \setminus u \simeq a \setminus u \not\simeq \Empty$ And so: $a \setminus u \not\leq \bigvee_{q\in Q}s_q$ As $\dom t \setminus u \geq a \setminus u$, we can immediatly obtain the remaining inequality. \end{proof} \begin{theorem}[Characterization of $\worra {} {}$] $\forall t, s.\ \worra t s = \min \{ u \alt \apply t {(\dom t \setminus u)} \leq \neg s \}$. \end{theorem} \begin{proof} Immediate consequence of the previous results. \end{proof}  Giuseppe Castagna committed Mar 03, 2020 143 \subsection{Type Schemes}  Giuseppe Castagna committed Mar 03, 2020 144 145 146 147 148 149 150 151  We introduce for the proofs the notion of \emph{type schemes} and we define a more powerful algorithmic type system that uses them. It allows us to have a stronger (but still partial) completeness theorem. The proofs for the algorithmic type system presented in \ref{sec:algorules} can be derived  Giuseppe Castagna committed Mar 03, 2020 152 from the proofs of this section (see Section \ref{sec:proofs_algorithmic_without_ts}).  Giuseppe Castagna committed Mar 03, 2020 153 154 155 156 157 158 159 160 161 162 163  \subsubsection{Type schemes}\label{app:typeschemes} We introduce the new syntactic category of \emph{type schemes} which are the terms~$\ts$ inductively 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 types, as formally stated by the following definition: \begin{definition}[Interpretation of type schemes]  Kim Nguyễn committed Feb 22, 2021 164  We define the function $\tsint {\_}$ that maps type schemes into sets of types.\svvspace{-2.5mm}  Giuseppe Castagna committed Mar 03, 2020 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206  \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 and that $\tsempty$, which denotes the empty set of types is different from $\Empty$ whose interpretation is the set of all types. \begin{lemma}[\cite{Frisch2008}] 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 scheme 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$. We also need to perform intersections of type schemes so as to intersect the static type of an expression (i.e., the one deduced by conventional rules) with the one deduced by occurrence typing (i.e., 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: \begin{lemma}[\cite{Frisch2008}] 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} Finally, given a type scheme $\ts$ it is straightforward to choose in its interpretation a type $\tsrep\ts$ which serves as the canonical representative of the set (i.e., $\tsrep \ts \in \tsint \ts$): \begin{definition}[Representative]  Kim Nguyễn committed Feb 22, 2021 207  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.\svvspace{-2mm}  Giuseppe Castagna committed Mar 03, 2020 208 209 210 211 212  \begin{align*} \begin{array}{lcllcl} \tsrep t &=& t & \tsrep {\ts_1 \tstimes \ts_2} &=& \pair {\tsrep {\ts_1}} {\tsrep {\ts_2}}\\ \tsrep {\tsfunone {t_i} {s_i}_{i\in I}} &=& \bigwedge_{i\in I} \arrow {t_i} {s_i} \qquad& \tsrep {\ts_1 \tsor \ts_2} &=& \tsrep {\ts_1} \vee \tsrep {\ts_2}\\ \tsrep \tsempty && \textit{undefined}  Kim Nguyễn committed Feb 22, 2021 213  \end{array}\svvspace{-4mm}  Giuseppe Castagna committed Mar 03, 2020 214 215 216 217 218 219 220  \end{align*} \end{definition} Type schemes are already present in the theory of semantic subtyping presented in~\cite[Section 6.11]{Frisch2008}. In particular, it explains how the operators such as $\circ$, $\bpl t$ and $\bpr t$ can be extended to type schemes (see also~\citep[\S4.4]{Cas15} for a detailed description).  Giuseppe Castagna committed Mar 03, 2020 221 \subsection{Algorithmic type system with type schemes}  Giuseppe Castagna committed Mar 03, 2020 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 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 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 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  We present here a refinement of the algorithmic type system presented in \ref{sec:algorules} that associates to an expression a type scheme instead of a regular type. This allows to type expressions more precisely and thus to have a more powerful (but still partial) completeness theorem in regards to the declarative type system. The results about this new type system will be used in \ref{sec:proofs_algorithmic_without_ts} in order to obtain a soundness and completeness theorem for the algorithmic type system presented in \ref{sec:algorules}. \begin{mathpar} \Infer[Efq\Aats] { } { \Gamma, (e:\Empty) \vdashAts e': \Empty } { \begin{array}{c}\text{\tiny with priority over}\-1.8mm]\text{\tiny all the other rules}\end{array}} \qquad \Infer[Var\Aats] { } { \Gamma \vdashAts x: \Gamma(x) } { x\in\dom\Gamma} \\ \Infer[Env\Aats] { \Gamma\setminus\{e\} \vdashAts e : \ts } { \Gamma \vdashAts e: \Gamma(e) \tsand \ts } { e\in\dom\Gamma \text{ and } e \text{ not a variable}} \qquad \Infer[Const\Aats] { } {\Gamma\vdashAts c:\basic{c}} {c\not\in\dom\Gamma} \\ \Infer[Abs\Aats] {\Gamma,x:s_i\vdashAts e:\ts_i'\\ \ts_i'\leq t_i} { \Gamma\vdashAts\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} \\ \Infer[App\Aats] { \Gamma \vdashAts e_1: \ts_1\\ \Gamma \vdashAts e_2: \ts_2\\ \ts_1 \leq \arrow \Empty \Any\\ \ts_2 \leq \dom {\ts_1} } { \Gamma \vdashAts {e_1}{e_2}: \ts_1 \circ \ts_2 } { {e_1}{e_2}\not\in\dom\Gamma} \\ \Infer[Case\Aats] {\Gamma\vdashAts e:\ts_0\\ \Refine {e,t} \Gamma \vdashAts e_1 : \ts_1\\ \Refine {e,\neg t} \Gamma \vdashAts e_2 : \ts_2} {\Gamma\vdashAts \tcase {e} t {e_1}{e_2}: \ts_1\tsor \ts_2} { \tcase {e} {t\!} {\!e_1\!}{\!e_2}\not\in\dom\Gamma} \\ \Infer[Proj\Aats] {\Gamma \vdashAts e:\ts\and \ts\leq\pair\Any\Any} {\Gamma \vdashAts \pi_i e:\bpi_{\mathbf{i}}(\ts)} {\pi_i e\not\in\dom\Gamma} \Infer[Pair\Aats] {\Gamma \vdashAts e_1:\ts_1 \and \Gamma \vdashAts e_2:\ts_2} {\Gamma \vdashAts (e_1,e_2):{\ts_1}\tstimes{\ts_2}} {(e_1,e_2)\not\in\dom\Gamma} \end{mathpar} \begin{align*} \tyof e \Gamma = \left\{\begin{array}{ll} \ts & \text{if } \Gamma \vdashAts e:\ts \\ \tsempty & \text{otherwise} \end{array}\right. \end{align*} \begin{eqnarray} \constr\epsilon{\Gamma,e,t} & = & t\\ \constr{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\env {\Gamma,e,t}{(\varpi.1)}}{\neg \env {\Gamma,e,t} (\varpi)})\\ \constr{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\env {\Gamma,e,t} (\varpi)}\\ \constr{\varpi.l}{\Gamma,e,t} & = & \bpl{\env {\Gamma,e,t} (\varpi)}\\ \constr{\varpi.r}{\Gamma,e,t} & = & \bpr{\env {\Gamma,e,t} (\varpi)}\\ \constr{\varpi.f}{\Gamma,e,t} & = & \pair{\env {\Gamma,e,t} (\varpi)}\Any\\ \constr{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\env {\Gamma,e,t} (\varpi)}\\ \env {\Gamma,e,t} (\varpi) & = & \tsrep {\constr \varpi {\Gamma,e,t} \tsand \tyof {\occ e \varpi} \Gamma} \end{eqnarray} \begin{align*} &\RefineStep {e,t} (\Gamma) = \Gamma' \text{ with:}\\ &\dom{\Gamma'}=\dom{\Gamma} \cup \{e' \alt \exists \varpi.\ \occ e \varpi \equiv e'\}\\ &\Gamma'(e') = \left\{\begin{array}{ll} \bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}} \env {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\ \Gamma(e') & \text{otherwise} \end{array}\right.\\&\\ &\Refine {e,t} \Gamma={\RefineStep {e,t}}^{n_o}(\Gamma)\qquad\text{with n a global parameter} \end{align*} \subsection{Proofs for the algorithmic type system with type schemes} This section is about the algorithmic type system with type schemes (soundness and some completeness properties). Note that, now that we have type schemes, use a different but more convenient definition for \tyof e \Gamma that the one in Section~\ref{sec:typenv}: \begin{align*} \tyof e \Gamma = \left\{\begin{array}{ll} \ts & \text{if } \Gamma \vdashAts e:\ts \\ \tsempty & \text{otherwise} \end{array}\right. \end{align*} In this way, \tyof e \Gamma is always defined but is equal to \tsempty when e is not well-typed in \Gamma. We will reuse the definitions and notations introduced in the previous proofs. In particular, we only consider well-formed environments, as in the proofs of the declarative type system. \subsubsection{Soundness} \begin{theorem}[Soundness of the algorithm]\label{soundnessAts} For every \Gamma, e, t, n_o, if \tyof e \Gamma \leq t, then we can derive \Gamma \vdash e:t. More precisely: \begin{align*} &\forall \Gamma, e, t.\ \tyof e \Gamma \leq t \Rightarrow \Gamma \vdash e:t\\ &\forall \Gamma, e, t, \varpi.\ \tyof e \Gamma \neq \tsempty \Rightarrow \pvdash \Gamma e t \varpi:\env {\Gamma,e,t} (\varpi)\\ &\forall \Gamma, e, t.\ \tyof e \Gamma \neq \tsempty \Rightarrow \Gamma \evdash e t \Refine {e,t} \Gamma \end{align*} \end{theorem} \begin{proof} We proceed by induction over the structure of e and, for two identical e, on the domain of \Gamma (with the inclusion order). Let's prove the first property. Let t such that \tsint{\tyof e \Gamma} \leq t. If \Gamma = \bot, we trivially have \Gamma \vdash e:t with the rule \Rule{Efq}. Let's assume \Gamma \neq \bot. If e=x is a variable, then the last rule used is \Rule{Var\Aats}. We can derive \Gamma \vdash x:t by using the rule \Rule{Env} and \Rule{Subs}. So let's assume that e is not a variable. If e\in\dom\Gamma, then the last rule used is \Rule{Env\Aats}. Let t'\in\tsint{\ts} such that t'\land\Gamma(e)\leq t. The induction hypothesis gives \Gamma\setminus\{e\} \vdash e:t' (the premise uses the same e but the domain of \Gamma is strictly smaller). Thus, we can build a derivation \Gamma \vdash e:t by using the rules \Rule{Subs}, \Rule{Inter}, \Rule{Env} and the derivation \Gamma\setminus\{e\} \vdash e:t'. Now, let's suppose that e\not\in\dom\Gamma. \begin{description} \item[e=c] The last rule is \Rule{Const\Aats}. We derive easily \Gamma \vdash c:t with \Rule{Const} and \Rule{Subs}. \item[e=x] Already treated. \item[e=\lambda^{\bigwedge_{i\in I} \arrow {t_i}{s_i}}x.e'] The last rule is \Rule{Abs\Aats}. We have \bigwedge_{i\in I} \arrow {t_i}{s_i} \leq t. Using the definition of type schemes, let t'=\bigwedge_{i\in I} \arrow {t_i}{s_i} \land \bigwedge_{j\in J} \neg \arrow {t'_j}{s'_j} such that \Empty \neq t' \leq t. The induction hypothesis gives, for all i\in I, \Gamma,x:s_i\vdash e':t_i. Thus, we can derive \Gamma\vdash e:\bigwedge_{i\in I} \arrow {t_i}{s_i} using the rule \Rule{Abs+}, and with \Rule{Inter} and \Rule{Abs-} we can derive \Gamma\vdash e:t'. We can conclude by applying \Rule{Subs}. \item[e=e_1 e_2] The last rule is \Rule{App\Aats}. We have \apply {\ts_1} {\ts_2} \leq t. Thus, let t_1 and t_2 such that \ts_1 \leq t_1, \ts_2 \leq t_2 and \apply {t_1} {t_2} \leq t. We know, according to the descriptive definition of \apply {} {}, that there exists s\leq t such that t_1 \leq \arrow {t_2} s. By using the induction hypothesis, we have \Gamma\vdash e_1:t_1 and \Gamma\vdash e_2:t_2. We can thus derive \Gamma\vdash e_1:\arrow {t_2} s using \Rule{Subs}, and together with \Gamma\vdash e_2:t_2 it gives \Gamma\vdash e_1\ e_2:s with \Rule{App}. We conclude with \Rule{Subs}. \item[e=\pi_i e'] The last rule is \Rule{Proj\Aats}. We have \bpi_i \ts \leq t. Thus, let t' such that \ts \leq t' and \bpi_i t' \leq t. We know, according to the descriptive definition of \bpi_i, that there exists t_i\leq t such that t' \leq \pair \Any {t_i} (for i=2) or t' \leq \pair {t_i} \Any (for i=1). By using the induction hypothesis, we have \Gamma\vdash e':t', and thus we easily conclude using \Rule{Subs} and \Rule{Proj} (for instance for the case i=1, we can derive \Gamma\vdash e':\pair {t_i} \Any with \Rule{Subs} and then use \Rule{Proj}). \item[e=(e_1,e_2)] The last rule is \Rule{Pair\Aats}. We conclude easily with the induction hypothesis and the rules \Rule{Subs} and \Rule{Pair}. \item[e=\ite {e_0} t {e_1} {e_2}] The last rule is \Rule{Case\Aats}. We conclude easily with the induction hypothesis and the rules \Rule{Subs} and \Rule{Case} (for the application of \Rule{Case}, t' must be taken equal to t_1 \vee t_2 with t_1 and t_2 such that \ts_1\leq t_1, \ts_2\leq t_2 and t_1 \vee t_2 \leq t). \end{description}\ \\ Now, let's prove the second property. We perform a (nested) induction on \varpi. Recall that \env {\Gamma,e,t} (\varpi) = \tsrep {\constr \varpi {\Gamma,e,t} \tsand \tyof {\occ e \varpi} \Gamma}. For any t' such that \tyof {\occ e \varpi} \Gamma \leq t', we can easily derive \pvdash \Gamma e t \varpi : t' by using the outer induction hypothesis (the first property that we have proved above) and the rule \Rule{PTypeof}. Now we have to derive \pvdash \Gamma e t \varpi : \constr \varpi {\Gamma,e,t} (then it will be easy to conclude using the rule \Rule{PInter}). \begin{description} \item[\varpi=\epsilon] We use the rule \Rule{PEps}. \item[\varpi=\varpi'.1] Let's note f=\tsrep {\tyof {\occ e {\varpi'.0}} \Gamma}, s=\env {\Gamma,e,t} (\varpi') and t_{\text{res}} = \worra f s. By using the outer and inner induction hypotheses, we can derive \pvdash \Gamma e t \varpi'.0 : f and \pvdash \Gamma e t \varpi' : s. By using the descriptive definition of \worra {} {}, we have t' = \apply f {(\dom f \setminus t_{\text{res}})} \leq \neg s. Moreover, by using the descriptive definition of \apply {} {} on t', we have f \leq \arrow {(\dom f \setminus t_{\text{res}})} {t'}. As t'\leq \neg s, it gives f \leq \arrow {(\dom f \setminus t_{\text{res}})} {\neg s}. Let's note t_1 = \dom f \setminus t_{\text{res}} and t_2 = \neg s. The above inequality can be rewritten f \leq \arrow {t_1} {t_2}. Thus, by using \Rule{PSubs} on the derivation \pvdash \Gamma e t \varpi'.0 : f, we can derive \pvdash \Gamma e t \varpi'.0 : \arrow {t_1} {t_2}. We have: \begin{itemize} \item t_2 \land s \simeq \Empty (as t_2 = \neg s) \item \neg t_1 = t_{\text{res}} \vee \neg \dom f = t_{\text{res}} \end{itemize} In consequence, we can conclude by applying the rule \Rule{PAppR} with the premises \pvdash \Gamma e t \varpi'.0 : \arrow {t_1} {t_2} and \pvdash \Gamma e t \varpi' : s. \item[\varpi=\varpi'.0] By using the inner induction hypothesis and the previous case we've just proved, we can derive \pvdash \Gamma e t \varpi' : \env {\Gamma,e,t} (\varpi') and \pvdash \Gamma e t \varpi'.1 : \env {\Gamma,e,t} (\varpi'.1). Hence we can apply \Rule{PAppL}. \item[\varpi=\varpi'.l] Let's note t_1=\bpi_1 \env {\Gamma,e,t} (\varpi'). According to the descriptive definition of \bpi_1, we have \env {\Gamma,e,t} (\varpi') \leq \pair {t_1} {\Any}. The inner induction hypothesis gives \pvdash \Gamma e t \varpi' : \env {\Gamma,e,t} (\varpi'), and thus using the rule \Rule{PSubs} we can derive \pvdash \Gamma e t \varpi' : \pair {t_1} \Any. We can conclude just by applying the rule \Rule{PPairL} to this premise. \item[\varpi=\varpi'.r] This case is similar to the previous. \item[\varpi=\varpi'.f] The inner induction hypothesis gives \pvdash \Gamma e t \varpi' : \env {\Gamma,e,t} (\varpi'), so we can conclude by applying \Rule{PFst}. \item[\varpi=\varpi'.s] The inner induction hypothesis gives \pvdash \Gamma e t \varpi' : \env {\Gamma,e,t} (\varpi'), so we can conclude by applying \Rule{PSnd}. \end{description}\ \\ Finally, let's prove the third property. Let \Gamma' = \Refine {e,t} \Gamma = {\RefineStep{e,t}}^{n_0}(\Gamma). We want to show that \Gamma \evdash e t \Gamma' is derivable. First, let's note that \evdash e t is transitive: if \Gamma \evdash e t \Gamma' and \Gamma' \evdash e t \Gamma'', then \Gamma \evdash e t \Gamma''. The proof is quite easy: we can just start from the derivation of \Gamma \evdash e t \Gamma', and we add at the end a slightly modified version of the derivation of \Gamma' \evdash e t \Gamma'' where: \begin{itemize} \item the initial \Rule{Base} rule has been removed in order to be able to do the junction, \item all the \Gamma' at the left of \evdash e t are replaced by \Gamma (the proof is still valid as this \Gamma' at the left is never used in any rule) \end{itemize} Thanks to this property, we can suppose that n_0 = 1 (and so \Gamma' = \RefineStep{e,t}(\Gamma)). If it is not the case, we just have to proceed by induction on n_0 and use the transitivity property. Let's build a derivation for \Gamma \evdash e t \Gamma'. By using the proof of the second property on e that we've done just before, we get: \forall \varpi.\ \pvdash \Gamma e t \varpi: \env {\Gamma,e,t} (\varpi). Let's recall a monotonicity property: for any \Gamma_1 and \Gamma_2 such that \Gamma_2 \leq \Gamma_1, we have \forall t'.\ \pvdash {\Gamma_1} e t \varpi:t' \Rightarrow \pvdash {\Gamma_2} e t \varpi:t'.\\ Moreover, when we also have \occ e \varpi \in\dom{\Gamma_2}, we can derive \pvdash {\Gamma_2} e t \varpi:t'\land\Gamma_2(\occ e \varpi) (just by adding a \Rule{PInter} rule with a \Rule{PTypeof} and a \Rule{Env}). Hence, we can apply successively a \Rule{Path} rule for all valid \varpi in e, with the following premises (\Gamma_\varpi being the previous environment, that trivially verifies \Gamma_\varpi\leq\Gamma):\\ \begin{tabular}{lll} If \occ e \varpi \in\dom{\Gamma_\varpi}&\pvdash {\Gamma_\varpi} e t \varpi: \env {\Gamma,e,t} (\varpi)\land\Gamma_\varpi(\occ e \varpi)&\Gamma\evdash e t {\Gamma_\varpi}\\ Otherwise&\pvdash {\Gamma_\varpi} e t \varpi: \env {\Gamma,e,t} (\varpi)&\Gamma\evdash e t {\Gamma_\varpi} \end{tabular} At the end, it gives the judgement \Gamma \evdash e t \Gamma', so it concludes the proof. \end{proof} \subsubsection{Completeness} \begin{definition}[Bottom environment] Let \Gamma an environment.\\ \Gamma is bottom (noted \Gamma = \bot) iff \exists e\in\dom\Gamma.\ \Gamma(e)\simeq\Empty. \end{definition} \begin{definition}[Algorithmic (pre)order on environments] Let \Gamma and \Gamma' two environments. We write \Gamma' \leqA \Gamma iff: \begin{align*} &\Gamma'=\bot \text{ or } (\Gamma\neq\bot \text{ and } \forall e \in \dom \Gamma.\ \tyof e \Gamma \leq \Gamma(e)) \end{align*} For an expression e, we write \Gamma' \leqA^e \Gamma iff: \begin{align*} &\Gamma'=\bot \text{ or } (\Gamma\neq\bot \text{ and } \forall e' \in \dom \Gamma \text{ such that e' is a subexpression of e}.\ \tyof {e'} \Gamma \leq \Gamma({e'})) \end{align*} Note that if \Gamma' \leqA \Gamma, then \Gamma' \leqA^e \Gamma for any e. \end{definition} \begin{definition}[Order relation for type schemes] Let \ts_1 and \ts_2 two type schemes. We write \ts_2 \leq \ts_1 iff \tsint {\ts_1} \subseteq \tsint{\ts_2}. \end{definition}  Mickael Laurent committed Sep 09, 2020 520  \begin{lemma} When well-defined, the following inequalities hold:  Giuseppe Castagna committed Mar 03, 2020 521 522  \begin{align*} &\forall t,\ts.\ \tsrep{t\tsand\ts} \leq t \land \tsrep{\ts}\\  Mickael Laurent committed Sep 09, 2020 523  &\forall t_1,t_2,\ts_1,\ts_2.\ t_1 \leq t_2 \text{ and } \ts_1\leq\ts_2 \text{ and } \tsrep{\ts_1}\leq\tsrep{\ts_2} \Rightarrow \tsrep{t_1\tsand\ts_1} \leq \tsrep{t_2\tsand\ts_2}\\  Giuseppe Castagna committed Mar 03, 2020 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626  &\forall \ts_1,\ts_2.\ \tsrep{\apply {\ts_1}{\ts_2}} \leq \apply {\tsrep {\ts_1}}{\tsrep {\ts_2}} \end{align*} \end{lemma} \begin{proof} Straightfoward, by induction on the structure of \ts. \end{proof} \begin{lemma}[Monotonicity of the algorithm] Let \Gamma, \Gamma' and e such that \Gamma'\leqA^e \Gamma and \tyof e \Gamma \neq \tsempty. We have: \begin{align*} &\tyof e {\Gamma'} \leq \tyof e {\Gamma} \text{ and } \tsrep{\tyof e {\Gamma'}} \leq \tsrep{\tyof e {\Gamma}}\\ &\forall t,\varpi.\ \env {\Gamma',e,t} (\varpi) \leq \env {\Gamma,e,t} (\varpi)\\ &\forall t.\ \Refine {e,t} {\Gamma'} \leqA^e \Refine {e,t} \Gamma\\ \end{align*} \end{lemma} \begin{proof} We proceed by induction over the structure of e and, for two identical e, on the domains of \Gamma and \Gamma' (with the lexicographical inclusion order). Let's prove the first property: \tyof e {\Gamma'} \leq \tyof e {\Gamma} \text{ and } \tsrep{\tyof e {\Gamma'}} \leq \tsrep{\tyof e {\Gamma}}. We will focus on showing \tyof e {\Gamma'} \leq \tyof e {\Gamma}. The property \tsrep{\tyof e {\Gamma'}} \leq \tsrep{\tyof e {\Gamma}} can be proved in a very similar way, by using the fact that operators on type schemes like \tsand or \apply {} {} are also monotone. (Note that the only rule that introduces the type scheme constructor \tsfun {\_} is \Rule{Abs\Aats}.) If \Gamma' = \bot we can conclude directly with the rule \Rule{Efq\Aats}. So let's assume \Gamma' \neq \bot and \Gamma \neq \bot (as \Gamma = \bot \Rightarrow \Gamma' = \bot by definition of \leqA^e). If e=x is a variable, then the last rule used in \tyof e \Gamma and \tyof e {\Gamma'} is \Rule{Var\Aats}. As \Gamma' \leqA^e \Gamma, we have \Gamma'(e) \leq \Gamma(e) and thus we can conclude with the rule \Rule{Var\Aats}. So let's assume that e is not a variable. If e\in\dom\Gamma, then the last rule used in \tyof e \Gamma is \Rule{Env\Aats}. As \Gamma' \leqA^e \Gamma, we have \tyof e {\Gamma'} \leq \Gamma(e). Moreover, by applying the induction hypothesis, we get \tyof e {\Gamma'\setminus \{e\}} \leq \tyof e {\Gamma\setminus \{e\}} (we can easily verify that \Gamma'\setminus\{e\} \leqA^e \Gamma\setminus\{e\}). \begin{itemize} \item If we have e\in\dom{\Gamma'}, we have according to the rule \Rule{Env\Aats} \tyof e {\Gamma'} \leq \tyof e {\Gamma'\setminus \{e\}} \leq \tyof e {\Gamma\setminus \{e\}}. Together with \tyof e {\Gamma'} \leq \Gamma(e), we deduce \tyof e {\Gamma'} \leq \Gamma(e) \tsand \tyof e {\Gamma\setminus \{e\}} = \tyof e {\Gamma}. \item Otherwise, we have e\not\in\dom{\Gamma'}. Thus \tyof e {\Gamma'} = \tyof e {\Gamma'\setminus \{e\}} \leq \Gamma(e) \tsand \tyof e {\Gamma\setminus \{e\}}=\tyof e {\Gamma}. \end{itemize} If e\not\in\dom\Gamma and e\in\dom{\Gamma'}, the last rule is \Rule{Env\Aats} for \tyof e {\Gamma'}. As \Gamma'\setminus\{e\} \leqA^e \Gamma\setminus\{e\} = \Gamma, we have \tyof e {\Gamma'} \leq \tyof e {\Gamma'\setminus \{e\}} \leq \tyof e {\Gamma} by induction hypothesis. Thus, let's suppose that e\not\in\dom\Gamma and e\not\in\dom{\Gamma'}. From now we know that the last rule in the derivation of \tyof e {\Gamma} and \tyof e {\Gamma'} (if any) is the same. \begin{description} \item[e=c] The last rule is \Rule{Const\Aats}. It does not depend on \Gamma so this case is trivial. \item[e=x] Already treated. \item[e=\lambda^{\bigwedge_{i\in I} \arrow {t_i}{s_i}}x.e'] The last rule is \Rule{Abs\Aats}. We have \forall i\in I.\ \Gamma', (x:s_i) \leqA^{e'} \Gamma, (x:s_i) (quite straightforward) so by applying the induction hypothesis we have \forall i\in I.\ \tyof {e'} {\Gamma', (x:s_i)} \leq \tyof {e'} {\Gamma, (x:s_i)}. \item[e=e_1 e_2] The last rule is \Rule{App\Aats}. We can conclude immediately by using the induction hypothesis and noticing that \apply {} {} is monotonic for both of its arguments. \item[e=\pi_i e'] The last rule is \Rule{Proj\Aats}. We can conclude immediately by using the induction hypothesis and noticing that \bpi_i is monotonic. \item[e=(e_1,e_2)] The last rule is \Rule{Pair\Aats}. We can conclude immediately by using the induction hypothesis. \item[e=\ite {e_0} t {e_1} {e_2}] The last rule is \Rule{Case\Aats}. By using the induction hypothesis we get \Refine {e_0,t} {\Gamma'} \leqA^{e_0} \Refine {e_0,t} \Gamma. We also have \Gamma' \leqA^{e_1} \Gamma (as e_1 is a subexpression of e). From those two properties, let's show that we can deduce \Refine {e_0,t} {\Gamma'} \leqA^{e_1} \Refine {e_0,t} \Gamma: Let e'\in\dom{\Refine {e_0,t} \Gamma} a subexpression of e_1. \begin{itemize} \item If e' is also a subexpression of e_0, we can directly deduce\\ \tyof {e'} {\Refine {e_0,t} \Gamma'} \leq (\Refine {e_0,t} \Gamma) (e') by using \Refine {e_0,t} {\Gamma'} \leqA^{e_0} \Refine {e_0,t} \Gamma. \item Otherwise, as \Refine {e_0,t} {\_} is reductive, we have \Refine {e_0,t} {\Gamma'} \leqA \Gamma' and thus by using the induction hypothesis \tyof {e'} {\Refine {e_0,t} {\Gamma'}} \leq \tyof {e'} {\Gamma'}. We also have \tyof {e'} {\Gamma'} \leq \Gamma(e') by using \Gamma' \leqA^{e_1} \Gamma. We deduce \tyof {e'} {\Refine {e_0,t} {\Gamma'}} \leq \Gamma(e') = (\Refine {e_0,t} \Gamma) (e'). \end{itemize} So we have \Refine {e_0,t} {\Gamma'} \leqA^{e_1} \Refine {e_0,t} \Gamma. Consequently, we can apply the induction hypothesis again to get \tyof {e_1} {\Refine {e_0,t} {\Gamma'}} \leq \tyof {e_1} {\Refine {e_0,t} {\Gamma}}. We proceed the same way for the last premise. \end{description}\ \\ Now, let's prove the second property. We perform a (nested) induction on \varpi.  Mickael Laurent committed Sep 09, 2020 627  Recall that we have \forall t_1,t_2,\ts_1,\ts_2.\ t_1 \leq t_2 \text{ and } \ts_1\leq\ts_2 \text{ and } \tsrep{\ts_1}\leq\tsrep{\ts_2} \Rightarrow \tsrep{t_1\tsand\ts_1} \leq \tsrep{t_2\tsand\ts_2} (lemma above).  Giuseppe Castagna committed Mar 03, 2020 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 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 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037  Thus, in order to prove \tsrep {\constr {\varpi} {\Gamma',e,t} \tsand \tyof {\occ e \varpi} {\Gamma'}} \leq \tsrep {\constr {\varpi} {\Gamma,e,t} \tsand \tyof {\occ e \varpi} {\Gamma}}, we can prove the following: \begin{align*} &\constr {\varpi} {\Gamma',e,t} \leq \constr {\varpi} {\Gamma,e,t}\\ &\tyof {\occ e \varpi} {\Gamma'} \leq \tyof {\occ e \varpi} {\Gamma}\\ &\tsrep{\tyof {\occ e \varpi} {\Gamma'}} \leq \tsrep{\tyof {\occ e \varpi} {\Gamma}} \end{align*} The two last inequalities can be proved with the outer induction hypothesis (for \varpi=\epsilon we use the proof of the first property above). Thus we just have to prove that \constr {\varpi} {\Gamma',e,t} \leq \constr {\varpi} {\Gamma,e,t}. The only case that is interesting is the case \varpi=\varpi'.1. First, we can notice that the \worra {} {} operator is monotonic for its second argument (consequence of its declarative definition). Secondly, let's show that for any function types t_1 \leq t_2, and for any type t', we have (\worra {t_1} {t'}) \land \dom {t_2} \leq \worra {t_2} {t'}. By the absurd, let's suppose it is not true. Let's note t'' = (\worra {t_1} {t'}) \land \dom {t_2}. Then we have t'' \leq \dom {t_2} \leq \dom {t_1} and t_2 \leq \arrow {t''} {t'} and t_1 \not\leq \arrow {t''} {t'}, which contradicts t_1 \leq t_2. Let's note t_1 = \tsrep {\tyof{\occ e{\varpi'.0}}{\Gamma'}} and t_2 = \tsrep {\tyof{\occ e{\varpi'.0}}\Gamma} and t'=\env {\Gamma,e,t} (\varpi'). As e is well-typed, and using the inner induction hypothesis, we have \tsrep {\tyof {\occ e {\varpi'.1}} {\Gamma'}} \leq \tsrep {\tyof {\occ e {\varpi'.1}} {\Gamma}} \leq \dom {t_2}.\\ Thus, using this property, we get:\\ \begin{align*} &(\worra {t_1} {t'}) \land \tsrep {\tyof {\occ e {\varpi'.1}} {\Gamma'}}\\ \leq &(\worra {t_2} {t'}) \land \tsrep {\tyof {\occ e {\varpi'.1}} {\Gamma}} \end{align*} Then, using the monotonicity of the second argument of \worra {}{} and the outer induction hypothesis: \begin{align*} &(\worra {t_1} {\env {\Gamma',e,t} (\varpi')}) \land \tsrep {\tyof {\occ e {\varpi'.1}} {\Gamma'}}\\ \leq &(\worra {t_2} {\env {\Gamma,e,t} (\varpi')}) \land \tsrep {\tyof {\occ e {\varpi'.1}} {\Gamma}} \end{align*} \\ \ Finally, we must prove the third property.\\ It is straightforward by using the previous result and the induction hypothesis:\\ \forall e' s.t. \exists \varpi.\ \occ e \varpi \equiv e', we get \bigwedge_{\{\varpi\alt \occ e \varpi \equiv e'\}} \env {\Gamma',e,t} (\varpi) \leq \bigwedge_{\{\varpi\alt \occ e \varpi \equiv e'\}} \env {\Gamma,e,t} (\varpi). The rest follows. \end{proof} \begin{definition}[Positive derivation] A derivation of the declarative type system is said positive iff it does not contain any rule \Rule{Abs-}. \end{definition} \begin{theorem}[Completeness for positive derivations]\label{completenessAtsPositive} For every \Gamma, e, t such that we have a positive derivation of \Gamma \vdash e:t, there exists a global parameter n_o with which \tsrep{\tyof e \Gamma} \leq t. More precisely: \begin{align*} &\forall \Gamma, e, t.\ \Gamma \vdash e:t \text{ has a positive derivation } \Rightarrow \tsrep{\tyof e \Gamma} \leq t\\ &\forall \Gamma, \Gamma', e, t.\ \Gamma \evdash e t \Gamma' \text{ has a positive derivation } \Rightarrow \Refine {e,t} \Gamma \leqA \Gamma' \text{ (for n_o large enough)} \end{align*} \end{theorem} \begin{proof} We proceed by induction on the derivation. Let's prove the first property. We have a positive derivation of \Gamma \vdash e:t. If \Gamma = \bot, we can conclude directly using \Rule{Efq\Aats}. Thus, let's suppose \Gamma \neq \bot. If e=x is a variable, then the derivation only uses \Rule{Env}, \Rule{Inter} and \Rule{Subs}. We can easily conclude just be using \Rule{Var\Aats}. Thus, let's suppose e is not a variable. If e\in\dom\Gamma, we can have the rule \Rule{Env} applied to e in our derivation, but in this case there can only be \Rule{Inter} and \Rule{Subs} after it (not \Rule{Abs-} as we have a positive derivation). Thus, our derivation contains a derivation of \Gamma \vdash e:t' that does not use the rule \Rule{Env} on e and such that t'\land \Gamma(e) \leq t (actually, it is possible for our derivation to typecheck e only using the rule \Rule{Env}: in this case we can take t'=\Any and use the fact that \Gamma is well-formed). Hence, we can build a positive derivation for \Gamma\setminus\{e\} \vdash e:t'. By using the induction hypothesis we deduce that \tsrep{\tyof e {\Gamma\setminus\{e\}}} \leq t'. Thus, by looking at the rule \Rule{Env\Aats}, we deduce \tsrep{\tyof e \Gamma} \leq \Gamma(e) \land \tsrep{\tyof e {\Gamma\setminus\{e\}}} \leq t. It concludes this case, so let's assume e\not\in\dom\Gamma. Now we analyze the last rule of the derivation: \begin{description} \item[\Rule{Env}] Impossible case (e\not\in\dom\Gamma). \item[\Rule{Inter}] By using the induction hypothesis we get \tsrep{\tyof e \Gamma} \leq t_1 and \tsrep{\tyof e \Gamma} \leq t_2. Thus, we have \tsrep{\tyof e \Gamma} \leq t_1 \land t_2. \item[\Rule{Subs}] Trivial using the induction hypothesis. \item[\Rule{Const}] We know that the derivation of \tyof e \Gamma (if any) ends with the rule \Rule{Const\Aats}. Thus this case is trivial. \item[\Rule{App}] We know that the derivation of \tyof e \Gamma (if any) ends with the rule \Rule{App\Aats}. Let \ts_1 = \tyof {e_1} \Gamma and \ts_2 = \tyof {e_2} \Gamma. With the induction hypothesis we have \tsrep {\ts_1} \leq \arrow {t_1} {t_2} and \tsrep {\ts_2} \leq t_1, with t_2=t. According to the descriptive definition of \apply{}{}, we have \apply{\tsrep {\ts_1}}{\tsrep {\ts_2}} \leq \apply{\arrow {t_1}{t_2}}{t_1} \leq t_2. As we also have \tsrep{\apply {\ts_1} {\ts_2}} \leq \apply{\tsrep {\ts_1}}{\tsrep {\ts_2}}, we can conclude that \tyof e \Gamma \leq t_2=t. \item[\Rule{Abs+}] We know that the derivation of \tyof e \Gamma (if any) ends with the rule \Rule{Abs\Aats}. This case is straightforward using the induction hypothesis. \item[\Rule{Abs-}] This case is impossible (the derivation is positive). \item[\Rule{Case}] We know that the derivation of \tyof e \Gamma (if any) ends with the rule \Rule{Case\Aats}. By using the induction hypothesis and the monotonicity lemma, we get \tsrep{\ts_1}\leq t and \tsrep{\ts_2}\leq t. So we have \tsrep{\ts_1\tsor\ts_2}=\tsrep{\ts1}\vee\tsrep{\ts2}\leq t. \item[\Rule{Proj}] Quite similar to the case \Rule{App}. \item[\Rule{Pair}] We know that the derivation of \tyof e \Gamma (if any) ends with the rule \Rule{Pair\Aats}. We just use the induction hypothesis and the fact that \tsrep{\ts_1\tstimes\ts_2}=\pair {\tsrep{\ts1}} {\tsrep{\ts2}}. \end{description} \ Now, let's prove the second property. We have a positive derivation of \Gamma \evdash e t \Gamma'. \begin{description} \item[\Rule{Base}] Any value of n_o will give \Refine {e,t} \Gamma \leqA \Gamma, even n_o = 0. \item[\Rule{Path}] We have \Gamma' = \Gamma_1,(\occ e \varpi:t'). By applying the induction hypothesis on the premise \Gamma \evdash e t \Gamma_1, we have \RefineStep {e,t}^n (\Gamma) = \Gamma_2 with \Gamma_2 \leqA \Gamma_1 for a certain n. We now proceed by induction on the derivation \pvdash {\Gamma_1} e t \varpi:t' to show that we can obtain \env {\Gamma'',e,t} (\varpi) \leq t' with \Gamma'' = \RefineStep {e,t}^{n'} (\Gamma_2) for a certain n'. It is then easy to conclude by taking n_o = n+n'. \begin{description} \item[\Rule{PSubs}] Trivial using the induction hypothesis. \item[\Rule{PInter}] By using the induction hypothesis we get: \begin{align*} &\env {\Gamma_1'',e,t} (\varpi) \leq t_1\\ &\env {\Gamma_2'',e,t} (\varpi) \leq t_2\\ &\RefineStep {e,t}^{n_1} (\Gamma_1) \leqA \Gamma_1''\\ &\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2'' \end{align*} By taking n'=\max (n_1,n_2), we can have \Gamma'' = \RefineStep {e,t}^{n'} (\Gamma_2) with \Gamma'' \leqA \Gamma_1'' and \Gamma'' \leqA \Gamma_2''. Thus, by using the monotonicity lemma, we can obtain \env {\Gamma'',e,t} (\varpi) \leq t_1 \land t_2 = t'. \item[\Rule{PTypeof}] By using the outer induction hypothesis we get \tsrep{\tyof {\occ e \varpi} {\Gamma_2}} \leq t'. Moreover we have \env {\Gamma_2,e,t} (\varpi) \leq \tsrep{\tyof {\occ e \varpi} {\Gamma_2}} (by definition of \env {}), thus we can conclude directly. \item[\Rule{PEps}] Trivial. \item[\Rule{PAppR}] By using the induction hypothesis we get: \begin{align*} &\env {\Gamma_1'',e,t} (\varpi.0) \leq \arrow {t_1} {t_2}\\ &\env {\Gamma_2'',e,t} (\varpi) \leq t_2'\\ & t_2\land t_2' \simeq \Empty\\ &\RefineStep {e,t}^{n_1} (\Gamma_1) \leqA \Gamma_1''\\ &\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2'' \end{align*} By taking n'=\max (n_1,n_2) + 1, we can have \Gamma'' = \RefineStep {e,t}^{n'} (\Gamma_2) with \Gamma'' \leqA \RefineStep {e,t} (\Gamma_1'') and \Gamma'' \leqA \RefineStep {e,t} (\Gamma_2''). In consequence, we have \tsrep{\tyof {\occ e {\varpi.0}} {\Gamma''}} \leq \env {\Gamma_1'',e,t} (\varpi.0) \leq \arrow {t_1} {t_2} (by definition of \RefineStep {e,t}). We also have, by monotonicity, \env {\Gamma'',e,t} (\varpi) \leq t_2'. As t_2\land t_2' \simeq \Empty, we have: \begin{align*} &\apply {(\arrow {t_1} {t_2})} {(\dom{\arrow {t_1} {t_2}}\setminus(\neg t_1))}\\ &\simeq \apply {(\arrow {t_1} {t_2})} {t_1} \simeq t_2 \leq \neg t_2' \end{align*} Thus, by using the declarative definition of \worra {} {}, we know that \worra {(\arrow {t_1} {t_2})} {t_2'} \leq \neg t_1. According to the properties on \worra {} {} that we have proved in the proof of the monotonicity lemma, we can deduce: \begin{align*} &t_1 \land \worra {\tsrep{\tyof {\occ e {\varpi.0}} {\Gamma''}}} {\env {\Gamma'',e,t} (\varpi)}\\ &\leq t_1 \land \worra {(\arrow {t_1} {t_2})} {t_2'} \leq t_1 \land \neg t_1 \simeq \Empty \end{align*} And thus \worra {\tsrep{\tyof {\occ e {\varpi.0}} {\Gamma''}}} {\env {\Gamma'',e,t} (\varpi)} \leq \neg t_1. It concludes this case. \item[\Rule{PAppL}] By using the induction hypothesis we get: \begin{align*} &\env {\Gamma_1'',e,t} (\varpi.1) \leq t_1\\ &\env {\Gamma_2'',e,t} (\varpi) \leq t_2\\ &\RefineStep {e,t}^{n_1} (\Gamma_1) \leqA \Gamma_1''\\ &\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2'' \end{align*} By taking n'=\max (n_1,n_2), we can have \Gamma'' = \RefineStep {e,t}^{n'} (\Gamma_2) with \Gamma'' \leqA \Gamma_1'' and \Gamma'' \leqA \Gamma_2''. Thus, by using the monotonicity lemma, we can obtain \env {\Gamma'',e,t} (\varpi.0) \leq \neg (\arrow {t_1} {\neg t_2}) = t'. \item[\Rule{PPairL}] Quite straightforward using the induction hypothesis and the descriptive definition of \bpi_1. \item[\Rule{PPairR}] Quite straightforward using the induction hypothesis and the descriptive definition of \bpi_2. \item[\Rule{PFst}] Trivial using the induction hypothesis. \item[\Rule{PSnd}] Trivial using the induction hypothesis. \end{description} \end{description} \end{proof} From this result, we will now prove a stronger but more complex completeness theorem. We were not able to prove full completeness, just a partial form of it. Indeed, the use of nested \Rule{PAppL} yields a precision that the algorithm loses by applying \tsrep{} in the definition of \constrf{}. Completeness is recovered by forbidding nested negated arrows on the left-hand side of negated arrows. \begin{definition}[Rank-0 negated derivation] A derivation of the declarative type system is said rank-0 negated iff any application of \Rule{PAppL} has a positive derivation as first premise (\pvdash \Gamma e t \varpi.1:t_1). \end{definition} \noindent The use of this terminology is borrowed from the ranking of higher-order types, since, intuitively, it corresponds to typing a language in which in the types used in dynamic tests, a negated arrow never occurs on the left-hand side of another negated arrow. \begin{lemma} If e is an application, then \tyof e \Gamma does not contain any constructor \tsfun \cdots. Consequently, we have \tsrep{\tyof e \Gamma} \simeq \tyof e \Gamma. \end{lemma} \begin{proof} By case analysis: neither \Rule{Efq\Aats}, \Rule{Env\Aats} nor \Rule{App\Aats} can produce a type containing a constructor \tsfun \cdots. \end{proof} \begin{theorem}[Completeness for rank-0 negated derivations] For every \Gamma, e, t such that we have a rank-0 negated derivation of \Gamma \vdash e:t, there exists a global parameter n_o with which \tyof e \Gamma \leq t. More precisely: \begin{align*} &\forall \Gamma, e, t.\ \Gamma \vdash e:t \text{ has a rank-0 negated derivation } \Rightarrow \tyof e \Gamma \leq t\\ &\forall \Gamma, \Gamma', e, t.\ \Gamma \evdash e t \Gamma' \text{ has a rank-0 negated derivation } \Rightarrow \Refine {e,t} \Gamma \leqA \Gamma' \text{ (for n_o large enough)} \end{align*} \end{theorem} \begin{proof} This proof is done by induction. It is quite similar to that of the completeness for positive derivations. In consequence, we will only detail cases that are quite different from those of the previous proof. Let's begin with the first property. We have a rank-0 negated derivation of \Gamma \vdash e:t. We want to show \tyof e \Gamma \leq t (note that this is weaker than showing \tsrep {\tyof e \Gamma} \leq t). As in the previous proof, we can suppose that \Gamma \neq \bot and that e is not a variable. The case e\in\dom\Gamma is also very similar, but there is an additional case to consider: the rule \Rule{Abs-} could possibly be used after a rule \Rule{Env} applied on e. However, this case can easily be eliminated by changing the premise of this \Rule{Abs-} with another one that does not use the rule \Rule{Env} on e (the type of the premise does not matter for the rule \Rule{Abs-}, even \Any suffices). Thus let's assume e\not\in\dom\Gamma. Now we analyze the last rule of the derivation (only the cases that are not similar are shown): \begin{description} \item[\Rule{Abs-}] We know that the derivation of \tyof e \Gamma (if any) ends with the rule \Rule{Abs\Aats}. Moreover, by using the induction hypothesis on the premise, we know that \tyof e \Gamma \neq \tsempty. Thus we have \tyof e \Gamma \leq \neg (\arrow {t_1} {t_2}) = t (because every type \neg (\arrow {s'} {t'}) such that \neg (\arrow {s'} {t'}) \land \bigwedge_{i\in I} \arrow {s_i} {t_i} \neq \Empty is in \tsint{\tsfun{\arrow {s_i} {t_i}}}). \end{description} \ Now let's prove the second property. We have a rank-0 negated derivation of \Gamma \evdash e t \Gamma'. \begin{description} \item[\Rule{Base}] Any value of n_o will give \Refine {e,t} \Gamma \leqA \Gamma, even n_o = 0. \item[\Rule{Path}] We have \Gamma' = \Gamma_1,(\occ e \varpi:t'). As in the previous proof of completeness, by applying the induction hypothesis on the premise \Gamma \evdash e t \Gamma_1, we have \RefineStep {e,t}^n (\Gamma) = \Gamma_2 with \Gamma_2 \leqA \Gamma_1 for a certain n. However, this time, we can't prove \env {\Gamma'',e,t} (\varpi) \leq t' with \Gamma'' = \RefineStep {e,t}^{n'} (\Gamma_2) for a certain n': the induction hypothesis is weaker than in the previous proof (we don't have \tsrep {\tyof e \Gamma} \leq t but only \tyof e \Gamma \leq t). Instead, we will prove by induction on the derivation \pvdash {\Gamma_1} e t \varpi:t' that \env {\Gamma'',e,t} (\varpi) \tsand \tyof {\occ e \varpi} {\Gamma''} \leq t'. It suffices to conclude in the same way as in the previous proof: by taking n_o = n+n', it ensures that our final environment \Gamma_{n_o} verifies \tyof {\occ e \varpi} \Gamma_{n_o} \leq t' and thus we have \Gamma_{n_o} \leq \Gamma' (given that \tsrep{\Empty} = \Empty, we also easily verify that if \Gamma' = \bot \Rightarrow \Gamma_{n_o}=\bot). \begin{description} \item[\Rule{PSubs}] Trivial using the induction hypothesis. \item[\Rule{PInter}] Quite similar to the previous proof (the induction hypothesis is weaker, but it works the same way). \item[\Rule{PTypeof}] By using the outer induction hypothesis we get \tyof {\occ e \varpi} {\Gamma_2} \leq t' so it is trivial. \item[\Rule{PEps}] Trivial. \item[\Rule{PAppR}] By using the induction hypothesis, we get: \begin{align*} &\env {\Gamma_1'',e,t} (\varpi.0) \tsand \tyof {\occ e {\varpi.0}} {\Gamma_1''} \leq \arrow {t_1} {t_2}\\ &\env {\Gamma_2'',e,t} (\varpi) \tsand \tyof {\occ e {\varpi}} {\Gamma_2''} \leq t_2'\\ &t_2 \land t_2' \simeq \Empty\\ &\RefineStep {e,t}^{n_1} (\Gamma_1) \leqA \Gamma_1''\\ &\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2'' \end{align*} Moreover, as \occ e {\varpi} is an application, we can use the lemma above to deduce \env {\Gamma_2'',e,t} (\varpi) \tsand \tyof {\occ e {\varpi}} {\Gamma_2''} = \env {\Gamma_2'',e,t} (\varpi) (see definition of \env {}). Thus we have \env {\Gamma_2'',e,t} (\varpi) \leq t_2'.\\ We also have \env {\Gamma_1'',e,t} (\varpi.0) \leq \tsrep{\env {\Gamma_1'',e,t} (\varpi.0) \tsand \tyof {\occ e {\varpi.0}} {\Gamma_1''}} \leq \arrow {t_1} {t_2}. Now we can conclude exactly as in the previous proof (by taking n'=\max (n_1,n_2)). \item[\Rule{PAppL}] We know that the left premise is a positive derivation. Thus, using the previous completeness theorem, we get: \begin{align*} &\env {\Gamma_1'',e,t} (\varpi.1) \leq t_1\\ &\RefineStep {e,t}^{n_1} (\Gamma_1) \leqA \Gamma_1'' \end{align*} By using the induction hypothesis, we also get: \begin{align*} &\env {\Gamma_2'',e,t} (\varpi) \tsand \tyof {\occ e {\varpi}} {\Gamma_2''} \leq t_2\\ &\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2'' \end{align*} Moreover, as \occ e {\varpi} is an application, we can use the lemma above to deduce \env {\Gamma_2'',e,t} (\varpi) \tsand \tyof {\occ e {\varpi}} {\Gamma_2''} = \env {\Gamma_2'',e,t} (\varpi) (see definition of \env {}). Thus we have \env {\Gamma_2'',e,t} (\varpi) \leq t_2. Now we can conclude exactly as in the previous proof (by taking n'=\max (n_1,n_2)). \item[\Rule{PPairL}] Quite straightforward using the induction hypothesis and the descriptive definition of \bpi_1. \item[\Rule{PPairR}] Quite straightforward using the induction hypothesis and the descriptive definition of \bpi_2. \item[\Rule{PFst}] Quite straightforward using the induction hypothesis. \item[\Rule{PSnd}] Quite straightforward using the induction hypothesis. \end{description} \end{description} \end{proof} \subsection{Proofs for the algorithmic type system without type schemes} \label{sec:proofs_algorithmic_without_ts} In this section, we consider the algorithmic type system without type schemes, as defined in \ref{sec:algorules}. \subsubsection{Soundness} \begin{lemma} \label{soundness_simple_ts} For every \Gamma, e, t, n_o, if \Gamma\vdashA e: t, then there exists \ts \leq t such that \Gamma \vdashAts e: \ts. \end{lemma} \begin{proof} Straightforward induction over the structure of e. \end{proof} \begin{theorem}[Soundness of the algorithmic type system without type schemes]\label{soundnessA} For every \Gamma, e, t, n_o, if \Gamma\vdashA e: t, then \Gamma \vdash e:t. \end{theorem} \begin{proof} Trivial by using the theorem \ref{soundnessAts} and the previous lemma. \end{proof} \subsubsection{Completeness} \[ \begin{array}{lrcl} \textbf{Simple type} & t_{s} & ::= & b \alt \pair {t_{s}} {t_{s}} \alt t_{s} \vee t_{s} \alt \neg t_{s} \alt \Empty \alt \arrow \Empty \Any\\ \textbf{Positive type} & t_+ & ::= & t_{s} \alt t_+ \vee t_+ \alt t_+ \land t_+ \alt \arrow {t_+} {t_+} \alt \arrow {t_+} {\neg t_+}\\ \textbf{Positive abstraction type} & t^\lambda_+ & ::= & \arrow {t_+} {t_+} \alt \arrow {t_+} {\neg t_+} \alt t^\lambda_+ \land t^\lambda_+\\ \textbf{Positive expression} & e_+ & ::= & c\alt x\alt e_+ e_+\alt\lambda^{t^\lambda_+} x.e_+\alt \pi_j e_+\alt(e_+,e_+)\alt\tcase{e_+}{t_{s}}{e_+}{e_+} \end{array} \begin{lemma} If we restrict the language to positive expressions $e_+$, then we have the following property: $\forall \Gamma, e_+, \ts.\ \Gamma \vdashAts e_+:\ts \Rightarrow \Gamma \vdashA e_+:\tsrep{\ts}$ \end{lemma} \begin{proof} We can prove it by induction over the structure of $e_+$. The main idea of this proof is that, as $e_+$ is a positive expression, the rule \Rule{Abs-} is not needed anymore because the negative part of functional types (i.e. the $N_i$ part of their DNF) becomes useless: \begin{itemize} \item When typing an application $e_1 e_2$, the negative part of the type of $e_1$ is ignored by the operator $\apply {} {}$. \item Moreover, as there is no negated arrows in the domain of lambda-abstractions, the negative arrows of the type of $e_2$ can also be ignored. \item Similarly, negative arrows can be ignored when refining an application ($\worra {} {}$ also ignore the negative part of the type of $e_1$). \item Finally, as the only functional type that we can test is $\arrow \Empty \Any$, a functional type cannot be refined to $\Empty$ due to its negative part, and thus we can ignore its negative part (it makes no difference relatively to the rule \Rule{Efq\Aats}). \end{itemize} \end{proof} \begin{theorem}[Completeness of the algorithmic type system for positive expressions]\label{completenessA} For every type environment $\Gamma$ and positive expression $e_+$, if $\Gamma\vdash e_+: t$, then there exist $n_o$ and $t'$ such that $\Gamma\vdashA e_+: t'$. \end{theorem} \begin{proof} Trivial by using the theorem \ref{completenessAtsPositive} and the previous lemma. \end{proof}