Commit 455324fe authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

spaces

parent 4e1f5e68
......@@ -111,7 +111,7 @@ where $x_i$'s denote variables, $t$ is some type, and $e_i$'s are generic expres
Depending the actual $t$ and the static types of $x_1$ and $x_2$, we
can make type assumptions for $x_1$, for $x_2$, \emph{and} for the application $x_1x_2$
when typing $e_1$ that are different from those we can make when typing
$e_2$. For instance, suppose $x_1$ is bound to the function \code{foo} defined in \eqref{foo2}. Thus $x_1$ has type $(\Int\to\Int)\wedge(\String\to\String)$ (we used the syntax of the types of Section~\ref{sec:language} where unions and intersections are denoted by $\vee$ and $\wedge$).
$e_2$. For instance, suppose $x_1$ is bound to the function \code{foo} defined in \eqref{foo2}. Thus $x_1$ has type $(\Int\to\Int)\wedge(\String\to\String)$ (we used the syntax of the types of Section~\ref{sec:language} where unions and intersections are denoted by $\vee$ and $\wedge$ and have priority over $\to$ and $\times$, but not over $\neg$).
Then it is not hard to see that the expression\footnote{This and most of the following expressions are just given for the sake of example. Determining the type of expressions other than variables is interesting for constructors but less so for destructors such as applications, projections, and selections: any reasonable programmer would not repeat the same application twice, (s)he would store its result in a variable. This becomes meaningful when we introduce constructor such as pairs, as we do for instance in the expression in~\eqref{pair}.}
%
\begin{equation}\label{mezzo}
......@@ -281,7 +281,7 @@ of all functions that when applied to an argument of type $t$ they
either diverge or return a value in $s$. As such the interpretation of $t\to s$ contains
all the functions that diverge (at least) on $t$. Therefore removing $t\to s$ from a type $u$ removes from $u$ not only all the functions that when applied to a $t$ argument return a result in $s$, but also all the functions that diverge on $t$.
Ergo $t_1\setminus (t_2^+\to
\neg(t_1\!\circ t_2^+)))$ removes, among others, all functions in $t_1$ that diverge on $t_2^+$.
\neg(t_1\!\circ t_2^+))$ removes, among others, all functions in $t_1$ that diverge on $t_2^+$.
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
$(t_2^+\to \neg(t_1\!\circ t_2^+))$, that is, $\String\to\neg\Int$. Since intersection distributes over unions we
obtain
......@@ -305,9 +305,9 @@ 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}.
\paragraph{Typing occurrences} As it should be clear by now, not only variables but also generic expression 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
\paragraph{Typing occurrences} As it should be clear by now, not only variables but also generic expression 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{-.9mm}
\begin{equation}\label{twobis}
\ifty{x_1x_2}{\Int}{...x_1x_2...}{...x_1x_2...}
\ifty{x_1x_2}{\Int}{...x_1x_2...}{...x_1x_2...}\vspace{-.9mm}
\end{equation}
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
......@@ -333,14 +333,14 @@ for the multiple occurrences of it.
\paragraph{Type preservation} We want our type system to be sound in the sense of~\citet{Wright1994}, that is, it
\paragraph{Type preservation} We want our type system to be sound in the sense of~\citet{Wright1994}, that is, that it
satisfies progress and type preservation. The latter property is
challenging because, as explained just above, our type
assumptions are not only about variables but also about
expressions. Two corner cases are particularly difficult. The first is
shown by the following example
shown by the following example\vspace{-.9mm}
\begin{equation}\label{bistwo}
\ifty{e(42)}{\Bool}{e}{...}
\ifty{e(42)}{\Bool}{e}{...}\vspace{-.9mm}
\end{equation}
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
......@@ -348,7 +348,10 @@ the positive branch will have type $(\Int\to t)\setminus(\Int\to\neg
will also be the type of the whole expression in \eqref{bistwo}. Now imagine
that the application $e(42)$ reduces to a Boolean value, then the whole
expression in \eqref{bistwo} reduces to $e$; but this has type
$\Int\to t$ which, in general, is \emph{not} a ssions by
$\Int\to t$ which, in general, is \emph{not} a subtype of $(\Int\to
t)\setminus(\Int\to\neg\Bool)$, and therefore type is not preserved by the reduction. To cope with this problem, in
Section~\ref{sec:language} we resort to \emph{type schemes} a
technique introduced by~\citet{Frisch2008} to type expressions by
sets of types, so that the expression in \eqref{bistwo} will have both the types at issue.
The second corner case is a modification of the example above
......@@ -385,9 +388,9 @@ an approximation thereof.
Finally, a nested check may help refining
the type assumptions on some outer expressions. For instance, when typing
the positive branch $e$ of
the positive branch $e$ of\vspace{-.9mm}
\begin{equation}\label{pair}
\ifty{(x,y)}{(\pair{(\Int\vee\Bool)}\Int)}{e}{...}
\ifty{(x,y)}{(\pair{(\Int\vee\Bool)}\Int)}{e}{...}\vspace{-.9mm}
\end{equation}
we can assume that the expression $(x,y)$ is of type
$\pair{(\Int\vee\Bool)}\Int$ and put it in the type environment. But
......
......@@ -293,7 +293,7 @@ root of the tree).
Let $e$ be an expression and $\varpi\in\{0,1,l,r,f,s\}^*$ a
\emph{path}; we denote $\occ e\varpi$ the occurrence of $e$ reached by
the path $\varpi$, that is (for $i=1,2$, and undefined otherwise)\vspace{-1mm}
the path $\varpi$, that is (for $i=1,2$, and undefined otherwise)\vspace{-.4mm}
%% \[
%% \begin{array}{l}
%% \begin{array}{r@{\downarrow}l@{\quad=\quad}l}
......@@ -311,7 +311,7 @@ the path $\varpi$, that is (for $i=1,2$, and undefined otherwise)\vspace{-1mm}
\begin{array}{r@{\downarrow}l@{\quad=\quad}lr@{\downarrow}l@{\quad=\quad}lr@{\downarrow}l@{\quad=\quad}l}
e&\epsilon & e & (e_0,e_1)& l.\varpi & \occ{e_0}\varpi &\pi_1 e& f.\varpi & \occ{e}\varpi\\
e_0e_1& i.\varpi & \occ{e_i}\varpi \quad\qquad& (e_0,e_1)& r.\varpi & \occ{e_1}\varpi \quad\qquad&
\pi_2 e& s.\varpi & \occ{e}\varpi\\[-1mm]
\pi_2 e& s.\varpi & \occ{e}\varpi\\[-.4mm]
\end{array}
\]
To ease our analysis we used different directions for each kind of
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment