### WIP Journal version :

- Make all negative vertical space conditional.
- Add mention about timing in the experimental part.
parent 21a3e35e
 ... @@ -16,7 +16,7 @@ rules% ... @@ -16,7 +16,7 @@ rules% particular connective (here, a type constructor, that is, either particular connective (here, a type constructor, that is, either $\to$, or $\times$, or $b$), while identity rules (e.g., axioms and $\to$, or $\times$, or $b$), while identity rules (e.g., axioms and cuts) and structural rules (e.g., weakening and contraction) do cuts) and structural rules (e.g., weakening and contraction) do not.\vspace{-3.3mm}} not.\svvspace{-3.3mm}} such as \Rule{Subs} and \Rule{Inter}. We handle this presence such as \Rule{Subs} and \Rule{Inter}. We handle this presence in the classic way: we define an algorithmic system that tracks the in the classic way: we define an algorithmic system that tracks the miminum type of an expression; this system is obtained from the miminum type of an expression; this system is obtained from the ... @@ -76,7 +76,7 @@ things get more difficult, since a function can be typed by, say, a ... @@ -76,7 +76,7 @@ things get more difficult, since a function can be typed by, say, a union of intersection of arrows and negations of types. Checking that union of intersection of arrows and negations of types. Checking that the function has a functional type is easy since it corresponds to the function has a functional type is easy since it corresponds to checking that it has a type subtype of $\Empty{\to}\Any$. Determining checking that it has a type subtype of $\Empty{\to}\Any$. Determining its domain and the type of the application is more complicated and needs the operators $\dom{}$ and $\circ$ we informally described in Section~\ref{sec:ideas} where we also introduced the operator $\worra{}{}$. These three operators are used by our algorithm and formally defined as:\vspace{-0.5mm} its domain and the type of the application is more complicated and needs the operators $\dom{}$ and $\circ$ we informally described in Section~\ref{sec:ideas} where we also introduced the operator $\worra{}{}$. These three operators are used by our algorithm and formally defined as:\svvspace{-0.5mm} \begin{eqnarray} \begin{eqnarray} \dom t & = & \max \{ u \alt t\leq u\to \Any\} \dom t & = & \max \{ u \alt t\leq u\to \Any\} \$-1mm] \\[-1mm] ... @@ -93,12 +93,12 @@ We need similar operators for projections since the type t ... @@ -93,12 +93,12 @@ We need similar operators for projections since the type t of e in \pi_i e may not be a single product type but, say, a union of e in \pi_i e may not be a single product type but, say, a union of products: all we know is that t must be a subtype of of products: all we know is that t must be a subtype of \pair\Any\Any. So let t be a type such that t\leq\pair\Any\Any, \pair\Any\Any. So let t be a type such that t\leq\pair\Any\Any, then we define:\vspace{-0.7mm} then we define:\svvspace{-0.7mm} \begin{equation} \begin{equation} \begin{array}{lcrlcr} \begin{array}{lcrlcr} \bpl t & = & \min \{ u \alt t\leq \pair u\Any\}\qquad&\qquad \bpl t & = & \min \{ u \alt t\leq \pair u\Any\}\qquad&\qquad \bpr t & = & \min \{ u \alt t\leq \pair \Any u\} \bpr t & = & \min \{ u \alt t\leq \pair \Any u\} \end{array}\vspace{-0.7mm} \end{array}\svvspace{-0.7mm} \end{equation} \end{equation} All the operators above but \worra{}{} are already present in the All the operators above but \worra{}{} are already present in the theory of semantic subtyping: the reader can find how to compute them theory of semantic subtyping: the reader can find how to compute them ... @@ -111,10 +111,10 @@ furthermore t\leq\Empty\to\Any, then t \simeq \bigvee_{i\in ... @@ -111,10 +111,10 @@ furthermore t\leq\Empty\to\Any, then t \simeq \bigvee_{i\in I}\left(\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in I}\left(\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n')\right) with \bigwedge_{p\in P_i}(s_p\to N_i}\neg(s_n'\to t_n')\right) with \bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n') \not\simeq \Empty for all t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n') \not\simeq \Empty for all i in I. For such a t and any type s then we have:\vspace{-1.0mm} i in I. For such a t and any type s then we have:\svvspace{-1.0mm} % % \begin{equation} \begin{equation} \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)\vspace{-1.0mm} \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)\svvspace{-1.0mm} \end{equation} \end{equation} The formula considers only the positive arrows of each summand that The formula considers only the positive arrows of each summand that forms t and states that, for each summand, whenever you take a subset forms t and states that, for each summand, whenever you take a subset ... @@ -136,7 +136,7 @@ extends \Gamma with hypotheses on the occurrences of e that are ... @@ -136,7 +136,7 @@ extends \Gamma with hypotheses on the occurrences of e that are the most general that can be deduced by assuming that e\,{\in}\,t succeeds. For that we need the notation \tyof{e}{\Gamma} which denotes the type deduced for e under the type environment \Gamma in the algorithmic type system of Section~\ref{sec:algorules}. the most general that can be deduced by assuming that e\,{\in}\,t succeeds. For that we need the notation \tyof{e}{\Gamma} which denotes the type deduced for e under the type environment \Gamma in the algorithmic type system of Section~\ref{sec:algorules}. That is, \tyof{e}{\Gamma}=t if and only if \Gamma\vdashA e:t is provable. That is, \tyof{e}{\Gamma}=t if and only if \Gamma\vdashA e:t is provable. We start by defining the algorithm for each single occurrence, that is for the deduction of \pvdash \Gamma e t \varpi:t'. This is obtained by defining two mutually recursive functions \constrf and \env{}{}:\vspace{-1.3mm} We start by defining the algorithm for each single occurrence, that is for the deduction of \pvdash \Gamma e t \varpi:t'. This is obtained by defining two mutually recursive functions \constrf and \env{}{}:\svvspace{-1.3mm} \begin{eqnarray} \begin{eqnarray} \constr\epsilon{\Gamma,e,t} & = & t\label{uno}\\[\sk] \constr\epsilon{\Gamma,e,t} & = & t\label{uno}\\[\sk] \constr{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\env {\Gamma,e,t}{(\varpi.1)}}{\neg \env {\Gamma,e,t} (\varpi)})\label{due}\\[\sk] \constr{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\env {\Gamma,e,t}{(\varpi.1)}}{\neg \env {\Gamma,e,t} (\varpi)})\label{due}\\[\sk] ... @@ -146,7 +146,7 @@ We start by defining the algorithm for each single occurrence, that is for the d ... @@ -146,7 +146,7 @@ We start by defining the algorithm for each single occurrence, that is for the d \constr{\varpi.f}{\Gamma,e,t} & = & \pair{\env {\Gamma,e,t} (\varpi)}\Any\label{sei}\\[\sk] \constr{\varpi.f}{\Gamma,e,t} & = & \pair{\env {\Gamma,e,t} (\varpi)}\Any\label{sei}\\[\sk] \constr{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\env {\Gamma,e,t} (\varpi)}\label{sette}\\[.8mm] \constr{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\env {\Gamma,e,t} (\varpi)}\label{sette}\\[.8mm] \env {\Gamma,e,t} (\varpi) & = & {\constr \varpi {\Gamma,e,t} \wedge \tyof {\occ e \varpi} \Gamma}\label{otto} \env {\Gamma,e,t} (\varpi) & = & {\constr \varpi {\Gamma,e,t} \wedge \tyof {\occ e \varpi} \Gamma}\label{otto} \end{eqnarray}\vspace{-5mm}\\ \end{eqnarray}\svvspace{-5mm}\\ All the functions above are defined if and only if the initial path All the functions above are defined if and only if the initial path \varpi is valid for e (i.e., \occ e{\varpi} is defined) and e \varpi is valid for e (i.e., \occ e{\varpi} is defined) and e is well-typed (which implies that all \tyof {\occ e{\varpi}} \Gamma is well-typed (which implies that all \tyof {\occ e{\varpi}} \Gamma ... @@ -159,7 +159,7 @@ in the definition are defined)% ... @@ -159,7 +159,7 @@ in the definition are defined)% this is defined for all \varpi since the first premisses of this is defined for all \varpi since the first premisses of \Rule{Case\Aa} states that \Gamma\vdash e:t_0 (and this is \Rule{Case\Aa} states that \Gamma\vdash e:t_0 (and this is possible only if we were able to deduce under the hypothesis possible only if we were able to deduce under the hypothesis \Gamma the type of every occurrence of e.)\vspace{-3mm}} \Gamma the type of every occurrence of e.)\svvspace{-3mm}} \else \else ; the well foundness of the definition can be deduced by analysing the rule~\Rule{Case\Aa} of Section~\ref{sec:algorules}. ; the well foundness of the definition can be deduced by analysing the rule~\Rule{Case\Aa} of Section~\ref{sec:algorules}. \fi \fi ... @@ -223,7 +223,7 @@ \Refinef yields for x a type strictly more precise than the type deduced in ... @@ -223,7 +223,7 @@ \Refinef yields for x a type strictly more precise than the type deduced in previous iteration. previous iteration. The solution we adopt in practice is to bound the number of iterations to some number n_o. This is obtained by the following definition of \Refinef\vspace{-1mm} The solution we adopt in practice is to bound the number of iterations to some number n_o. This is obtained by the following definition of \Refinef\svvspace{-1mm} \[ \[ \begin{array}{rcl} \begin{array}{rcl} \Refinef_{e,t} \eqdef (\RefineStep{e,t})^{n_o}\\[-2mm] \Refinef_{e,t} \eqdef (\RefineStep{e,t})^{n_o}\\[-2mm] ... @@ -234,7 +234,7 @@ The solution we adopt in practice is to bound the number of iterations to some ... @@ -234,7 +234,7 @@ The solution we adopt in practice is to bound the number of iterations to some \Gamma(e') & \text{otherwise, if } e'\in\dom\Gamma\\ \Gamma(e') & \text{otherwise, if } e'\in\dom\Gamma\\ \text{undefined} & \text{otherwise} \text{undefined} & \text{otherwise} \end{array}\right. \end{array}\right. \end{array}\vspace{-1.5mm} \end{array}\svvspace{-1.5mm}$ \] Note in particular that $\Refine{e,t}\Gamma$ extends $\Gamma$ with hypotheses on the expressions occurring in $e$, since Note in particular that $\Refine{e,t}\Gamma$ extends $\Gamma$ with hypotheses on the expressions occurring in $e$, since $\dom{\Refine{e,t}\Gamma} = \dom{\RefineStep {e,t}(\Gamma)} = \dom{\Gamma} \cup \{e' \alt \exists \varpi.\ \occ e \varpi \equiv e'\}$. $\dom{\Refine{e,t}\Gamma} = \dom{\RefineStep {e,t}(\Gamma)} = \dom{\Gamma} \cup \{e' \alt \exists \varpi.\ \occ e \varpi \equiv e'\}$. ... @@ -275,7 +275,7 @@ We now have all the definitions we need for our typing algorithm% ... @@ -275,7 +275,7 @@ We now have all the definitions we need for our typing algorithm% { } { } { \Gamma \vdashA x: \Gamma(x) } { \Gamma \vdashA x: \Gamma(x) } { x\in\dom\Gamma} { x\in\dom\Gamma} \vspace{-2mm}\\ \svvspace{-2mm}\\ \Infer[Env\Aa] \Infer[Env\Aa] { \Gamma\setminus\{e\} \vdashA e : t } { \Gamma\setminus\{e\} \vdashA e : t } { \Gamma \vdashA e: \Gamma(e) \wedge t } { \Gamma \vdashA e: \Gamma(e) \wedge t } ... @@ -285,7 +285,7 @@ We now have all the definitions we need for our typing algorithm% ... @@ -285,7 +285,7 @@ We now have all the definitions we need for our typing algorithm% { } { } {\Gamma\vdashA c:\basic{c}} {\Gamma\vdashA c:\basic{c}} {c\not\in\dom\Gamma} {c\not\in\dom\Gamma} \vspace{-2mm}\\ \svvspace{-2mm}\\ \ifsubmission\else \ifsubmission\else \end{mathpar} \end{mathpar} \begin{mathpar} \begin{mathpar} ... @@ -296,7 +296,7 @@ We now have all the definitions we need for our typing algorithm% ... @@ -296,7 +296,7 @@ We now have all the definitions we need for our typing algorithm% \Gamma\vdashA\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle\wedge_{i\in I} {\arrow {s_i} {t_i}} \Gamma\vdashA\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle\wedge_{i\in I} {\arrow {s_i} {t_i}} } } {\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e\not\in\dom\Gamma} {\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e\not\in\dom\Gamma} \vspace{-2mm}\\ \svvspace{-2mm}\\ \Infer[App\Aa] \Infer[App\Aa] { { \Gamma \vdashA e_1: t_1\\ \Gamma \vdashA e_1: t_1\\ ... @@ -306,7 +306,7 @@ We now have all the definitions we need for our typing algorithm% ... @@ -306,7 +306,7 @@ We now have all the definitions we need for our typing algorithm% } } { \Gamma \vdashA {e_1}{e_2}: t_1 \circ t_2 } { \Gamma \vdashA {e_1}{e_2}: t_1 \circ t_2 } { {e_1}{e_2}\not\in\dom\Gamma} { {e_1}{e_2}\not\in\dom\Gamma} \vspace{-2mm}\\ \svvspace{-2mm}\\ \Infer[Case\Aa] \Infer[Case\Aa] {\Gamma\vdashA e:t_0\\ {\Gamma\vdashA e:t_0\\ %\makebox{$\begin{array}{l} %\makebox{$\begin{array}{l} ... @@ -326,7 +326,7 @@ We now have all the definitions we need for our typing algorithm% ... @@ -326,7 +326,7 @@ We now have all the definitions we need for our typing algorithm% {\Gamma\vdashA \tcase {e} t {e_1}{e_2}: t_1\vee t_2} {\Gamma\vdashA \tcase {e} t {e_1}{e_2}: t_1\vee t_2} %{\ite {e} t {e_1}{e_2}\not\in\dom\Gamma} %{\ite {e} t {e_1}{e_2}\not\in\dom\Gamma} { \tcase {e} {t\!} {\!e_1\!}{\!e_2}\not\in\dom\Gamma} { \tcase {e} {t\!} {\!e_1\!}{\!e_2}\not\in\dom\Gamma} \vspace{-2mm} \\ \svvspace{-2mm} \\ \Infer[Proj\Aa] \Infer[Proj\Aa] {\Gamma \vdashA e:t\and \!\!t\leq\pair{\Any\!}{\!\Any}} {\Gamma \vdashA e:t\and \!\!t\leq\pair{\Any\!}{\!\Any}} {\Gamma \vdashA \pi_i e:\bpi_{\mathbf{i}}(t)} {\Gamma \vdashA \pi_i e:\bpi_{\mathbf{i}}(t)} ... @@ -429,11 +429,11 @@ rule \Rule{Path} and $(ii)$ the use of nested \Rule{PAppL} that yields ... @@ -429,11 +429,11 @@ rule \Rule{Path} and $(ii)$ the use of nested \Rule{PAppL} that yields a precision that the algorithm loses by using type schemes in defining of \constrf{} (case~\eqref{due} is the critical a precision that the algorithm loses by using type schemes in defining of \constrf{} (case~\eqref{due} is the critical one). Completeness is recovered by $(i)$ limiting the depth of the one). Completeness is recovered by $(i)$ limiting the depth of the derivations and $(ii)$ forbidding nested negated arrows on the derivations and $(ii)$ forbidding nested negated arrows on the left-hand side of negated arrows.\vspace{-.7mm} left-hand side of negated arrows.\svvspace{-.7mm} \begin{definition}[Rank-0 negation] \begin{definition}[Rank-0 negation] A derivation of $\Gamma \vdash e:t$ is \emph{rank-0 negated} if A derivation of $\Gamma \vdash e:t$ is \emph{rank-0 negated} if \Rule{Abs--} never occurs in the derivation of a left premise of a \Rule{Abs--} never occurs in the derivation of a left premise of a \Rule{PAppL} rule.\vspace{-.7mm} \Rule{PAppL} rule.\svvspace{-.7mm} \end{definition} \end{definition} \noindent The use of this terminology is borrowed from the ranking of higher-order \noindent The use of this terminology is borrowed from the ranking of higher-order types, since, intuitively, it corresponds to typing a language in types, since, intuitively, it corresponds to typing a language in ... ...
 ... @@ -150,7 +150,7 @@ $(\Int\to\textsf{Empty})\land(\neg\Int\to{}2)$\newline ... @@ -150,7 +150,7 @@ $(\Int\to\textsf{Empty})\land(\neg\Int\to{}2)$\newline } } \caption{Types inferred by the implementation} \caption{Types inferred by the implementation} \ifsubmission% \ifsubmission% \vspace{-10mm} \svvspace{-10mm} \fi% \fi% \label{tab:implem} \label{tab:implem} \end{table} \end{table}
 ... @@ -64,11 +64,11 @@ field $\ell = t \vee \Undef$% ... @@ -64,11 +64,11 @@ field $\ell = t \vee \Undef$% For what concerns \emph{expressions}, we cannot use CDuce record expressions For what concerns \emph{expressions}, we cannot use CDuce record expressions as they are, but we must adapt them to our analysis. In particular, we as they are, but we must adapt them to our analysis. In particular, we consider records that are built starting from the empty record expression \erecord{} by adding, updating, or removing fields:\vspace{-0.75mm} consider records that are built starting from the empty record expression \erecord{} by adding, updating, or removing fields:\svvspace{-0.75mm} $\[ \begin{array}{lrcl} \begin{array}{lrcl} \textbf{Expr} & e & ::= & \erecord {} ~\alt~ \recupd e \ell e ~\alt~ \recdel e \ell ~\alt~ e.\ell \textbf{Expr} & e & ::= & \erecord {} ~\alt~ \recupd e \ell e ~\alt~ \recdel e \ell ~\alt~ e.\ell \end{array}\vspace{-.75mm} \end{array}\svvspace{-.75mm}$ \] in particular $\recdel e \ell$ deletes the field $\ell$ from $e$, $\recupd e \ell e'$ adds the field $\ell=e'$ to the record $e$ (deleting any existing $\ell$ field), while $e.\ell$ is field selection with the reduction: in particular $\recdel e \ell$ deletes the field $\ell$ from $e$, $\recupd e \ell e'$ adds the field $\ell=e'$ to the record $e$ (deleting any existing $\ell$ field), while $e.\ell$ is field selection with the reduction: $$\erecord{...,\ell=e,...}.\ell\ \reduces\ e$$. $$\erecord{...,\ell=e,...}.\ell\ \reduces\ e$$. ... @@ -77,7 +77,7 @@ To define record type subtyping and record expression type inference we need thr ... @@ -77,7 +77,7 @@ To define record type subtyping and record expression type inference we need thr % % Then two record types $t_1$ and $t_2$ are in subtyping relation, $t_1 \leq t_2$, if and only if for all $\ell \in \Labels$ we have $\proj \ell {t_1} \leq \proj \ell {t_2}$. In particular $\orecord{\!\!}$ is the largest record type. Then two record types $t_1$ and $t_2$ are in subtyping relation, $t_1 \leq t_2$, if and only if for all $\ell \in \Labels$ we have $\proj \ell {t_1} \leq \proj \ell {t_2}$. In particular $\orecord{\!\!}$ is the largest record type. Expressions are then typed by the following rules (already in algorithmic form).\vspace{-.1mm} Expressions are then typed by the following rules (already in algorithmic form).\svvspace{-.1mm} \begin{mathpar} \begin{mathpar} \Infer[Record] \Infer[Record] {~} {~} ... @@ -90,7 +90,7 @@ Expressions are then typed by the following rules (already in algorithmic form). ... @@ -90,7 +90,7 @@ Expressions are then typed by the following rules (already in algorithmic form). {\recupd{e_1\!\!}{\!\!\ell}{e_2} \not\in\dom\Gamma} {\recupd{e_1\!\!}{\!\!\ell}{e_2} \not\in\dom\Gamma} %\end{mathpar} %\end{mathpar} %\begin{mathpar} %\begin{mathpar} \vspace{-1.9mm} \svvspace{-1.9mm} \\ \\ \Infer[Delete] \Infer[Delete] {\Gamma \vdash e:t\and t\leq\orecord {\!\!}} {\Gamma \vdash e:t\and t\leq\orecord {\!\!}} ... @@ -100,7 +100,7 @@ Expressions are then typed by the following rules (already in algorithmic form). ... @@ -100,7 +100,7 @@ Expressions are then typed by the following rules (already in algorithmic form). \Infer[Proj] \Infer[Proj] {\Gamma \vdash e:t\and t\leq\orecord{\ell = \Any}} {\Gamma \vdash e:t\and t\leq\orecord{\ell = \Any}} {\Gamma \vdash e.\ell:\proj \ell {t}} {\Gamma \vdash e.\ell:\proj \ell {t}} {e.\ell\not\in\dom\Gamma}\vspace{-2mm} {e.\ell\not\in\dom\Gamma}\svvspace{-2mm} \end{mathpar} \end{mathpar} To extend occurrence typing to records we add the following values to paths: $\varpi\in\{\ldots,a_\ell,u_\ell^1,u_\ell^2,r_\ell\}^*$, with To extend occurrence typing to records we add the following values to paths: $\varpi\in\{\ldots,a_\ell,u_\ell^1,u_\ell^2,r_\ell\}^*$, with $$e.\ell\downarrow a_\ell.\varpi =\occ{e}\varpi$$, $$e.\ell\downarrow a_\ell.\varpi =\occ{e}\varpi$$, ... @@ -108,7 +108,7 @@ To extend occurrence typing to records we add the following values to paths: $\v ... @@ -108,7 +108,7 @@ To extend occurrence typing to records we add the following values to paths:$\v $$\recupd{e_1}\ell{e_2}\downarrow u_\ell^i.\varpi = \occ{e_i}\varpi$$ $$\recupd{e_1}\ell{e_2}\downarrow u_\ell^i.\varpi = \occ{e_i}\varpi$$ and add the following rules for the new paths: and add the following rules for the new paths: \begin{mathpar}\vspace{-8.7mm}\\ \begin{mathpar}\svvspace{-8.7mm}\\ \Infer[PSel] \Infer[PSel] { \pvdash \Gamma e t \varpi:t'} { \pvdash \Gamma e t \varpi:t'} { \pvdash \Gamma e t {\varpi.a_\ell}:\orecord {\ell:t'} } { \pvdash \Gamma e t {\varpi.a_\ell}:\orecord {\ell:t'} } ... @@ -118,7 +118,7 @@ and add the following rules for the new paths: ... @@ -118,7 +118,7 @@ and add the following rules for the new paths: { \pvdash \Gamma e t \varpi:t'} { \pvdash \Gamma e t \varpi:t'} { \pvdash \Gamma e t \varpi.r_\ell: (\recdel {t'} \ell) + \crecord{\ell \eqq \Any}} { \pvdash \Gamma e t \varpi.r_\ell: (\recdel {t'} \ell) + \crecord{\ell \eqq \Any}} { } { } \vspace{-3mm}\\ \svvspace{-3mm}\\ \Infer[PUpd1] \Infer[PUpd1] { \pvdash \Gamma e t \varpi:t'} { \pvdash \Gamma e t \varpi:t'} { \pvdash \Gamma e t \varpi.u_\ell^1: (\recdel {t'} \ell) + \crecord{\ell \eqq \Any}} { \pvdash \Gamma e t \varpi.u_\ell^1: (\recdel {t'} \ell) + \crecord{\ell \eqq \Any}} ... ...
 ... @@ -15,7 +15,7 @@ In a sense, occurrence typing is a ... @@ -15,7 +15,7 @@ In a sense, occurrence typing is a discipline designed to push forward the frontiers beyond which gradual discipline designed to push forward the frontiers beyond which gradual typing is needed, thus reducing the amount of runtime checks needed. For typing is needed, thus reducing the amount of runtime checks needed. For instance, the JavaScript code of~\eqref{foo} and~\eqref{foo2} in the introduction can also be instance, the JavaScript code of~\eqref{foo} and~\eqref{foo2} in the introduction can also be typed by using gradual typing:%\vspace{-.2mm} typed by using gradual typing:%\svvspace{-.2mm} \begin{alltt}\color{darkblue}\morecompact \begin{alltt}\color{darkblue}\morecompact function foo(x\textcolor{darkred}{ : \pmb{\dyn}}) \{ function foo(x\textcolor{darkred}{ : \pmb{\dyn}}) \{ return (typeof(x) === "number")? x+1 : x.trim(); \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo3} return (typeof(x) === "number")? x+1 : x.trim(); \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo3} ... @@ -105,7 +105,7 @@ other words, if a function expects an argument of type $\tau$ but can be ... @@ -105,7 +105,7 @@ other words, if a function expects an argument of type $\tau$ but can be typed under the hypothesis that the argument has type $\tauUp$, then no casts typed under the hypothesis that the argument has type $\tauUp$, then no casts are needed, since every cast that succeeds will be a subtype of are needed, since every cast that succeeds will be a subtype of $\tauUp$. Taking advantage of this property, we modify the rule for $\tauUp$. Taking advantage of this property, we modify the rule for functions as: \vspace{-2mm} functions as: \svvspace{-2mm} % % %\begin{mathpar} %\begin{mathpar} % \Infer[Abs] % \Infer[Abs] ... @@ -128,7 +128,7 @@ functions as: \vspace{-2mm} ... @@ -128,7 +128,7 @@ functions as: \vspace{-2mm} } } { { \Gamma\vdash\lambda x:\sigma'.e:\textstyle\bigwedge_{(\sigma,\tau) \in T}\sigma\to \tau \Gamma\vdash\lambda x:\sigma'.e:\textstyle\bigwedge_{(\sigma,\tau) \in T}\sigma\to \tau }\vspace{-2mm} }\svvspace{-2mm} \] \] The main idea behind this rule is the same as before: we first collect all the The main idea behind this rule is the same as before: we first collect all the information we can into $\psi$ by analyzing the body of the function. We then information we can into $\psi$ by analyzing the body of the function. We then ... @@ -149,7 +149,7 @@ $\code{number} \land \dyn\simeq \code{number}$ is ... @@ -149,7 +149,7 @@ $\code{number} \land \dyn\simeq \code{number}$ is not an option, since it would force us to choose between having not an option, since it would force us to choose between having the gradual guarantee or having, say, the gradual guarantee or having, say, $\code{number} \land \code{string}$ be more precise than $\code{number} \land \code{string}$ be more precise than $\code{number} \land \dyn$.\vspace{-2mm}} $\code{number} \land \dyn$.\svvspace{-2mm}} Hence the need for the second part of Hence the need for the second part of Rule~\textsc{[AbsInf+]}: the maximal interpretation of $\code{number} \land \dyn$ Rule~\textsc{[AbsInf+]}: the maximal interpretation of $\code{number} \land \dyn$ is $\code{number}$, and it is clear that, if $\code x$ is given type \code{number}, is $\code{number}$, and it is clear that, if $\code x$ is given type \code{number}, ... ...
 ... @@ -238,7 +238,8 @@ that $e_1e_2$ has type $t$ succeeds or fails. Let us start with refining the typ ... @@ -238,7 +238,8 @@ that $e_1e_2$ has type $t$ succeeds or fails. Let us start with refining the typ which the test succeeds. Intuitively, we want to remove from $t_2$ all which the test succeeds. Intuitively, we want to remove from $t_2$ all the values for which the application will surely return a result not the values for which the application will surely return a result not in $t$, thus making the test fail. Consider $t_1$ and let $s$ be the in $t$, thus making the test fail. Consider $t_1$ and let $s$ be the largest subtype of $\dom{t_1}$ such that\vspace{-1.29mm} largest subtype of $\dom{t_1}$ such that% \svvspace{-1.29mm} \begin{equation}\label{eq1} \begin{equation}\label{eq1} t_1\circ s\leq \neg t t_1\circ s\leq \neg t \end{equation} \end{equation} ... @@ -293,9 +294,10 @@ Ergo $t_1\setminus (t_2^+\to ... @@ -293,9 +294,10 @@ Ergo$t_1\setminus (t_2^+\to Let us see all this on our example \eqref{exptre}, in particular, by showing how this technique deduces that the type of $x_1$ in the positive branch is (a subtype of) $\Int{\vee}\String\to\Int$. Let us see all this on our example \eqref{exptre}, in particular, by showing how this technique deduces that the type of $x_1$ in the positive branch is (a subtype of) $\Int{\vee}\String\to\Int$. Take the static type of $x_1$, that is $(\Int{\vee}\String\to\Int)\vee(\Bool{\vee}\String\to\Bool)$ and intersect it with Take the static type of $x_1$, that is $(\Int{\vee}\String\to\Int)\vee(\Bool{\vee}\String\to\Bool)$ and intersect it with $(t_2^+\to \neg t)$, that is, $\String\to\neg\Int$. Since intersection distributes over unions we $(t_2^+\to \neg t)$, that is, $\String\to\neg\Int$. Since intersection distributes over unions we obtain\vspace{-1mm} obtain \svvspace{-1mm} % % $((\Int{\vee}\String{\to}\Int)\wedge\neg(\String{\to}\neg\Int))\vee((\Bool{\vee}\String{\to}\Bool)\wedge\neg(\String{\to}\neg\Int))\vspace{-1mm}$ $((\Int{\vee}\String{\to}\Int)\wedge\neg(\String{\to}\neg\Int))\vee((\Bool{\vee}\String{\to}\Bool)\wedge\neg(\String{\to}\neg\Int))\svvspace{-1mm}$ % % and since and since $(\Bool{\vee}\String{\to}\Bool)\wedge\neg(\String{\to}\neg\Int)$ is empty $(\Bool{\vee}\String{\to}\Bool)\wedge\neg(\String{\to}\neg\Int)$ is empty ... @@ -314,9 +316,18 @@ This is essentially what we formalize in Section~\ref{sec:language}, in the type ... @@ -314,9 +316,18 @@ This is essentially what we formalize in Section~\ref{sec:language}, in the type In the previous section we outlined the main ideas of our approach to occurrence typing. However, devil is in the details. So the formalization we give in Section~\ref{sec:language} is not so smooth as we just outlined: we must introduce several auxiliary definitions to handle some corner cases. This section presents by tiny examples the main technical difficulties we had to overcome and the definitions we introduced to handle them. As such it provides a kind of road-map for the technicalities of Section~\ref{sec:language}. In the previous section we outlined the main ideas of our approach to occurrence typing. However, devil is in the details. So the formalization we give in Section~\ref{sec:language} is not so smooth as we just outlined: we must introduce several auxiliary definitions to handle some corner cases. This section presents by tiny examples the main technical difficulties we had to overcome and the definitions we introduced to handle them. As such it provides a kind of road-map for the technicalities of Section~\ref{sec:language}. \paragraph{Typing occurrences} As it should be clear by now, not only variables but also generic expressions are given different types in the then'' and else'' branches of type tests. For instance, in \eqref{two} the expression $x_1x_2$ has type \Int{} in the positive branch and type \Bool{} in the negative one. In this specific case it is possible to deduce these typings from the refined types of the variables (in particular, thanks to the fact that $x_2$ has type \Int{} the positive branch and \Bool{} in the negative one), but this is not possible in general. For instance, consider $x_1:\Int\to(\Int\vee\Bool)$, $x_2:\Int$, and the expression\vspace{-1mm} \paragraph{Typing occurrences} As it should be clear by now, not only variables but also generic expressions are given different types in the then'' and else'' branches of type tests. For instance, in \eqref{two} the expression $x_1x_2$ has type \Int{} in the positive branch and type \Bool{} in the negative one. In this specific case it is possible to deduce these typings from the refined types of the variables (in particular, thanks to the fact that $x_2$ has type \Int{} the positive branch and \Bool{} in the negative one), but this is not possible in general. For instance, consider $x_1:\Int\to(\Int\vee\Bool)$, $x_2:\Int$, and the expression \svvspace{-1mm} \begin{equation}\label{twobis} \begin{equation}\label{twobis} \ifty{x_1x_2}{\Int}{...x_1x_2...}{...x_1x_2...}\vspace{-1mm} \ifty{x_1x_2}{\Int}{...x_1x_2...}{...x_1x_2...}\svvspace{-1mm} \end{equation} \end{equation} It is not possible to specialize the type of the variables in the It is not possible to specialize the type of the variables in the branches. Nevertheless, we want to be able to deduce that $x_1x_2$ has branches. Nevertheless, we want to be able to deduce that $x_1x_2$ has ... @@ -347,9 +358,9 @@ satisfies progress and type preservation. The latter property is ... @@ -347,9 +358,9 @@ satisfies progress and type preservation. The latter property is challenging because, as explained just above, our type challenging because, as explained just above, our type assumptions are not only about variables but also about assumptions are not only about variables but also about expressions. Two corner cases are particularly difficult. The first is expressions. Two corner cases are particularly difficult. The first is shown by the following example\vspace{-.9mm} shown by the following example\svvspace{-.9mm} \begin{equation}\label{bistwo} \begin{equation}\label{bistwo} \ifty{e(42)}{\Bool}{e}{...}\vspace{-.9mm} \ifty{e(42)}{\Bool}{e}{...} \svvspace{-.9mm} \end{equation} \end{equation} If $e$ is an expression of type $\Int\to t$, then, as discussed before, If $e$ is an expression of type $\Int\to t$, then, as discussed before, the positive branch will have type $(\Int\to t)\setminus(\Int\to\neg the positive branch will have type$(\Int\to t)\setminus(\Int\to\neg ... @@ -396,9 +407,9 @@ an approximation thereof. ... @@ -396,9 +407,9 @@ an approximation thereof. Finally, a nested check may help refining Finally, a nested check may help refining the type assumptions on some outer expressions. For instance, when typing the type assumptions on some outer expressions. For instance, when typing the positive branch $e$ of\vspace{-.9mm} the positive branch $e$ of\svvspace{-.9mm} \begin{equation}\label{pair} \begin{equation}\label{pair} \ifty{(x,y)}{(\pair{(\Int\vee\Bool)}\Int)}{e}{...}\vspace{-.9mm} \ifty{(x,y)}{(\pair{(\Int\vee\Bool)}\Int)}{e}{...}\svvspace{-.9mm} \end{equation} \end{equation} we can assume that the expression $(x,y)$ is of type we can assume that the expression $(x,y)$ is of type $\pair{(\Int\vee\Bool)}\Int$ and put it in the type environment. But $\pair{(\Int\vee\Bool)}\Int$ and put it in the type environment. But ... ...
 ... @@ -7,7 +7,7 @@ In this section we formalize the ideas we outlined in the introduction. We start ... @@ -7,7 +7,7 @@ In this section we formalize the ideas we outlined in the introduction. We start \subsection{Types} \subsection{Types} \begin{definition}[Types]\label{def:types} \begin{definition}[Types]\label{def:types} %\iflongversion%%%%%%% %\iflongversion%%%%%%% The set of types \types{} is formed by the terms $t$ coinductively produced by the grammar:\vspace{-1.45mm} The set of types \types{} is formed by the terms $t$ coinductively produced by the grammar:\svvspace{-1.45mm} $\[ \begin{array}{lrcl} \begin{array}{lrcl} \textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty \textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty ... @@ -17,10 +17,10 @@ and that satisfy the following conditions ... @@ -17,10 +17,10 @@ and that satisfy the following conditions \begin{itemize}[nosep] \begin{itemize}[nosep] \item (regularity) every term has a finite number of different sub-terms; \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 \item (contractivity) every infinite branch of a term contains an infinite number of occurrences of the arrow or product type constructors.\vspace{-1mm} arrow or product type constructors.\svvspace{-1mm} \end{itemize} \end{itemize} \iffalse%%%%%%%%%%%%%%%%%%%%%%%%%% \iffalse%%%%%%%%%%%%%%%%%%%%%%%%%% A type t\in\types{} is a term coinductively produced by the grammar:\vspace{-1.45mm} A type t\in\types{} is a term coinductively produced by the grammar:\svvspace{-1.45mm} \[ \[ \begin{array}{lrcl} \begin{array}{lrcl} \textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty \textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty ... @@ -28,7 +28,7 @@ A type t\in\types{} is a term coinductively produced by the grammar:\vspace{-1 ... @@ -28,7 +28,7 @@ A type t\in\types{} is a term coinductively produced by the grammar:\vspace{-1$ \] that satisfies the following conditions: $(1)$\emph{Regularity}: the that satisfies the following conditions: $(1)$\emph{Regularity}: the term has a finite number of different sub-terms; $(2)$ \emph{Contractivity}: every infinite branch of the term contains an infinite number of occurrences of the term has a finite number of different sub-terms; $(2)$ \emph{Contractivity}: every infinite branch of the term contains an infinite number of occurrences of the arrow or product type constructors.\vspace{-1mm} arrow or product type constructors.\svvspace{-1mm} \fi%%%%%%%%%%%%%%%%%%% \fi%%%%%%%%%%%%%%%%%%% \end{definition} \end{definition} We use the following abbreviations: $We use the following abbreviations:$ ... @@ -79,7 +79,7 @@ union of the values of the two types). We use $\simeq$ to denote the ... @@ -79,7 +79,7 @@ union of the values of the two types). We use $\simeq$ to denote the 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. 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. \subsection{Syntax}\label{sec:syntax} \subsection{Syntax}\label{sec:syntax} The expressions $e$ and values $v$ of our language are inductively generated by the following grammars:\vspace{-1mm} The expressions $e$ and values $v$ of our language are inductively generated by the following grammars:\svvspace{-1mm} \begin{equation}\label{expressions} \begin{equation}\label{expressions} \begin{array}{lrclr} \begin{array}{lrclr} \textbf{Expr} &e &::=& c\alt x\alt ee\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt \pi_j e\alt(e,e)\alt\tcase{e}{t}{e}{e}\\[.3mm] \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] ... @@ -110,7 +110,7 @@ values. We write $v\in t$ if the most specific type of $v$ is a subtype of $t$ ( ... @@ -110,7 +110,7 @@ values. We write $v\in t$ if the most specific type of $v$ is a subtype of $t$ ( \subsection{Dynamic semantics}\label{sec:opsem} \subsection{Dynamic semantics}\label{sec:opsem} 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} 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:\svvspace{-1.2mm} \[ \[ \begin{array}{rcll} \begin{array}{rcll} (\lambda^{\wedge_{i\in I}s_i\to t_i} x.e)\,v &\reduces& e\subst x v\\[-.4mm] (\lambda^{\wedge_{i\in I}s_i\to t_i} x.e)\,v &\reduces& e\subst x v\\[-.4mm] ... @@ -137,7 +137,7 @@ standard, for what concerns the type system we will have to introduce several ... @@ -137,7 +137,7 @@ standard, for what concerns the type system we will have to introduce several unconventional features that we anticipated in unconventional features that we anticipated in Section~\ref{sec:challenges} and are at the core of our work. Let Section~\ref{sec:challenges} and are at the core of our work. Let us start with the standard part, that is the typing of the functional us start with the standard part, that is the typing of the functional core and the use of subtyping, given by the following typing rules:\vspace{-1mm} core and the use of subtyping, given by the following typing rules:\svvspace{-1mm} \begin{mathpar} \begin{mathpar} \Infer[Const] \Infer[Const] { } { } ... @@ -182,7 +182,7 @@ core and the use of subtyping, given by the following typing rules:\vspace{-1mm} ... @@ -182,7 +182,7 @@ core and the use of subtyping, given by the following typing rules:\vspace{-1mm} { \Gamma \vdash e:t\\t\leq t' } { \Gamma \vdash e:t\\t\leq t' } { \Gamma \vdash e: t' } { \Gamma \vdash e: t' } { } { } \qquad\vspace{-3mm} \qquad\svvspace{-3mm} \end{mathpar} \end{mathpar} 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. 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. ... @@ -190,7 +190,7 @@ The first unconventional aspect is that, as explained in ... @@ -190,7 +190,7 @@ The first unconventional aspect is that, as explained in Section~\ref{sec:challenges}, our type assumptions are about Section~\ref{sec:challenges}, our type assumptions are about expressions. Therefore, in our rules the type environments, ranged over expressions. Therefore, in our rules the type environments, ranged over by $\Gamma$, map \emph{expressions}---rather than just variables---into by $\Gamma$, map \emph{expressions}---rather than just variables---into types. This explains why the classic typing rule for variables is replaced by a more general \Rule{Env} rule defined below:\vspace{-1mm} types. This explains why the classic typing rule for variables is replaced by a more general \Rule{Env} rule defined below:\svvspace{-1mm} \begin{mathpar} \begin{mathpar} \Infer[Env] \Infer[Env] { } { } ... @@ -200,7 +200,7 @@ types. This explains why the classic typing rule for variables is replaced by a ... @@ -200,7 +200,7 @@ types. This explains why the classic typing rule for variables is replaced by a \Infer[Inter] \Infer[Inter] { \Gamma \vdash e:t_1\\\Gamma \vdash e:t_2 } { \Gamma \vdash e:t_1\\\Gamma \vdash e:t_2 } { \Gamma \vdash e: t_1 \wedge t_2 } { \Gamma \vdash e: t_1 \wedge t_2 } { }\vspace{-3mm} { }\svvspace{-3mm} \end{mathpar} \end{mathpar}