Commit 082e483e by Giuseppe Castagna

 ... @@ -20,7 +20,7 @@ following two type constructors:\$1.4mm] ... @@ -20,7 +20,7 @@ following two type constructors:\\[1.4mm] %% \textbf{Types} & t & ::= & \record{\ell_1=t \ldots \ell_n=t}{t}\alt \Undef %% \textbf{Types} & t & ::= & \record{\ell_1=t \ldots \ell_n=t}{t}\alt \Undef %% \end{array} %% \end{array} %%$ %% \] where $\ell$ ranges over an infinite set of labels $\Labels$, $\Undef$ where $\ell$ ranges over an infinite set of labels $\Labels$ and $\Undef$ is a special singleton type whose only value is the constant is a special singleton type whose only value is the constant $\undefcst$ which is a constant not in $\Any$. The type $\undefcst$ which is a constant not in $\Any$. The type $\record{\ell_1=t_1 \ldots \ell_n=t_n}{t}$ is a \emph{quasi-constant $\record{\ell_1=t_1 \ldots \ell_n=t_n}{t}$ is a \emph{quasi-constant ... @@ -34,12 +34,12 @@ following syntactic sugar and that form the \emph{record types} of our language\ ... @@ -34,12 +34,12 @@ following syntactic sugar and that form the \emph{record types} of our language\ \item $\crecord{\ell_1=t_1, \ldots, \ell_n=t_n}$ for $\record{\ell_1=t_1 \ldots \ell_n=t_n}{\Undef}$ (closed records). \item $\crecord{\ell_1=t_1, \ldots, \ell_n=t_n}$ for $\record{\ell_1=t_1 \ldots \ell_n=t_n}{\Undef}$ (closed records). \item $\orecord{\ell_1=t_1, \ldots, \ell_n=t_n}$ for $\record{\ell_1=t_1 \ldots \ell_n=t_n}{\Any \vee \Undef}$ (open records). \item $\orecord{\ell_1=t_1, \ldots, \ell_n=t_n}$ for $\record{\ell_1=t_1 \ldots \ell_n=t_n}{\Any \vee \Undef}$ (open records). \end{itemize} \end{itemize} plus the notation $\mathtt{\ell \eqq t}$ to denote optional fields, plus the notation $\mathtt{\ell \eqq} t$ to denote optional fields, which corresponds to using in the quasi-constant function notation the which corresponds to using in the quasi-constant function notation the field $\ell = t \vee \Undef$. field $\ell = t \vee \Undef$. For what concern expressions, we adapt CDuce records to our analysis. In particular records are built starting from the empty record expressions \erecord{} and by adding, updating, or removing fields:\vspace{-1mm} For what concerns expressions, we adapt CDuce records to our analysis. In particular records are built starting from the empty record expression \erecord{} and by adding, updating, or removing fields:\vspace{-1mm} \[ \[ \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 ... @@ -62,7 +62,7 @@ To define record type subtyping and record expression type inference we need the ... @@ -62,7 +62,7 @@ To define record type subtyping and record expression type inference we need the \proj {\ell'} u \geq \proj {\ell'} t &\text{ otherwise} \proj {\ell'} u \geq \proj {\ell'} t &\text{ otherwise} \end{array}\right\}\right\} \end{array}\right\}\right\} \end{eqnarray} \end{eqnarray} Then two record types $t_1$ and $t_2$ are in subtyping relation, $t_1 \leq t_2$, if and only if $\forall \ell \in \Labels. \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). Expressions are then typed by the following rules (already in algorithmic form). \begin{mathpar} \begin{mathpar} ... @@ -86,7 +86,7 @@ Expressions are then typed by the following rules (already in algorithmic form). ... @@ -86,7 +86,7 @@ Expressions are then typed by the following rules (already in algorithmic form). {\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}\vspace{-2mm} \end{mathpar} \end{mathpar} To extend occurrence typing to records we add paths 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$$, $$\recdel e \ell\downarrow r_\ell.\varpi = \occ{e}\varpi$$, and $$\recdel e \ell\downarrow r_\ell.\varpi = \occ{e}\varpi$$, and $$\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$$ ... ...
 ... @@ -20,7 +20,7 @@ in its body, and use this information to partition the domain of the function ... @@ -20,7 +20,7 @@ in its body, and use this information to partition the domain of the function and to re-type its body. Consider a more involved example and to re-type its body. Consider a more involved example \begin{alltt}\color{darkblue}\morecompact \begin{alltt}\color{darkblue}\morecompact function (x \textcolor{darkred}{: $$\tau$$}) \{ function (x \textcolor{darkred}{: $$\tau$$}) \{ (x $$\in$$ Real) ? \{ (x $$\in$$ Int) ? succ x : sqrt x \} : \{ $$\neg$$x \} (x $$\in$$ Real) ? \{ (x $$\in$$ Int) ? succ x : sqrt x \} : \{ $$\neg$$x \} \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foorefine} \} \} \end{alltt} \end{alltt} When $\tau$ is \code{Real|Bool} (we assume that \code{Int} is a When $\tau$ is \code{Real|Bool} (we assume that \code{Int} is a ... @@ -139,10 +139,10 @@ domain of $\Gamma$ restricted to variables. ... @@ -139,10 +139,10 @@ domain of $\Gamma$ restricted to variables. Simply put, this rule first collects all possible types that are deduced Simply put, this rule first collects all possible types that are deduced for a variable $x$ during typing and then uses them to re-type the body for a variable $x$ during typing and then uses them to re-type the body of the lambda under this new refined hypothesis for the type of of the lambda under this new refined hypothesis for the type of $x$. The re-typing ensures that that the type soundness property $x$. The re-typing ensures that the type safety property carries over to this new rule. carries over to this new rule. This system is enough to type our case study for the case $\tau$ This system is enough to type our case study \eqref{foorefine} for the case $\tau$ defined as \code{Real|Bool}. Indeed the analysis of the body yields defined as \code{Real|Bool}. Indeed the analysis of the body yields $\psi(x)=\{\Int,\Real\setminus\Int\}$ for the branch \code{(x\,$\in$\,Int) ? succ\,x : sqrt\,x} and, since $\psi(x)=\{\Int,\Real\setminus\Int\}$ for the branch \code{(x\,$\in$\,Int) ? succ\,x : sqrt\,x} and, since \code{$(\Bool\vee\Real)\setminus\Real = \Bool$}, yields \code{$(\Bool\vee\Real)\setminus\Real = \Bool$}, yields ... @@ -152,7 +152,7 @@ will be checked for the input types $\Int$, $\Real\setminus\Int$, and ... @@ -152,7 +152,7 @@ will be checked for the input types $\Int$, $\Real\setminus\Int$, and It is not too difficult to generalize this rule when the lambda is It is not too difficult to generalize this rule when the lambda is typed by an intersection type. Indeed, even if the programmer has typed by an intersection type. Indeed, even if the programmer has specified a particular intersection type for the function we may want specified a particular intersection type for the function, we may want to refine each of its arrows. This is exactly what the following rule to refine each of its arrows. This is exactly what the following rule does:\vspace{-1mm} does:\vspace{-1mm} \begin{mathpar} \begin{mathpar} ... ...