Commit 49358a9e authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

More refining.

parent 94bfb2a7
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 As explained in the introduction, both TypeScript and Flow deduce the type
\begin{alltt}\color{darkblue} \code{(number$\vee$string)$\to$number} for the function \code{foo} we
function foo(x : number | string) \{ defined.\footnote{\label{null}Actually, they
(typeof(x) === "number")? x++ : x.\textcolor{darkred}{trim()} deduce as return type \code{number$\vee$null}, since both languages
\} track the possibility that some operation may yield \code{null}
\end{alltt} results. Considering this would not pose any problem but clutter the
where \code{trim()} is the JavaScript library function that removes all blank spaces at the beginiing and end of 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): presentation, so we omit such details.}
As we have seen, a more precise type for this function is
\begin{equation}\label{tyinter} \begin{equation}\label{tyinter}
\code{(number$\to$number)$\,\wedge\,$(string$\to$string)} \code{(number$\to$number)$\,\wedge\,$(string$\to$string)}
\end{equation} \end{equation}
...@@ -20,7 +21,11 @@ type \code{number} or not (i.e., \code{(number$\vee$string)$\setminus$number}, t ...@@ -20,7 +21,11 @@ type \code{number} or not (i.e., \code{(number$\vee$string)$\setminus$number}, t
should be enough for the system to deduce the type \eqref{tyinter} should be enough for the system to deduce the type \eqref{tyinter}
even in the absence of an explicit type annotation. 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. 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
to check the body of the function. Consider a more involved example
\begin{alltt}\color{darkblue} \begin{alltt}\color{darkblue}
function (x \textcolor{darkred}{: \(\tau\)}) \{ function (x \textcolor{darkred}{: \(\tau\)}) \{
(x \(\in\) Real) (x \(\in\) Real)
...@@ -28,25 +33,28 @@ In this section we show how to do it by using the theory of occurrence typing we ...@@ -28,25 +33,28 @@ In this section we show how to do it by using the theory of occurrence typing we
: \{ \(\neg\)x \} : \{ \(\neg\)x \}
\} \}
\end{alltt} \end{alltt}
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 assume that \code{Int} is a
subtype of \code{Real}) we want to deduce for this function the
type type
\code{$(\Int\to\Int)\wedge(\Real\backslash\Int\to\Complex)\wedge(\Bool\to\Bool)$}. \code{$(\Int\to\Int)\wedge(\Real\backslash\Int\to\Real)\wedge(\Bool\to\Bool)$}.
If we omit $\tau$ and imagine that this is syntactic sugar for the When $\tau$ is \Any,
parameter to be typed with \Any\ (we do not consider polymorphism),
then the function must be rejected (since it tries to type then the function must be rejected (since it tries to type
\code{\(\neg\)x} under the assumption that \code x\ has type \code{\(\neg\)x} under the assumption that \code x\ has type
\code{$\neg\Real$}. Notice that this last syntactic sugar (i.e., \code{$\neg\Real$}. Notice that typing the function under the
typing function parameter by $\Any$ when type annotation are omitted) hypothesis that $\tau$ is \Any,
allows us to capture user-defined discrimination as defined allows us to capture user-defined discrimination as defined
by~\citet{THF10} since, for instance by~\citet{THF10} since, for instance
\begin{alltt}\color{darkblue} \begin{alltt}\color{darkblue}
let is_int x = (x\(\in\)Int)? true : false let is_int x = (x\(\in\)Int)? true : false
in if is_int z then z+1 else 42 in if is_int z then z+1 else 42
\end{alltt} \end{alltt}
is well typed since the function \code{is\_int} is given type $(\Int\to\True)\wedge(\neg\Int\to\False)$. is well typed since the function \code{is\_int} is given type
$(\Int\to\True)\wedge(\neg\Int\to\False)$. We choose a more general
approach allowing the programmer to hint a particular type for the
argument and deducing, if possible, an intersection type for the
function.
We start by considering the system where $\lambda$-abstractions are
We start by considering the system where $\lambda$-abstraction are
typed by a single arrow and later generalize it to the case of typed by a single arrow and later generalize it to the case of
intersections of arrows. First, we define the auxiliary judgement intersections of arrows. First, we define the auxiliary judgement
\begin{displaymath} \begin{displaymath}
...@@ -153,10 +161,6 @@ for a variable $x$ during typing and then uses them to re-type the body ...@@ -153,10 +161,6 @@ 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 that the type soundness property
carries over this new rule. carries over this new 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 }
This system is enough to type our case study for the case $\tau$ 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 defined as \code{Real|Bool}. Indeed the analysis of the body yields
...@@ -167,10 +171,34 @@ $\psi(x)=\{\Bool\}$ for the branch \code{$\neg$x}. So the function ...@@ -167,10 +171,34 @@ $\psi(x)=\{\Bool\}$ for the branch \code{$\neg$x}. So the function
will be checked for the input types $\Int$, $\Real\setminus\Int$, and will be checked for the input types $\Int$, $\Real\setminus\Int$, and
\Bool, yielding the expected result. \Bool, yielding the expected result.
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[AbsInf+] {\forall i\in I~\Gamma,x:s_i\vdash
e\triangleright\psi_i
\and
\Gamma,x:s_i\vdash
e : t_i
\and
T_i = \{ (u, v) ~|~ u\in\psi_i(x) \land \Gamma, x:u\vdash e : v\}
} { \Gamma\vdash\lambda^{\bigwedge_{i\in
I}s_i\to t_i} x.e:\bigwedge_{i\in I}(u_j\to
v_i)\land\bigwedge_{(u, v)\in T_i}(u\to v) } {}
\end{mathpar}
Here, for each arrow in the declared 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 the possible output types for this refined input
types and add the resulting arrows to the type we deduce for the whole
function.
{\color{darkred} RANDOM THOUGHTS: {\color{darkred} RANDOM THOUGHTS:
\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 }
A delicate point is the definition of the union A delicate point is the definition of the union
$\psi_1\cup\psi_2$. The simplest possible definition is the $\psi_1\cup\psi_2$. The simplest possible definition is the
component-wise union. This definition is enough to avoid the problem component-wise union. This definition is enough to avoid the problem
...@@ -210,16 +238,8 @@ of the ``if'' ... but it is probably better to check it by modifying ...@@ -210,16 +238,8 @@ 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 the rule of ``if'' (that is, add $\psi_\circ$ only for when it brings new
information). 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 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)?}
......
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