Commit 3e1f0eb0 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

rewording

parent 668fb500
......@@ -97,7 +97,7 @@ provided to us by occurrence typing and deduce for the function in~\eqref{foo3}
function is applied to a number.
To achieve this, we simply modify the typing rule for functions that we defined
in the previous section to accommodate for gradual typing. Let $\sigma$ and $\tau$ range over \emph{gradual types}, that is the types produced by the grammar in Definition~\ref{def:types} to which we add \dyn{} as basic type (see~\citet{castagna2019gradual} for the definition of the subtyping relation on these types). For every gradual type
$\tau$, define $\tauUp$ as the (non graudal) type obtained from $\tau$ by replacing all
$\tau$, define $\tauUp$ as the (non gradual) type obtained from $\tau$ by replacing all
covariant occurrences of \dyn{} by \Any{} and all contravariant ones by \Empty. The
type $\tauUp$ can be seen as the \emph{maximal} interpretation of $\tau$, that is,
every expression that can safely be cast to $\tau$ is of type $\tauUp$. In
......
......@@ -414,11 +414,11 @@ the intersection of the static type of $\occ e \varpi$ (deduced by
\Rule{PTypeof}) with the type deduced for $\varpi$ by the other $\vdashp$ rules. The
rule \Rule{PEps} is the starting point of the analysis: if we are assuming that the test $e\in t$ succeeds, then we can assume that $e$ (i.e.,
$\occ e\epsilon$) has type $t$ (recall that assuming that the test $e\in t$ fails corresponds to having $\neg t$ at the index of the turnstyle).
The rule \Rule{PApprR} implements occurrence typing for
The rule \Rule{PAppR} implements occurrence typing for
the arguments of applications, since it states that if a function maps
arguments of type $t_1$ in results of type $t_2$ and an application of
this function yields results (in $t'_2$) that cannot be in $t_2$
(since $t_2\land t_2' \simeq \Empty$), then the argument of this application cannot be of type $t_1$. \Rule{PAppR} performs the
(since $t_2\land t_2' \simeq \Empty$), then the argument of this application cannot be of type $t_1$. \Rule{PAppL} performs the
occurrence typing analysis for the function part of an application,
since it states that if an application has type $t_2$ and the argument
of this application has type $t_1$, then the function in this
......
......@@ -876,7 +876,7 @@
\subsection{New algorithmic type system with type schemes}
As explained in TODO, we introduce for the proofs the notion of \emph{types schemes}
As explained in TODO, we introduce for the proofs the notion of \emph{type schemes}
and we define a new (more powerful) algorithmic type system that uses them.
It allows us to have a stronger (but still partial) completeness theorem.
......@@ -885,7 +885,7 @@ from the proofs of this section (see section \ref{sec:proofs_algorithmic_without
\subsubsection{Type schemes}\label{app:typeschemes}
We introduce the new syntactic category of \emph{types schemes} which are the terms~$\ts$ inductively produced by the following grammar.
We introduce the new syntactic category of \emph{type schemes} which are the terms~$\ts$ inductively produced by the following grammar.
\[
\begin{array}{lrcl}
\textbf{Type schemes} & \ts & ::= & t \alt \tsfun {\arrow t t ; \cdots ; \arrow t t} \alt \ts \tstimes \ts \alt \ts \tsor \ts \alt \tsempty
......
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