Commit 65e90d07 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

more on refining

parent 9cd4ebdb
......@@ -326,31 +326,6 @@ Note that every time the function is applied to an argument of type $s_i$ no cas
To see how this work, consider again our case study for the case $\tau$ equal to \code{?}. The analysis would yield $\psi(x)=\{\Int,\Real\setminus\Int\}$ for the branch \code{(x $\in$ Int) ? succ x : sqrt x} (as before), but yield $\psi(x)=\{\Any\setminus\Real\}$ for the branch \code{$\neg$x}. Therefore, according to the rule above the function would be checked for the input types, $\Int$, $\Real\setminus\Int$, $\Any\setminus\Real$, and $\code{?}\setminus(\Int\vee(\Real\setminus\Int)$. The typing would fail for the case $\Any\setminus\Real$ leaving just the relevant cases.
This also show how to generalize this technique for functions that are
already typed with intersection types (of static types, or of just one
gradual type): if we want to type a function annotated by
$\bigwedge_{i\in I} s_i\to t_i$ then we perform the analysis for each
distinct $s_i$ and single out the cases for which a more precise
typing can be obtained, and finally take the huge intersection of all
subcases.
\begin{mathpar}
\Infer[Abs]
{\forall i\in I~\Gamma,x:s_i\vdash e\triangleright\psi_i
\quad
\Gamma,x:s_i\setminus\textstyle\vee_{i\in J_i}u_i\vdash e:t_i
\quad
\forall j\in J_i~\Gamma,x:u_j\vdash e:v_j\leq t_i }
{
\Gamma\vdash\lambda^{\bigwedge_{i\in I}s_i\to t_i} x.e:\bigwedge_{i\in I}((s_i\setminus\vee_{j\in J_i}u_i)\to t_i) \wedge(\textstyle\bigwedge_{j\in J_i}u_j\to v_i))
}
{\psi_i(x)\supseteq\{u_j\alt j\in J_i\}\supsetneq\varnothing}
\end{mathpar}
\beppe{Problem 1: is it true that this typing techniques captures all the ``inituitive cases''? That is to say, is it true that this typing and the semantics in which in type case we strip all ``negative'' casts off the resulting values are equivalent? That is they yield the to the same result (probably module the stripping of negatibe casts)?}
\beppe{Problem 2: how to compile functions with intersection types, since their body is typed several distinct types. I see two possible solutions: either merge the casts of the various typings (as we did in the compilation of polymorphic functions for semantic subtyping) or allow just one gradual type in the intersection when a function is explicitly typed (reasonable since, why would you use more gradual types in an intersection?)}
\subsection{Limitations}
......
Both TypeScript and Flow deduce for the function \code{foo} in the introduction the type $\code{number | string}\to\code{number}$.\footnote{Actually they deduce as return type \code{number | string | null}, but it does not matter}
Consider the following modification of our example.
Both TypeScript and Flow deduce the type \code{(number$\vee$string)$\to$number} for the function \code{foo} we defined in the introduction.\footnote{\label{null}Actually, they deduce as return type \code{number$\vee$null}, since both languages track the possibility that some operation may yield \code{null} results. Considering this would not pose any problem but clutter the presentation, so we omit such details.} Consider, next the following slight modification of that example
\begin{alltt}\color{darkblue}
function foo(x\textcolor{darkred}{ : number | string}) \{
(typeof(x) === "number")? x++ : x.tile()
function foo(x : number | string) \{
(typeof(x) === "number")? x++ : x.\textcolor{darkred}{tile()}
\}
\end{alltt}
where \code{tile()} is the JavaScript library function that removes all blank spaces from a string. Now the type deduce is \code{number | string}$\to$\code{number | string} but it is clear that a better type for this function would be the intersection type ...
Currently it is possible to deduce this type both in Typescript and Flow by explicit annotations. But it is clear that that the current use of typeof should be enough to suggest the system to check separatly the types for \code{number} and for \code{string} (i.e., \code{number | string}$\setminus$\code{number}). )
More generally we can refine the type of a function with intersection in may different ways, but we use the analysis of our occurrence typing to do it
\vdots
\bigskip
\vdots
The case of study is the following function
where \code{tile()} is the JavaScript library function that removes all blank spaces from a string. Now, the type deduced is \code{(number$\vee$string)$\to$(number$\vee$string)}, but it is clear that a better type for this function would be the following intersection type (Footnote~\ref{null} applies here, too):
\begin{equation}\label{tyinter}
\code{(number$\to$number)$\,\wedge\,$(string$\to$string)}
\end{equation}
since this would allow to deduce for, say, \code{foo(42)} the
type \code{number} instead of the less precise
type \code{number$\vee$string}. Both TypeScript and Flow can deduce
for \code{foo} the type \eqref{tyinter}, but only if they are instructed to do so: the
programmer has to explicitly annotate \code{foo} with the
type \eqref{tyinter}. But this seems like overkill, since a simple
analysis of the body of \code{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., \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 of an explicit type annotation.
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 the parameter of a function is assigned in its body to determine a partition of the domain types againt which check the body of the function. Let us consider an example more general than the one above.
\begin{alltt}\color{darkblue}
function (x \textcolor{darkred}{: \(\tau\)}) \{
(x \(\in\) Real) ?
......@@ -33,34 +28,29 @@ The case of study is the following function
: \{ \(\neg\)x \}
\}
\end{alltt}
first we consider the case without gradual typing. In particular when
$\tau$ is \code{Real|Bool} (we suppose that \code{Int} is a subtype of \code{Real}) we want to deduce for this function the
When $\tau$ is \code{Real|Bool} (we suppose that \code{Int} is a subtype of \code{Real}) we want to deduce for this function the
type
\code{$(\Int\to\Int)\wedge(\Real\backslash\Int\to\Complex)\wedge(\Bool\to\Bool)$}. No
cast is inserted, of course.
Then we consider gradual typing and in particular when $\tau$ is
\code{?}. Then we want to deduce for this function the type
\code{$(\Int\to\Int)\wedge(\Real\backslash\Int\to\Complex)\wedge(?\backslash\Real\to\Bool)$},
and a cast is inserted on the last occurrence of \code x\ which is
compiled as \code{\(\neg\)(\Cast{Bool}{x})}.
\code{$(\Int\to\Int)\wedge(\Real\backslash\Int\to\Complex)\wedge(\Bool\to\Bool)$}.
If we omit $\tau$ and imagine that this is syntactic sugar for the
parameter to be typed with \Any\ (we do not consider polymorphism),
then the function must be rejected (since it tries to type
\code{\(\neg\)x} under the assumption that \code x\ has type
\code{$\neg\Real$}. Notice that this last syntactic sugar (i.e., typing function parameter by $\Any$ when type annotation are omitted) allows us to
capture user-defined discrimination as defined by ~\citet{THF10}
since, for instance
\code{$\neg\Real$}. Notice that this last syntactic sugar (i.e.,
typing function parameter by $\Any$ when type annotation are omitted)
allows us to capture user-defined discrimination as defined
by~\citet{THF10} since, for instance
\begin{alltt}\color{darkblue}
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)$
Here is how to do it first for non-gradual types.
First we define the auxiliary deduction system that collects type information on the variable lambda abstracted (i.e., those in the domain of $\Gamma$):
We start by considering the system where $\lambda$-abstraction are
typed by a single arrow and later generalaze it to the case of
intersections of arrows. First, we define the auxiliary deduction system
that collects type information on the variable lambda abstracted
(i.e., those in the domain of $\Gamma$):
\begin{mathpar}
......@@ -87,8 +77,8 @@ First we define the auxiliary deduction system that collects type information on
\\
\Infer[If]
{\Gamma\vdash e\triangleright\psi_\circ\\
\Gamma, \Gamma^+_{\Gamma,e,t}\vdash e_1\triangleright\psi_1\\
\Gamma, \Gamma^-_{\Gamma,e,t}\vdash e_2\triangleright\psi_2}
\Gamma \evdash + e t \Gamma^+\\ \Gamma^+\vdash e_1\triangleright\psi_1\\
\Gamma \evdash + e t \Gamma^- \\ \Gamma^-\vdash e_2\triangleright\psi_2}
{\Gamma\vdash \ite e t {e_1}{e_2}\triangleright\psi_\circ\cup\psi_1\cup\psi_2}
{}
\\
......@@ -107,7 +97,7 @@ First we define the auxiliary deduction system that collects type information on
Where
\begin{enumerate}
\item STL is the set of expressions in simply-typed lambda calculus (i.e., expression without any type-case occurring in them),
\item STL is the set of expressions in simply-typed lambda calculus with pairs (i.e., expression without any type-case occurring in them),
\item $\{\Gamma\}$ is the function that maps $\Gamma(e)$ into $\{\Gamma(e)\}$ if $e$ is a variable and undefined otherwise
......@@ -117,7 +107,7 @@ Where
\end{enumerate}
And now all we need to do is to modify the typing rule for lambdas as follows
And now all we need to do is to modify the typing rule for lambdas as follows\beppe{I omitted the negated arrows}
\begin{mathpar}
\Infer[Abs]
{\Gamma,x:t\vdash e\triangleright\psi\and \forall i\in I\quad \Gamma,x:s_i\vdash e:t_i }
......@@ -126,7 +116,7 @@ And now all we need to do is to modify the typing rule for lambdas as follows
}
{\psi(x)=\{s_i\alt i\in I\}}
\end{mathpar}
Note the invariant that the domain of $\psi$ is always equal to the domain of $\Gamma$ restricted to variables. It is not too difficult to generalize this rule when the lambda is typed by an intersection type.
Note the invariant that the domain of $\psi$ is always equal to the domain of $\Gamma$ restricted to variables.
This system is enough to type our case study for the case $\tau$ 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 \code{$(\Bool\vee\Real)\setminus\Real = \Bool$}, yields $\psi(x)=\{\Bool\}$ for the branch \code{$\neg$x}. So the function will be checked for the input types $\Int$, $\Real\setminus\Int$, and \Bool, yielding the expected result.
......@@ -172,3 +162,21 @@ 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).
}
It is not too difficult to generalize this rule when the lambda is typed by an intersection type. Indeed, even if the programmer has specified a particular intersection type for the function we may want to refine each of its arrow. This is exactly what the following rule does:
\begin{mathpar}
\Infer[Abs] {\forall i\in I~\Gamma,x:s_i\vdash
e\triangleright\psi_i \quad \forall j\in J_i~\Gamma,x:u_j\vdash
e:v_j\leq t_i } { \Gamma\vdash\lambda^{\bigwedge_{i\in
I}s_i\to t_i} x.e:\bigwedge_{i\in I,j\in J_i}(u_j\to
v_i) } {\psi_i(x)=\{u_j\alt j\in
J_i\}}
\end{mathpar}
\beppe{Problem 1: is it true that this typing techniques captures all the ``inituitive cases''? That is to say, is it true that this typing and the semantics in which in type case we strip all ``negative'' casts off the resulting values are equivalent? That is they yield the to the same result (probably module the stripping of negatibe casts)?}
\beppe{Problem 2: how to compile functions with intersection types, since their body is typed several distinct types. I see two possible solutions: either merge the casts of the various typings (as we did in the compilation of polymorphic functions for semantic subtyping) or allow just one gradual type in the intersection when a function is explicitly typed (reasonable since, why would you use more gradual types in an intersection?)}
\beppe{Explain why we use the type cases for our inference}
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