Commit 899b276b authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

moved [OverApp] Rule

parent 31db3325
......@@ -84,7 +84,7 @@ $(\lnot(\Int \lor \Char) \to (\Int \to 2) \land
(\lnot\Int \to 3) \land$\newline
\hspace*{0.2cm}$(\Bool \to 3) \land(\lnot(\Bool \lor \Int) \to 3)
\land (\lnot\Bool \to 2
\lor 3))$~~$\land \ldots$ (two other redundant cases ommitted)
\lor 3))$~~$\land \ldots$ (two other redundant cases omitted)
% \newline
% $(\lnot\Char \to (\Int \to 2) \land (\lnot\Int \to 1 \lor 3) \land (\Bool \to 1 \lor 3) \land$\newline
% \hspace*{1cm}$(\lnot(\Bool \lor \Int) \to 3) \land
......
......@@ -26,7 +26,7 @@
\submissionfalse
\newif\iflongversion
\longversiontrue
%\longversionfalse
\longversionfalse
\usepackage{setup}
\fancypagestyle{emptyfooter}{
......
......@@ -11,7 +11,7 @@ of our type-checking implementation in Table~\ref{tab:implem} by
listing some examples none of which can be typed by current
systems (even though some system such as Flow and TypeScript
can type some of them by adding explicit type annotation, the code 6,
7, 9, and 10 and the \code{and\_} and \code{xor\_} functions at the end of this
7, 9, and 10 in Table~\ref{tab:implem} and, even more, the \code{and\_} and \code{xor\_} functions at the end of this
section are out of reach of current systems, even when using the right
explicit annotations). These examples and others can be tested in the
online toplevel available at
......@@ -31,7 +31,7 @@ function under this assumption, but doing so collects that the type of
$\texttt{x}$ is specialized to \Int{} in the ``then'' case and to \Bool{}
in the ``else'' case. The function is thus type-checked twice more
under each hypothesis for \texttt{x}, yielding the precise type
$(\Int\to\Int)\land(\Bool\to\Bool)$. Note that w.r.t.\ rule \Rule{AbsInf+} of Section~\ref{sec:refining}, we improved the output of the computed
$(\Int\to\Int)\land(\Bool\to\Bool)$. Note that w.r.t.\ rule \Rule{AbsInf+} of Section~\ref{sec:refining}, our implementation improved the output of the computed
type. Indeed using rule~[{\sc AbsInf}+] we would obtain the
type
$(\Int\to\Int)\land(\Bool\to\Bool)\land(\Bool\vee\Int\to\Bool\vee\Int)$
......@@ -117,46 +117,28 @@ 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 another enhancement that allows us
to further improve the precision of the inferred type.
Code~9 shows the usefulness of the rule \Rule{OverApp}.
Consider the definition of the \texttt{xor\_} operator (Code~9).
Here the rule~[{\sc AbsInf}+] is not sufficient to precisely type the
function, and using only this rule would yield a type
$\Any\to\Any\to\Bool$. Let us follow the behavior of the
$\Any\to\Any\to\Bool$.
\iflongversion
Let us follow the behavior of the
``$\worra{}{}$'' operator. Here the whole \texttt{and\_} is requested
to have type \True, which implies that \texttt{or\_ x y} must have
type \True. This can always happen, whether \texttt{x} is \True{} or
not (but then depends on the type of \texttt{y}). The ``$\worra{}{}$''
operator correctly computes that the type for \texttt{x} in the
``\texttt{then}'' branch is $\True\vee\lnot\True\lor\True\simeq\Any$,
and a similar reasoning holds for \texttt{y}. To solve this problem,
we can first remark that even though type cases in the body of a
function are tipping points that may change the type of the result
of the function, they are not the only ones: applications of overloaded functions play exactly the same role. We
therefore extend deduction system for $\Gamma \vdash e\triangleright\psi$ defined in Section~\ref{sec:refining} with
the following rule\\[1mm]
\centerline{\(
\Infer[OverApp]
{
\Gamma \vdash e : \textstyle\bigvee \bigwedge_{i \in I}t_i\to{}s_i\\
\Gamma \vdash x : t\\
\Gamma \vdash e\triangleright\psi_1\\
\Gamma \vdash x\triangleright\psi_2\\
}
{ \Gamma \vdash\textstyle
{e}{~x}\triangleright\psi_1\cup\psi_2\cup\bigcup_{i\in I}\{
x\mapsto t\wedge t_i\} }
{(t\wedge t_i\not\simeq\Empty)}
\)}\\
Whenever a function parameter is the argument of an
overloaded function, we record as possible types for this parameter
all the domains $t_i$ of the arrows that type the overloaded
function, restricted (via intersection) by the static type $t$ of the parameter and provided that the type is not empty ($t\wedge t_i\not\simeq\Empty$). In Code~9,
since \texttt{or\_} has type\\[.7mm]
\centerline{$(\True\to\Any\to\True)\land(\Any\to\True\to\True)\land
(\lnot\True\to\lnot\True\to\False)$}\\[.7mm]
then \True, \Any, and $\lnot\True$ become candidate types for
\texttt{x} and this allows us to deduce the precise type given in the table. Finally, thanks to this rule it is no longer necessary to use a type case to force refinement. As a consequence we can define the functions \texttt{and\_} and \texttt{xor\_} more naturally as:
and a similar reasoning holds for \texttt{y}.
\fi%%%%%%%%%%%%%%
However, since in Code~9 \texttt{or\_} has type
%\\[.7mm]\centerline{%
$(\True\to\Any\to\True)\land(\Any\to\True\to\True)\land
(\lnot\True\to\lnot\True\to\False)$
%}\\[.7mm]
then the rule \Rule{OverApp} applies and \True, \Any, and $\lnot\True$ become candidate types for
\texttt{x}, which allows us to deduce the precise type given in the table. Finally, thanks to rule \Rule{OverApp} it is not necessary to use a type case to force refinement. As a consequence we can define the functions \texttt{and\_} and \texttt{xor\_} more naturally as:
\begin{alltt}\color{darkblue}\morecompact
let and_ = fun (x : Any) -> fun (y : Any) -> not_ (or_ (not_ x) (not_ y))
let xor_ = fun (x : Any) -> fun (y : Any) -> and_ (or_ x y) (not_ (and_ x y))
......
......@@ -185,7 +185,29 @@ against the singleton types of all its inputs. But any finer partition
would return, in many cases, not a much better information, since most
partitions would collapse on the same return type: type-cases on the
parameter are the tipping points that are likely to make a difference, by returning different
types for different partitions thus yielding more precise typing. But they are not the only such tipping points: see rule \Rule{OverApp} in Section~\ref{sec:practical}.
types for different partitions thus yielding more precise typing.
Even though type cases in the body of a
function are tipping points that may change the type of the result
of the function, they are not the only ones: applications of overloaded functions play exactly the same role. We
therefore add to our deduction system a last further rule:\\[1mm]
\centerline{\(
\Infer[OverApp]
{
\Gamma \vdash e : \textstyle\bigvee \bigwedge_{i \in I}t_i\to{}s_i\\
\Gamma \vdash x : t\\
\Gamma \vdash e\triangleright\psi_1\\
\Gamma \vdash x\triangleright\psi_2\\
}
{ \Gamma \vdash\textstyle
{e}{~x}\triangleright\psi_1\cup\psi_2\cup\bigcup_{i\in I}\{
x\mapsto t\wedge t_i\} }
{(t\wedge t_i\not\simeq\Empty)}
\)}\\
Whenever a function parameter is the argument of an
overloaded function, we record as possible types for this parameter
all the domains $t_i$ of the arrows that type the overloaded
function, restricted (via intersection) by the static type $t$ of the parameter and provided that the type is not empty ($t\wedge t_i\not\simeq\Empty$). We show the full power of this rule on some practical examples in Section~\ref{sec:practical}.
\ignore{\color{darkred} RANDOM THOUGHTS:
A delicate point is the definition of the union
......
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