Commit b935e55d authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

small rewording

parent c6a249d1
......@@ -11,7 +11,7 @@ auxiliary deduction system for paths.
$(i)$. Multiple types have two distinct origins each requiring a distinct
technical solution. The first origin is the presence of
structural
rules
rules%
\footnote{\label{fo:rules}In logic, logical rules refer to a
particular connective (here, a type constructor, that is, either
$\to$, or $\times$, or $b$), while identity rules (e.g., axioms and
......@@ -27,7 +27,7 @@ need to define some operators on types, which are given in
Section~\ref{sec:typeops}. The second origin is the rule \Rule{Abs-}
by which it is possible to deduce for every well-typed lambda
abstraction infinitely many types, that is the annotation of the
function intersected with as many negations of arrow types as
function intersected with as (finitely) many negations of arrow types as
possible without making the type empty. We do not handle this
multiplicity directly in the algorithmic system but only in the proof
of its soundness by using and adapting the technique of \emph{type
......@@ -62,7 +62,7 @@ system given in Section~\ref{sec:algorules}.
In order to define the algorithmic typing of expressions like
applications and projections we need to define the operators on
types we used in Section~\ref{sec:ideas}. Consider the rule \Rule{App} for applications. It essentially
types we used in Section~\ref{sec:ideas}. Consider the classic rule \Rule{App} for applications. It essentially
does three things: $(i)$ it checks that the function has functional
type; $(ii)$ it checks that the argument is in the domain of the
function, and $(iii)$ it returns the type of the application. In systems
......@@ -103,7 +103,7 @@ then we define:\vspace{-1.2mm}
All the operators above but $\worra{}{}$ are already present in the
theory of semantic subtyping: the reader can find how to compute them
in~\cite[Section
6.11]{Frisch2008} (see also~\citep[\S4.4]{Cas15} for a detailed description). Below we just show the formula that computes
6.11]{Frisch2008} (see also~\citep[\S4.4]{Cas15} for a detailed description). Below we just show a new formula that computes
$\worra t s$ for a $t$ subtype of $\Empty\to\Any$. For that, we use a
result of semantic subtyping that states that every type $t$ is
equivalent to a type in disjunctive normal form and that if
......
......@@ -96,7 +96,7 @@ occurrence typing approach will refine not only the types of variables
but also the types of generic expressions (bypassing usual type
inference). Second, the result of our analysis can be used to infer
intersection types for functions, even in the absence of precise type
annotations such as the one in the definition of \code{foo} in~\eqref{foo2}: in practice, we are able to
annotations such as the one in the definition of \code{foo} in~\eqref{foo2}: to put it simply, we are able to
infer the type~\eqref{eq:inter} for the unannotated pure JavaScript code of \code{foo}. Third, we
show how to combine occurrence typing with gradual typing, and in
particular how the former can be used to optimize the compilation of
......@@ -118,7 +118,7 @@ Depending on the actual $t$ and on the static types of $x_1$ and $x_2$, we
can make type assumptions for $x_1$, for $x_2$, \emph{and} for the application $x_1x_2$
when typing $e_1$ that are different from those we can make when typing
$e_2$. For instance, suppose $x_1$ is bound to the function \code{foo} defined in \eqref{foo2}. Thus $x_1$ has type $(\Int\to\Int)\wedge(\String\to\String)$ (we used the syntax of the types of Section~\ref{sec:language} where unions and intersections are denoted by $\vee$ and $\wedge$ and have priority over $\to$ and $\times$, but not over $\neg$).
Then it is not hard to see that if $x_2:\Int{\vee}\String$, then the expression\footnote{This and most of the following expressions are just given for the sake of example. Determining the type \emph{in each branch} of expressions other than variables is interesting for constructors but less so for destructors such as applications, projections, and selections: any reasonable programmer would not repeat the same application twice, (s)he would store its result in a variable. This becomes meaningful with constructor such as pairs, as we do for instance in the expression in~\eqref{pair}.}
Then, it is not hard to see that if $x_2:\Int{\vee}\String$, then the expression\footnote{This and most of the following expressions are just given for the sake of example. Determining the type \emph{in each branch} of expressions other than variables is interesting for constructors but less so for destructors such as applications, projections, and selections: any reasonable programmer would not repeat the same application twice, (s)he would store its result in a variable. This becomes meaningful with constructor such as pairs, as we do for instance in the expression in~\eqref{pair}.}
%
\begin{equation}\label{mezzo}
\texttt{let }x_1 \texttt{\,=\,}\code{foo}\texttt{ in } \ifty{x_1x_2}{\Int}{((x_1x_2)+x_2)}{\texttt{42}}
......@@ -239,7 +239,7 @@ largest subtype of $\dom{t_1}$ such that\vspace{-1.29mm}
\begin{equation}\label{eq1}
t_1\circ s\leq \neg t
\end{equation}
In other terms, $s$ contains all the arguments that make any function
In other terms, $s$ contains all the legal arguments that make any function
in $t_1$ return a result not in $t$. Then we can safely remove from
$t_2$ all the values in $s$ or, equivalently, keep in $t_2$ all the
values of $\dom{t_1}$ that are not in $s$. Let us implement the second
......
......@@ -383,7 +383,7 @@ of rules.
{ \pvdash \Gamma e t \varpi.0:\arrow{t_1}{t_2} \\ \pvdash \Gamma e t \varpi:t_2'}
{ \pvdash \Gamma e t \varpi.1:\neg t_1 }
{ t_2\land t_2' \simeq \Empty }
\end{mathpar}\begin{mathpar}
\end{mathpar}\begin{mathpar}\vspace{-2mm}
\Infer[PAppL]
{ \pvdash \Gamma e t \varpi.1:t_1 \\ \pvdash \Gamma e t \varpi:t_2 }
{ \pvdash \Gamma e t \varpi.0:\neg (\arrow {t_1} {\neg t_2}) }
......@@ -407,7 +407,7 @@ of rules.
\Infer[PSnd]
{ \pvdash \Gamma e t \varpi:t' }
{ \pvdash \Gamma e t \varpi.s:\pair \Any {t'} }
{ }\vspace{-1.9mm}
{ }\vspace{-0.9mm}
\end{mathpar}
These rules implement the analysis described in
Section~\ref{sec:ideas} for functions and extend it to products. Let
......@@ -435,13 +435,13 @@ $\pair{t'}\Any$ (respectively, $\pair\Any{t'}$).
This concludes the presentation of our type system, which satisfies
the property of safety, deduced, as customary, from the properties
of progress and subject reduction (\emph{cf.} Appendix~\ref{app:soundness}).\vspace{-1.5mm}
of progress and subject reduction (\emph{cf.} Appendix~\ref{app:soundness}).\vspace{-.5mm}
\begin{theorem}[type safety]
For every expression $e$ such that $\varnothing\vdash e:t$ either $e$
diverges or there
exists a value $v$ of type $t$ such that $e\reduces^* v$.
\end{theorem}
\vspace{-2mm}
\vspace{-2.1mm}
......
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