Commit 360e6fb8 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

bla bla

parent 362bbf8c
\subsection{Adding structured types}
{\color{gray}
\subsubsection{Products}
First thing we add a new type constructor for products.
......@@ -90,7 +91,7 @@ As an example one can consider TODO
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, in particular formulae (4.20) and (4.21))
}
\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}.
......
......@@ -551,16 +551,96 @@ Note that $\tsrep \ts \in \tsint \ts$.
\subsubsection{Operators on types}\label{sec:typeops}
\subsubsection{Operators for type constructors}\label{sec:typeops}
\paragraph{Declarative version}
Let $t$ be a functional type (i.e., $t\leq\Empty\to\Any$) then
\begin{eqnarray}
\dom t & = & \max \{ u \alt t\leq u\to \Any\}
\\
\apply t s & = &\min \{ u \alt t\leq s\to u\}
\\
\worra t s & = &\min\{u\leq \dom t\alt t\circ(\dom t\setminus u)\leq \neg s\}
\end{eqnarray}
Let $t$ be a product type (i.e., $t\leq\pair\Any\Any$) then:
\begin{eqnarray}
\bpl t & = & \min \{ u \alt t\leq \pair u\Any\}\\
\bpr t & = & \min \{ u \alt t\leq \pair \Any u\}
\end{eqnarray}
\paragraph{Algorithmic version}
If
\[ t \simeq \bigvee_{i\in I}\left(\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n')\right) \]
with \[\forall i\in I.\ \bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n') \not\simeq \Empty\]
then
\begin{eqnarray*}
\dom{t} & = & \bigwedge_{i\in I}\bigvee_{p\in P_i}s_p\\[4mm]
t\circ s & = & \bigvee_{i\in I}\left(\bigvee_{\{Q\subsetneq P_i\alt s\not\leq\bigvee_{q\in Q}s_q\}}\left(\bigwedge_{p\in P_i\setminus Q}t_p\right)\right)\hspace*{1cm}\makebox[0cm][l]{(for $s\leq\dom{t}$)}\\[4mm]
\worra t s & = & \dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P\subset P_i\alt s\leq \bigvee_{p \in P} \neg t_p\}}\left(\bigvee_{p \in P} \neg s_p\right) \right)
\end{eqnarray*}
\beppe{Explain, especially the last one}
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, in particular formulae (4.20) and (4.21))
\subsubsection{Type environments for occurrence typing}\label{sec:typenv}
\[
\begin{array}{lcl}
\typep+\epsilon{\Gamma,e,t} & = & t\\
\typep-\epsilon{\Gamma,e,t} & = & \neg t\\
\typep{p}{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\Gp p{\Gamma,e,t}{(\varpi.1)}}{\neg \Gp p {\Gamma,e,t} (\varpi)})\\
\typep{p}{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\Gp p {\Gamma,e,t} (\varpi)}\\
\typep{p}{\varpi.l}{\Gamma,e,t} & = & \bpl{\Gp p {\Gamma,e,t} (\varpi)}\\
\typep{p}{\varpi.r}{\Gamma,e,t} & = & \bpr{\Gp p {\Gamma,e,t} (\varpi)}\\
\typep{p}{\varpi.f}{\Gamma,e,t} & = & \pair{\Gp p {\Gamma,e,t} (\varpi)}\Any\\
\typep{p}{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\Gp p {\Gamma,e,t} (\varpi)}\\ \\
\Gp p {\Gamma,e,t} (\varpi) & = & \typep p \varpi {\Gamma,e,t} \land \tsrep {\tyof {\occ e \varpi} \Gamma}\\
%\underbrace{\land \tyof {\occ e \varpi} {\Gamma\setminus\{\occ e \varpi\}}}_{\text{if $\occ e \varpi$ is not a variable}}}\\
\end{array}
\]
\begin{align*}
&(\RefineStep p {e,t} (\Gamma))(e') =
\left\{\begin{array}{ll}
%\tyof {e'} \Gamma \tsand
\bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}}
\Gp p {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\
\Gamma(e') & \text{otherwise, if } e' \in \dom \Gamma\\
\text{undefined} & \text{otherwise}
\end{array}\right.\\
&\Refine p {e,t} \Gamma=\fixpoint_\Gamma (\RefineStep p {e,t})\qquad \text{(for the order $\leq$ on environments, defined in the proofs section)}
\end{align*}
All the functions above are defined iff all their subexpressions are (e.g., $\occ e{\varpi.i}$ must be defined).
The notation $\tyof{o}{\Gamma}$ denotes the type that can be deduced for the occurence $o$ under the type envirenment $\Gamma$.
That is, $\tyof{o}{\Gamma}=\ts$ if and only if $\Gamma\vdash o:\ts$ can be deduced by the typing rules.
\footnote{Note that the definition is well-founded.
This can be seen by analyzing the rule \Rule{If}: the definition of $\Refine + {e,t} \Gamma$ and $\Refine - {e,t} \Gamma$ 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:\ts_0$ (and this is possible only if we were able to deduce under the hypothesis $\Gamma$ the type of every occurrence of $e$.)}
The reason for the definition of $\RefineStep p {e,t}$ is that the same subterm of $e$
may occur several times in $e$ and therefore we can collect for every
occurrence a different type constraint. Since all the constraints must
hold, then we take their intersection. For instance, if $f$ is a function
of type $(s_1\times s_2\to t)\wedge( s_3\to\neg t)$ and we test
whether $f(x,x)$ is of type $t$ or not, then the test succeed only if $(x,x)$ is of
type $s_1\times s_2$, that is, that $x$ has both type $s_1$ and type
$s_2$ and thus their intersection $s_1{\wedge}s_2$.
\subsection{Algorithmic typing rules}\label{sec:algorules}
......
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