Merge branch 'master' of gitlab.math.univ-paris-diderot.fr:beppe/occurrence-typing

code_table.tex

@@ -133,6 +133,18 @@ let xor_ = fun (x : Any) -> fun (y : Any) ->
 $\True\to((\True\to\False)\land(\lnot\True\to\True))~\land$\newline
 $(\lnot\True\to((\True\to\True) \land (\lnot\True\to\False))$
     \\\hline
+
+ 10 & \begin{lstlisting}
+(* f and g have type:
+   (Int -> Int) & (Any ->Bool) *)
+
+let example10 =
+   fun (x : Any) ->
+     if (f x, g x) is (Int, Bool) then 1 else 2
+\end{lstlisting} &\vfill
+$(\Int\to\Empty)\land(\Any\setminus\Int\to{}2)$
+\texttt{Warning: line 4, charcater 39-40: expression is unreachable}
+    \\\hline
   \end{tabular}
 }
 \caption{Types inferred by implementation}\vspace{-10mm}

intro.tex

@@ -370,13 +370,13 @@ $\ifty{\textsf{false}}{\Bool}{\textsf{false}}{\textsf{true}}$): see Appendix~\re
 from the mutual dependence of different type checks. In particular, there are two cases
 that pose a problem. The first can be shown by two functions $f$ and $g$ both of type $(\Int\to\Int)\wedge(\Any\to\Bool)$, $x$ of type $\Any$ and the test:
 \begin{equation}\label{nest1}
-\ifty{(fx,gx)}{\pair\Int\Bool}{\,...\,}{\,...}
+\ifty{(f\,x,g\,x)}{\pair\Int\Bool}{\,...\,}{\,...}
 \end{equation}
-If we independently check $fx$ against $\Int$ and $gx$ against $\Bool$
+If we independently check $f\,x$ against $\Int$ and $g\,x$ against $\Bool$
 we deduce $\Int$ for the first occurrence of $x$ and $\Any$ for the
 second. Thus we would type the positive branch of \eqref{nest1} under the hypothesis
 that $x$ is of type $\Int$. But if we use the hypothesis generated by
-the test of $fx$, that is, that $x$ is of type \Int, to check $gx$ against \Bool,
+the test of $f\,x$, that is, that $x$ is of type \Int, to check $g\,x$ against \Bool,
 then the type deduced for $x$ is $\Empty$---i.e., the branch is never selected. In other words, we want to produce type
 environmments for occurrence typing by taking into account  all
 the available hypotheses, even when these hypotheses are formulated later

practical.tex

@@ -127,7 +127,7 @@ nodes. This splits, at the type level, the case for the \Keyw{Element}
 type depending on whether the content of the \texttt{childNodes} field
 is the empty list or not.
 
-Our implementation features one last enhancement that allows us
+Our implementation features another enhancement that allows us
 to further improve the precision of the inferred type.
 Consider the definition of the \texttt{xor\_} operator (Code~9).
 Here the rule~[{\sc AbsInf}+] is not sufficient to precisely type the
@@ -172,3 +172,21 @@ We consider \True, \Any, and $\lnot\True$ as candidate types for
   let xor_ = fun (x : Any) -> fun (y : Any) -> and_ (or_ x y) (not_ (and_ x y))
 \end{alltt}
 for which the very same types as in Table~\ref{tab:implem} are deduced.
+
+Last but not least Code~10 (which corresponds to our introductory
+Example~\ref{nest1}) illustrate the need for iterative refinement of
+type environments, as defined in Section~\ref{sec:typenv}. Indeed, has
+we have explained, a single pass analysis would deduce independently
+for {\tt x}
+a type \Int from the {\tt f~x} application and \Any from the {\tt g~x}
+application. Here by iterating a second time, the algorithm deduces
+that {\tt x} has type \Empty, that is that the first branch can never
+be selected (and our implementation warns the user accordingly). In
+hindsight, the only way for a well typed overloaded function to have
+type $(\Int\to\Int)\land(\Any\to\Bool)$ is to diverge when the
+argument is of type \Int (since this intersection types states that
+whenever the input is \Int, {\em both\/} branches can be selected,
+yielding a result that is at the same time an integer and a Boolean.
+This is precisely reflected by the case $\Int\to\Empty$ in the result.
+Indeed our {\tt example10} function can be applied to an integer, but
+at runtime the application of {\tt f ~x} will diverge.

proofs.tex

@@ -788,8 +788,6 @@
             This is equivalent to the wanted result.
             \end{proof}
 
-            \pagebreak
-        
             \begin{lemma}[$\worra {} {}$ alternative definition]
                 The following algorithmic definition for $\worra {} {}$ is equivalent to the previous one:
         
@@ -798,6 +796,8 @@
             \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)\\
@@ -826,8 +826,8 @@
                 & \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}
-            \pagebreak
         
             \begin{lemma}[Optimality of $\worra {} {}$]
                 Let $t$, $s$, two types.
@@ -1476,24 +1476,33 @@
           \end{description}
           \end{proof}
         
+          \[
+            \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{corollary}\label{app:completeness}
-            If we restrict our language so that the only functional type that can be used in a test is $\arrow \Empty \Any$
-            and such that there is no negated arrows in the domain of lambda-abstractions,
-            then the algorithmic type system becomes complete
-            (i.e. any expression that can be typed in the declarative type system is also typeable in the algorithmic one)
-            and type schemes can be removed from it (we can use regular types instead).
+            If we restrict the language to positive expressions $e_+$, the algorithmic type system is complete and type schemes can be removed from it (we can use regular types instead).
+            
+            More precisely:
+            $\forall \Gamma, e_+, t.\ \Gamma \vdash e_+:t \Rightarrow \tyof {e_+} \Gamma \neq \tsempty$
           \end{corollary}
         
           \begin{proof}
-            With such restrictions, the rule \Rule{Abs-} is not needed anymore.
+            With such restrictions, the rule \Rule{Abs-} is not needed anymore
+            because the negative part of functional types (i.e. the $N_i$ part of their DNF) is useless.
         
-            Indeed, when typing an application $e_1 e_2$, the negative part of the type of $e_1$ (i.e. the $N_i$ part of its DNF)
+            Indeed, when typing an application $e_1 e_2$, the negative part of the type of $e_1$ 
             is ignored by the operator $\apply {} {}$.
         
             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.
         
-            Similarly, negative arrows can also be ignored when refining an application ($\worra {} {}$ also ignore the negative part
+            Similarly, negative arrows can be ignored when refining an application ($\worra {} {}$ also ignore the negative part
             of the type of $e_1$).
         
             Finally, as the only functional type that we can test is $\arrow \Empty \Any$, a functional type
@@ -1540,7 +1549,7 @@
             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\Aa}.
-              Moreover, by using the induction hypothesis on the premise, we know that $\tyof e \Gamma \neq \varnothing$.
+              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}
@@ -1619,4 +1628,4 @@
             \end{description}
           \end{proof}
                           
-          \newpage
\ No newline at end of file
+          \newpage