Commit 2f04fe50 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

wording

parent c9956011
......@@ -58,14 +58,14 @@ union of the values of the two types). We use $\simeq$ to denote the
symmetric closure of $\leq$: thus $s\simeq t$ means that $s$ and $t$ denote the same set of values and, as such, they are semantically the same type.
\subsection{Syntax}\label{sec:syntax}
The expressions $e$ and values $v$ of our language are the terms inductively generated by the following grammars:
The expressions $e$ and values $v$ of our language are inductively generated by the following grammars:
\begin{equation}\label{expressions}
\begin{array}{lrclr}
\textbf{Expr} &e &::=& c\alt x\alt ee\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt \pi_i e\alt(e,e)\alt\tcase{e}{t}{e}{e}\\[1mm]
\textbf{Expr} &e &::=& c\alt x\alt ee\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt \pi_j e\alt(e,e)\alt\tcase{e}{t}{e}{e}\\[1mm]
\textbf{Values} &v &::=& c\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt (v,v)
\end{array}
\end{equation}
for $i=1,2$. In~\eqref{expressions}, $c$ ranges over constants
for $j=1,2$. In~\eqref{expressions}, $c$ ranges over constants
(e.g., \texttt{true}, \texttt{false}, \texttt{1}, \texttt{2},
...) which are values of basic types (we use $\basic{c}$ to denote the
basic type of the constant $c$); $x$ ranges over variables; $(e,e)$
......@@ -168,7 +168,7 @@ The first one is that, as explained in
Section~\ref{sec:challenges}, our type assumptions are about
expressions. Therefore, in our rules the type environments, ranged over
by $\Gamma$, map \emph{expressions}---rather than just variables---into
types. This explains why the classic typing rule for variables is replaced by a more general \Rule{Env} rule defined below:\beppe{Changed the name of Occ into Env since it seems more appropriate}
types. This explains why the classic typing rule for variables is replaced by a more general \Rule{Env} rule defined below:
\begin{mathpar}
\Infer[Env]
{ }
......
......@@ -3,12 +3,12 @@ As we explained in the introduction, both TypeScript and Flow deduce the type
\begin{equation}\label{tyinter}
\code{(number$\to$number)$\,\wedge\,$(string$\to$string)}
\end{equation}
can be deduced by TypeScript and Flow only if they are instructed to do so: the
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 hevier. But this seems like overkill, since a simple
type \eqref{tyinter}: we did it in \eqref{foo2} using Flow---the TypeScript annotation for it is much hevier. 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., \code{(number$\vee$string)$\setminus$number}, that is \code{string}), and this is
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}.
......@@ -48,14 +48,16 @@ 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}
%\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)$ is
the set of all the types of all the occurrences of $x$ in $e$. This
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 variable lambda abstracted
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):
\begin{mathpar}
......@@ -131,7 +133,7 @@ following rule
Note the invariant that the domain of
$\psi$ is always equal to the
domain of $\Gamma$ restricted to variables.
Simply put, this rule first collect all possible types that are deduced
Simply put, this rule first collects all possible types that are deduced
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
$x$. The re-typing ensures that that the type soundness property
......@@ -174,16 +176,16 @@ function.
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 a nutshell, what we have done is that when we have to type a
In a nutshell, what we have done is that in order to type a
function we use the type-cases on its parameter to partition the
domain of the function and test it on the single partitions rather
than on the union thereof. Of course we could use a much finer
domain of the function and we type-check the function on the single partitions 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 input. But a finer partition
would not probably return much better information since most
partitions would collapse on the same return type: type case on the
parameter are those that may do a difference, returning different
types for different partitions thus yield more precise typing.
against the singleton types of all its inputs. But any finer partition
would not in general return 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 make a difference, by returning different
types for different partitions thus yielding more precise typing.
\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