Skip to content

GitLab

Commit 0c965e07 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

add refining.tex

parent 92584f9a
Hide whitespace changes
Inline Side-by-side
refining.tex 0 → 100644
View file @ 0c965e07
\newcommand{\negspace}{\vspace{-.5mm}}
As we explained in the introduction, both TypeScript and Flow deduce the type
\code{(number$\vee$string) $\to$ (number$\vee$string)} for the first definition of the function \code{foo} in~\eqref{foo}, and the more precise type\vspace{-3pt}
\begin{equation}\label{tyinter}
\code{(number$\to$number)$\,\wedge\,$(string$\to$string)}\vspace{-3pt}
\end{equation}
can be deduced by these languages only if they are instructed to do so: the
programmer has to explicitly annotate \code{foo} with the
type \eqref{tyinter}: we did it in \eqref{foo2} using Flow---the TypeScript annotation for it is much heavier. But this seems like overkill, since a simple
analysis of the body of \code{foo} in \eqref{foo} shows that its execution may have
two possible behaviors according to whether the parameter \code{x} has
type \code{number} or not (i.e., or \code{(number$\vee$string)$\setminus$number}, that is \code{string}), and this is
should be enough for the system to deduce the type \eqref{tyinter}
even in the absence the annotation given in \eqref{foo2}.
%
In this section we show how to do it by using the theory of occurrence
typing we developed in the first part of the paper. In particular, we
collect the different types that are assigned to the parameter of a function
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 in a pseudo
TypeScript that uses our notation
\begin{alltt}\color{darkblue}\morecompact
function (x \textcolor{darkred}{: \(\tau\)}) \{
return (x \(\in\) Real) ? ((x \(\in\) Int) ? x+1 : sqrt(x)) : !x; \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foorefine}
\}
\end{alltt}
where we assume that \code{Int} is a
subtype of \code{Real}. When $\tau$ is \code{Real$\vee$Bool} we want to deduce for this function the
type
\code{$(\Int\to\Int)\wedge(\Real\backslash\Int\to\Real)\wedge(\Bool\to\Bool)$}.
When $\tau$ is \Any,
then the function must be rejected (since it tries to type
\code{!x} under the assumption that \code x\ has type
\code{$\neg\Real$}). Notice that typing the function under the
hypothesis that $\tau$ is \Any,
allows us to capture user-defined discrimination as defined
by~\citet{THF10} since, for instance
\begin{alltt}\color{darkblue}\morecompact
let is_int x = (x\(\in\)Int)? true : false
in if is_int z then z+1 else 42
\end{alltt}
is well typed since the function \code{is\_int} is given type
$(\Int\to\True)\wedge(\neg\Int\to\False)$. We propose a more general
approach than the one by~\citet{THF10} since we allow the programmer to hint a particular type for the
argument and let the system deduce, if possible, an intersection type for the
function.
We start by considering the system where $\lambda$-abstractions are
typed by a single arrow and later generalize it to the case of
intersections of arrows. First, we define the auxiliary judgement
%\begin{displaymath}
\(
\Gamma \vdash e\triangleright\psi
\)
%\end{displaymath}
where $\Gamma$ is a typing environement, $e$ an expression and $\psi$
a mapping from variables to sets of types. Intuitively $\psi(x)$ denotes
the set that contains the types of all the occurrences of $x$ in $e$. This
judgement can be deduced by the following deduction system
that collects type information on the variables that are $\lambda$-abstracted
(i.e., those in the domain of $\Gamma$, since lambdas are our only
binders):\vspace{-1.5mm}
\begin{mathpar}
\Infer[Var]
{
}
{ \Gamma \vdash x \triangleright\{x \mapsto \{ \Gamma(x) \} \} }
{}
\hfill
\Infer[Const]
{
}
{ \Gamma \vdash c \triangleright \varnothing }
{}
\hfill
\Infer[Abs]
{\Gamma,x:s\vdash e\triangleright\psi}
{
\Gamma\vdash\lambda x:s.e\triangleright\psi\setminus\{x\}
}
{}
\vspace{-2.3mm}\\
\Infer[App]
{
\Gamma \vdash e_1\triangleright\psi_1 \\
\Gamma\vdash e_2\triangleright\psi_2
}
{ \Gamma \vdash {e_1}{e_2}\triangleright\psi_1\cup\psi_2 }
{}
\hfill
\Infer[Pair]
{\Gamma \vdash e_1\triangleright\psi_1 \and \Gamma \vdash e_2\triangleright\psi_2}
{\Gamma \vdash (e_1,e_2)\triangleright\psi_1\cup\psi_2}
{}
\hfill
\Infer[Proj]
{\Gamma \vdash e\triangleright\psi}
{\Gamma \vdash \pi_i e\triangleright\psi}
{}
\vspace{-2.3mm}\\
\Infer[Case]
{\Gamma\vdash e\triangleright\psi_\circ\\
\Gamma \evdash e t \Gamma_1\\ \Gamma_1\vdash e_1\triangleright\psi_1\\
\Gamma \evdash e {\neg t} \Gamma_2 \\ \Gamma_2\vdash e_2\triangleright\psi_2}
{\Gamma\vdash \ifty{e}{t}{e_1}{e_2}\triangleright\psi_\circ\cup\psi_1\cup\psi_2}
{}\vspace{-1.4mm}
\end{mathpar}
Where $\psi\setminus\{x\}$ is the function defined as $\psi$ but undefined on $x$ and $\psi_1\cup \psi_2$ denotes component-wise union%
\iflongversion%
, that is :
\begin{displaymath}
(\psi_1\cup \psi_2)(x) = \left\{\begin{array}{ll}
\psi_1 (x) & \text{if~} x\notin
\dom{\psi_2}\\
\psi_2 (x) & \text{if~} x\notin
\dom{\psi_1}\\
\psi_1(x)\cup\psi_2(x) & \text{otherwise}
\end{array}\right.
\end{displaymath}
\noindent
\else.~\fi
All that remains to do is to replace the rule [{\sc Abs}+] with the
following rule\vspace{-.8mm}
\begin{mathpar}
\Infer[AbsInf+]
{\Gamma,x:s\vdash e\triangleright\psi
\and
\Gamma,x:s\vdash e:t
\and
T = \{ (s,t) \} \cup \{ (u,w) ~|~
u\in\psi(x) \land \Gamma,x:u\vdash e:w \}}
{
\Gamma\vdash\lambda x{:}s.e:\textstyle\bigwedge_{(u,w) \in T}u\to w
}
{}\vspace{-2.5mm}
\end{mathpar}
Note the invariant that the domain of
$\psi$ is always conatined in the
domain of $\Gamma$ restricted to variables.
Simply put, this rule first collects all possible types that are deduced
for a variable $x$ during the typing of the body of the $\lambda$ and then uses them to re-type the body
under this new refined hypothesis for the type of
$x$. The re-typing ensures that the type safety property
carries over to this new rule.
This system is enough to type our case study \eqref{foorefine} for the case $\tau$
defined as \code{Real$\vee$Bool}. Indeed, the analysis of the body yields
$\psi(x)=\{\Int,\Real\setminus\Int\}$ for the branch \code{(x\,$\in$\,Int) ? x+1 : sqrt(x)} and, since
\code{$(\Bool\vee\Real)\setminus\Real = \Bool$}, yields
$\psi(x)=\{\Bool\}$ for the branch \code{!x}. So the function
will be checked for the input types $\Int$, $\Real\setminus\Int$, and
\Bool, yielding the expected result.
It is not too difficult to generalize this rule when the lambda is
typed by an intersection type:\vspace{-.8mm}
\begin{mathpar}
\Infer[AbsInf+] {\forall i\in I\hspace*{2mm}\Gamma,x:s_i\vdash
e\triangleright\psi_i
\and
\Gamma,x:s_i\vdash
e : t_i
\and
T_i = \{ (u, w) ~|~ u\in\psi_i(x) \land \Gamma, x:u\vdash e : w\}
} {\textstyle \Gamma\vdash\lambda^{\bigwedge_{i\in
I}s_i\to t_i} x.e:\bigwedge_{i\in I}(s_i\to
t_i)\land\bigwedge_{(u, w)\in T_i}(u\to w) } {}\vspace{-3mm}
\end{mathpar}
For each arrow declared in the interface of the function, we
first typecheck the body of the function as usual (to check that the
arrow is valid) and collect the refined types for the parameter $x$.
Then we deduce all possible output types for this refined set of input
types and add the resulting arrows to the type deduced for the whole
function (see Appendix~\ref{app:optimize} for an even more precise rule).
\kim{We define the rule on the type system not the algorithm. I think
we could do the same (by collecting type scheme) in $\psi$ but we
then need to choose a candidate in the type scheme \ldots }
In summary, in order to type a
function we use the type-cases on its parameter to partition the
domain of the function and we type-check the function on each single partition rather
than on the union thereof. Of course, we could use much a finer
partition: the finest (but impossible) one is to check the function
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.
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 remarkable 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
$\psi_1\cup\psi_2$. The simplest possible definition is the
component-wise union. This definition is enough to avoid the problem
of typecases on casted values and it is also enough to type our case
study, as we showed before. However if we want a more precise typing
discipline we may want to consider a more sophisticated way of
combining the information collected by the various $\psi$. For
instance, consider the following pair
\[\code{( \ite x s {e_1}{e_2} , \ite x t {e_3}{e_4} )}\]
Then we have $x:\Any\vdash \code{( \ite x s {e_1}{e_2} , \ite x t
{e_3}{e_4} )}\triangleright x\mapsto\{s,\neg s, t, \neg t\}$. However if this
code is the body of a function with parameter $x$, then it may be
tempting to try to produce a finer-grained analysis: for example,
instead of checking as input type just $s$ and $t$ one could check
instead $s\setminus t$, $t\setminus s$, and $s\wedge t$, whenever these
three types are not empty. This can be obtained by defining the union
operation as follows:
\[ (\psi_0\cup\psi_1)(x)=\{ t \alt \exists t_1\in\psi_1(x), t_2\in\psi_2(x), t=t_1\setminus t_2 \text{ or } t=t_2\setminus t_1 \text{ or } t=t_1\wedge t_2\text{ and } t\not\simeq\Empty\}\]
Do we really gain in precision? I think the gain is minimum. All we may obtain just come from a polymorphic use of the variable, but we can hardly gain more. Probably it is not worth the effort. As a concrete case consider
\[\code{function x \{ ( \ite x {\texttt{String|Bool}} {x}{x} , \ite x {\texttt{Bool|Int}} {x}{x} )} \}\]
So what?
A simple solution would be to define the union as follows
\begin{equation}
(\psi_0\cup\psi_1)(x)=
\left\{\begin{array}{ll}
\psi_i(x) &\text{ if }\psi_i(x)\subseteq\psi_{((i+1)\,\text{mod}\,2)}(x)\\
\psi_0(x)\cup\psi_1(x) &\text{ otherwise}
\end{array}\right.
\end{equation}
and $\psi_1(x)\subseteq\psi_2(x)\iff \forall\tau\in\psi_1(x),\exists \tau'\in\psi_2(x),\tau\leq\tau'$
This would be interesting to avoid to use as domains those in
$\psi_\circ$ that would be split in two in the $\psi_1$ and $\psi_2$
of the ``if'' ... but it is probably better to check it by modifying
the rule of ``if'' (that is, add $\psi_\circ$ only for when it brings new
information).
}
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