Commit 20ad3030 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

rewriting

parent 4d21eb5b
......@@ -60,7 +60,21 @@ Let $e$ be an expression, $t$ a type, $\Gamma$ a type environment, $\varpi\in\{0
\typep{p}{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\typep p \varpi{\Gamma,e,t}}
\end{array}
\]
and extend the previous definitions $\Gp p {\Gamma,e,t}(\varpi)$ and $\Gamma^p_{\Gamma,e,t}$ to the new paths. All it remains to do is to add the typing rules for the new expressions:
and extend the previous definitions $\Gp p {\Gamma,e,t}(\varpi)$ and
$\Gamma^p_{\Gamma,e,t}$ to the new paths. The reason why in the
definition of $\typep{p}{\varpi.l}{\Gamma,e,t}$ and
$\typep{p}{\varpi.l}{\Gamma,e,t}$ we intersected $\typep p
\varpi{\Gamma,e,t}$ with $\pair\Any\Any$ is to ensure that the
operators $\bpl{}$ and $\bpr{}$ are defined. It handles the (admitedly
stupid) cases in which an \texttt{if} tests whether a pair has a type
which contains values other than pairs, such as for instance
%
$$\ite {(x,y)}{((\pair\Int\Int)\vee(\Int\to\Bool))}{...}{...},$$
%
thus deducing the type $\Int$ for the occurrences of $x$ and $y$ in the \texttt{then} branch.
All it remains to do is to add the typing rules for the new expressions:
\begin{mathpar}
\Infer[Proj]
......@@ -74,9 +88,11 @@ and extend the previous definitions $\Gp p {\Gamma,e,t}(\varpi)$ and $\Gamma^p
{(e_1,e_2)\not\in\dom\Gamma}
\end{mathpar}
As an example one can consider
As an example one can consider
Finally, for what concerns the algorithmic part, the operators $\bpi_{\boldsymbol 1}$ and $\bpi_{\boldsymbol 2}$ are standard in the semantic subtyping framework and they can be computed as described by~\citet{???} (see also~\citep[\S4.4.1]{Cas15} for a detailed description)
Finally, for what concerns the algorithmic part, the operators $\bpi_{\boldsymbol 1}$ and $\bpi_{\boldsymbol 2}$ are standard in the semantic subtyping framework and they can be computed as described by~\citet{} (see also~\citep[\S4.4.1]{Cas15} for a detailed description)
\subsubsection{Lists} The work above on pairs is enough for having also the lists. It suffices to encode them as right associative nested pairs, as it is done in the language CDuce. The interesting part is that thanks to the presence of union and recursive types one can type heterogeneous lists whose content is described by regular expressions on types as proposed by~\citet{hosoyapierce}.
......@@ -117,12 +133,13 @@ where {\Cast{$t$}{$e$}} is a type-cast.\footnote{Intuitively, \code{\Cast{$t$}{$
We have already seen in the introduction that by using occurrence
typing combined with a union type instead of the gradual type \code{?}
for parameter annotation, we can avoid the insertion of any cast. But
occurrence typing can be used also on the gradually typed code. This
occurrence typing can be used also on the gradually typed code. If we use
occurrence typing in typing the gradually-typed version of the code of \code{foo} this
allows the system to avoid inserting the first cast
\code{\Cast{number}{x}} since, thanks to occurrence typing, the
occurrence of \code{x} at issue is given type \code{number} (the
second cast is still necessary instead). But removing this cast is far
from satisfactory, since when this function is applied to an integer
from being satisfactory, since when this function is applied to an integer
there are some casts that still need to be applied at the
application. The reason is that the compiled version of the function
has type \code{?$\to$number}, it therefore expects an argument of type
......@@ -155,7 +172,7 @@ a first class type, and not just a directive to the
front-end. Whatever solution we choose it is clear that in both cases
it would be much better if the application \code{foo(42)} were
compiled as it is, thus getting rid of a cast that at best is useless
and at worse give a counterintuitive and unexpected semantics.
and at worse gives a counterintuitive and unexpected semantics.
......@@ -202,7 +219,7 @@ 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 allows us to
\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}
......
......@@ -78,7 +78,7 @@ Let $e$ be an expression, $t$ a type, $\Gamma$ a type environment, $\varpi\in\{0
\]
All the functions above are defined iff all their subexpressions are (e.g., $\occ e{\varpi.i}$ must be defined).
Let $\Gamma$ be a type environment and $o$ an occurrence. We denote $\tyof{o}{\Gamma}$ the type that can be deduced for $o$ under the type envirenment $\Gamma$. That is, $\tyof{o}{\Gamma}=t$ if and only if $\Gamma\vdash o:t$ can be deduced by the rules below.
Let $\Gamma$ be a type environment and $o$ an occurrence. We denote $\tyof{o}{\Gamma}$ the type that can be deduced for $o$ under the type envirenment $\Gamma$. That is, $\tyof{o}{\Gamma}=t$ if and only if $\Gamma\vdash o:t$ can be deduced by the rules below.\footnote{Note that the definition is well-founded. This can be seen by analyzing the rule \Rule{If}: the definition of $\Gamma^+_{\Gamma,e,t}$ and $\Gamma^-_{\Gamma,e,t}$ use $\tyof{\occ e{\varpi}}\Gamma$, and this is defined for all $\varpi$ since the first premisses of \Rule{If} states that $\Gamma\vdash e:t_\circ$ (and this is possible only if we were able to deduce under the hypothesis $\Gamma$ the type of every occurrence of $e$.)}
In what follows we will omit the indexes $e$ and $\Gamma,e,t$ when they are clear from the context.
......@@ -131,8 +131,8 @@ We define the following algorithmic system (we deduce at most one type for every
{\Gamma\vdash e:t_\circ\\
\Gamma, \Gamma^+_{\Gamma,e,t}\vdash e_1 : t_1\\
\Gamma, \Gamma^-_{\Gamma,e,t}\vdash e_2 : t_2}
{\Gamma\vdash \ite e t {e_1}{e_2}: t_1\vee t_2}
{\makebox[3cm][l]{$\ite e t {e_1}{e_2}\not\in\dom\Gamma$}}
{\Gamma\vdash \ite {e} t {e_1}{e_2}: t_1\vee t_2}
{\makebox[3cm][l]{$\ite {e} t {e_1}{e_2}\not\in\dom\Gamma$}}
\\\end{mathpar}
The side condition for constants is probably interesting only for functional constants that have union and/or intersection arrow types. Notice that we we can have a more precise typing discipline by not typing a branch whenever the corresponding $\Gamma^p_{\Gamma,e,t}$ maps some expression $e$ into $\Empty$, since this means that the branch could not be selected under the current typing hypotheses.
......
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