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

Language section

parent 0d323ff4
......@@ -549,47 +549,70 @@ Note that $\tsrep \ts \in \tsint \ts$.
}
{}
\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
{}\beppe{The explaination that follows is redundant in Section~\ref{sec:ideas}. Harmonize!}
In order to define the algorithmic typing of expressions like
applications and projections we need to define the operator on
types we used in Section~\ref{sec:ideas}. Consider the rule \Rule{App} for applications. It essentially
does three things: $(1)$ it checks that the function has functional
type; $(2)$ it checks that the argument is in the domain of the
function, and $(3)$ it returns the type of the application. In systems
without set-theoretic types these operations are quite
straightforward: $(1)$ corresponds to checking that the function has
an arrow type, $(2)$ corresponds to checking that the argument is in
the domain of the arrow deduced for the function and $(3)$ corresponds
to returning the codomain of that same arrow. With set-theoretic types
things are more difficult since a function can be typed by, say, a
union of intersection of arrows and negations of types. Checking that
the function has a functional type is easy since it corresponds to
checking that it has a type subtype of $\Empty\to\Any$. Determining
its domain and the type of the application is more complicated. For
instance if we have a function of type \code{\(t=(\Int \to \Int)\) \(\wedge\) \((\Bool \to \Bool)\)}, which
denotes functions that will return an integer if applied to an integer,
and will return a Boolean if applied to a Boolean.
It is possible to compute the domain of such a type
(i.e., of the functions of this type), denoted by
\code{\( \texttt{dom}(t) = \Int \vee \Bool \)},
that is the union of all the possible
input types. But what is the precise return type of such a
function? It depends on what the argument of such a function is:
either an integer or a Boolean---or both, denoted by the union type
\(\Int\vee\Bool\). This is computed by an operator we denote by \( \circ \).
More precisely, we denote by \( t_1\circ t_2\) the type of
an application of a function of type \(t_1\) to an argument of
type \(t_2\).
In the example with \code{\(t=(\Int \to \Int)\) \(\wedge\) \((\Bool \to \Bool)\)}, it gives \code{\( t \circ \Int = \Int \)},
\code{\( t \circ \Bool = \Bool \)}, and
\code{\( t \circ (\Int\vee\Bool) = \Int \vee \Bool \)}. In summary, given a functional type $t$ (\emph{ie}, a type $t$ such that $t\leq\Empty\to\Any$) our algorithms we use the following three operators
\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\}
\worra t s & = &\min\{u\leq \dom t\alt t\circ(\dom t\setminus u)\leq \neg s\}\label{worra}
\end{eqnarray}
\beppe{Wouldn't $\worra t s = \min\{u \alt t\circ(\dom t\setminus u)\leq \neg s\}$ be enough?}
The first two operators belongs to the theory of semantic subtyping while the last one is new and we described it in Section~\ref{sec:ideas}
Let $t$ be a product type (i.e., $t\leq\pair\Any\Any$) then:
We need similar operators for projections since the type $t$ of $e$ in $\pi_i e$ may not be a single product type but, say, a union of products: all we know is that $t$ must be a subtype of $\pair\Any\Any$. So let $t$ be a type such that $t\leq\pair\Any\Any$) then we define:
\begin{eqnarray}
\bpl t & = & \min \{ u \alt t\leq \pair u\Any\}\\
\bpr t & = & \min \{ u \alt t\leq \pair \Any u\}
\end{eqnarray}
All the operators above but $\worra{}{}$ are already present in the theory of semantic subtyping. The reader can find how to compute them and how to extend them to type schemes in~\cite[Section 6.11]{Frisch2008}. Below we just show the 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 furthermore $t\leq\Empty\to\Any$, then $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 $\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n') \not\simeq \Empty$ for all $i$ in $I$. For such a $t$ and any type $s$ then we have:
%
\begin{equation}
\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{equation}
\beppe{Explain the formula?}
The proof that this type satisfies \eqref{worra} is given in the Appendix~ref{}.
\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}
......@@ -694,9 +717,9 @@ $s_2$ and thus their intersection $s_1{\wedge}s_2$.
%\end{array}$}
\Refine + {e,t} \Gamma \vdashA e_1 : \ts_1\\
\Refine - {e,t} \Gamma \vdashA e_2 : \ts_2}
{\Gamma\vdashA \ite {e} t {e_1}{e_2}: \ts_1\tsor \ts_2}
{\Gamma\vdashA \tcase {e} t {e_1}{e_2}: \ts_1\tsor \ts_2}
%{\ite {e} t {e_1}{e_2}\not\in\dom\Gamma}
{\texttt{if}\dots\not\in\dom\Gamma}
{ \tcase {e} {t\!} {\!e_1\!}{\!e_2}\not\in\dom\Gamma}
\\
\Infer[Proj$_{\scriptscriptstyle\mathcal{A}}$]
{\Gamma \vdashA e:\ts\and \ts\leq\pair\Any\Any}
......
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