Commit 7f0d3a38 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

more on removing type schemes

parent 02aec485
......@@ -8,7 +8,7 @@ $(i)$~how to handle the fact that it is possible to deduce several
types for the same well-typed expression and $(ii)$~how to compute the
auxiliary deduction system for paths.
Multiple types have two distinct origins each requiring a distinct
$(i)$. Multiple types have two distinct origins each requiring a distinct
technical solution. The first origin is the presence of structural
rules\footnote{\label{fo:rules}In logic, logical rules refer to a
particular connective (here, a type constructor, that is, either
......@@ -32,14 +32,14 @@ its soundness by using and adapting the technique of \emph{type
representations of the infinite sets of types of
$\lambda$-abstractions which can be used to define an algorithmic
system that can be easily proved to be sound. The simpler algorithm
that we propose in this section implies the one with type schemes (cf
that we propose in this section implies (i.e., it is less precise than) the one with type schemes (cf.\
Theorem~\ref{????}) and it is thus sound, too. The algorithm of this
section is not only simpler but, as we discuss in Section~\ref{???},
is also the one that should be used in practice. This is why we preferred to
present it here and relegate the presentation of type schemes to
Appendix~\ref{???}.
For what concerns the use of the auxiliary derivation for the $\Gamma \evdash e t \Gamma' $ and $\pvdash \Gamma e t \varpi:t'$
$(ii)$. For what concerns the use of the auxiliary derivation for the $\Gamma \evdash e t \Gamma' $ and $\pvdash \Gamma e t \varpi:t'$
judgments, we present in Section~\ref{sec:typenv} an algorithm that is sound and satisfies a limited form of
completeness. All these notions are then used in the algorithmic typing
system given in Section~\ref{sec:algorules}.
......@@ -53,70 +53,6 @@ system given in Section~\ref{sec:algorules}.
%% }
\subsubsection{Type schemes}\label{sec:type-schemes}
We introduce the new syntactic category of \emph{types 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
\end{array}
\]
Type schemes denote sets of types, as formally stated by the following definition:
\begin{definition}[Interpretation of type schemes]
We define the function $\tsint {\_}$ that maps type schemes into sets of types.\vspace{-2.5mm}
\begin{align*}
\begin{array}{lcl}
\tsint t &=& \{s\alt t \leq s\}\\
\tsint {\tsfunone {t_i} {s_i}_{i=1..n}} &=& \{s\alt
\exists s_0 = \bigwedge_{i=1..n} \arrow {t_i} {s_i}
\land \bigwedge_{j=1..m} \neg (\arrow {t_j'} {s_j'}).\
\Empty \not\simeq s_0 \leq s \}\\
\tsint {\ts_1 \tstimes \ts_2} &=& \{s\alt \exists t_1 \in \tsint {\ts_1}\
\exists t_2 \in \tsint {\ts_2}.\ \pair {t_1} {t_2} \leq s\}\\
\tsint {\ts_1 \tsor \ts_2} &=& \{s\alt \exists t_1 \in \tsint {\ts_1}\
\exists t_2 \in \tsint {\ts_2}.\ {t_1} \vee {t_2} \leq s\}\\
\tsint \tsempty &=& \varnothing
\end{array}
\end{align*}
\end{definition}
Note that $\tsint \ts$ is closed under subsumption and intersection
and that $\tsempty$, which denotes the
empty set of types is different from $\Empty$ whose interpretation is
the set of all types.
\begin{lemma}[\cite{Frisch2008}]
Let $\ts$ be a type scheme and $t$ a type. It is possible to decide the assertion $t \in \tsint \ts$,
which we also write $\ts \leq t$.
\end{lemma}
We can now formally define the relation $v\in t$ used in
Section~\ref{sec:opsem} to define the dynamic semantics of
the language. First, we associate each (possibly, not well-typed)
value to a type scheme representing the best type information about
the value. By induction on the definition of values: $\tyof c {} =
\basic c$, $\tyof {\lambda^{\wedge_{i\in I}s_i\to t_i} x.e}{}=
\tsfun{s_i\to t_i}_{i\in I}$, $\tyof {(v_1,v_2)}{} = \tyof
{v_1}{}\tstimes\tyof {v_1}{}$. Then we have $v\in t\iffdef \tyof
v{}\leq t$.
We also need to perform intersections of type schemes so as to intersect the static type of an expression (i.e., the one deduced by conventional rules) with the one deduced by occurrence typing (i.e., the one derived by $\vdashp$). For our algorithmic system (see \Rule{Env$_{\scriptscriptstyle\mathcal{A}}$} in Section~\ref{sec:algorules}) all we need to define is the intersection of a type scheme with a type:
\begin{lemma}[\cite{Frisch2008}]
Let $\ts$ be a type scheme and $t$ a type. We can compute a type scheme, written $t \tsand \ts$, such that
\(\tsint {t \tsand \ts} = \{s \alt \exists t' \in \tsint \ts.\ t \land t' \leq s \}\)
\end{lemma}
Finally, given a type scheme $\ts$ it is straightforward to choose in its interpretation a type $\tsrep\ts$ which serves as the canonical representative of the set (i.e., $\tsrep \ts \in \tsint \ts$):
\begin{definition}[Representative]
We define a function $\tsrep {\_}$ that maps every non-empty type scheme into a type, \textit{representative} of the set of types denoted by the scheme.\vspace{-2mm}
\begin{align*}
\begin{array}{lcllcl}
\tsrep t &=& t & \tsrep {\ts_1 \tstimes \ts_2} &=& \pair {\tsrep {\ts_1}} {\tsrep {\ts_2}}\\
\tsrep {\tsfunone {t_i} {s_i}_{i\in I}} &=& \bigwedge_{i\in I} \arrow {t_i} {s_i} \qquad& \tsrep {\ts_1 \tsor \ts_2} &=& \tsrep {\ts_1} \vee \tsrep {\ts_2}\\
\tsrep \tsempty && \textit{undefined}
\end{array}\vspace{-4mm}
\end{align*}
\end{definition}
\subsubsection{Operators for type constructors}\label{sec:typeops}
......@@ -124,13 +60,13 @@ Finally, given a type scheme $\ts$ it is straightforward to choose in its interp
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
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
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
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
straightforward: $(i)$ corresponds to checking that the function has
an arrow type, $(ii)$ corresponds to checking that the argument is in
the domain of the arrow deduced for the function, and $(iii)$ corresponds
to returning the codomain of that same arrow. With set-theoretic types
things get more difficult, since a function can be typed by, say, a
union of intersection of arrows and negations of types. Checking that
......@@ -161,7 +97,7 @@ then we define:\vspace{-1.2mm}
\end{equation}
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 their definition to type schemes in~\cite[Section
in~\cite[Section
6.11]{Frisch2008} (see also~\citep[\S4.4]{Cas15} for a detailed description). 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
......@@ -188,33 +124,33 @@ Appendix~\ref{app:worra}.
\subsubsection{Type environments for occurrence typing}\label{sec:typenv}
The last step for our presentation is to define the algorithm for the
The second ingredient necessary to the definition of our algorithmic systems is the algorithm for the
deduction of $\Gamma \evdash e t \Gamma'$, that is an algorithm that
takes as input $\Gamma$, $e$, and $t$, and returns an environment that
extends $\Gamma$ with hypotheses on the occurrences of $e$ that are
the most general that can be deduced by assuming that $e\in t$ succeeds. For that we need the notation $\tyof{e}{\Gamma}$ which denotes the type scheme deduced for $e$ under the type environment $\Gamma$ in the algorithmic type system of Section~\ref{sec:algorules}.
That is, $\tyof{e}{\Gamma}=\ts$ if and only if $\Gamma\vdashA e:\ts$ is provable.
the most general that can be deduced by assuming that $e\,{\in}\,t$ succeeds. For that we need the notation $\tyof{e}{\Gamma}$ which denotes the type deduced for $e$ under the type environment $\Gamma$ in the algorithmic type system of Section~\ref{sec:algorules}.
That is, $\tyof{e}{\Gamma}=t$ if and only if $\Gamma\vdashA e:t$ is provable.
We start by defining the algorithm for each single occurrence, that is for the deduction of $\pvdash \Gamma e t \varpi:t'$. This is obtained by defining two mutually recursive functions $\constrf$ and $\env{}{}$:\vspace{-1.3mm}
\begin{eqnarray}
\constr\epsilon{\Gamma,e,t} & = & t\label{uno}\\[\sk]
\constr{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\env {\Gamma,e,t}{(\varpi.1)}}{\neg \env {\Gamma,e,t} (\varpi)})\label{due}\\[\sk]
\constr{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\env {\Gamma,e,t} (\varpi)}\label{tre}\\[\sk]
\constr{\varpi.1}{\Gamma,e,t} & = & \worra{{\tyof{\occ e{\varpi.0}}\Gamma}}{\env {\Gamma,e,t} (\varpi)}\label{tre}\\[\sk]
\constr{\varpi.l}{\Gamma,e,t} & = & \bpl{\env {\Gamma,e,t} (\varpi)}\label{quattro}\\[\sk]
\constr{\varpi.r}{\Gamma,e,t} & = & \bpr{\env {\Gamma,e,t} (\varpi)}\label{cinque}\\[\sk]
\constr{\varpi.f}{\Gamma,e,t} & = & \pair{\env {\Gamma,e,t} (\varpi)}\Any\label{sei}\\[\sk]
\constr{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\env {\Gamma,e,t} (\varpi)}\label{sette}\\[.8mm]
\env {\Gamma,e,t} (\varpi) & = & \tsrep {\constr \varpi {\Gamma,e,t} \tsand \tyof {\occ e \varpi} \Gamma}\label{otto}
\env {\Gamma,e,t} (\varpi) & = & {\constr \varpi {\Gamma,e,t} \wedge \tyof {\occ e \varpi} \Gamma}\label{otto}
\end{eqnarray}\vspace{-5mm}\\
All the functions above are defined if and only if the initial path
$\varpi$ is valid for $e$ (i.e., $\occ e{\varpi}$ is defined) and $e$
is well-typed (which implies that all $\tyof {\occ e{\varpi}} \Gamma$
in the definition are defined).\footnote{Note that the definition is
well-founded. This can be seen by analyzing the rule
\Rule{Case\Aa}: the definition of $\Refine {e,t} \Gamma$ and
\Rule{Case\Aa} of Section~\ref{sec:algorules}: the definition of $\Refine {e,t} \Gamma$ and
$\Refine {e,\neg t} \Gamma$ use $\tyof{\occ e{\varpi}}\Gamma$, and
this is defined for all $\varpi$ since the first premisses of
\Rule{Case\Aa} states that $\Gamma\vdash e:\ts_0$ (and this is
\Rule{Case\Aa} states that $\Gamma\vdash e:t_0$ (and this is
possible only if we were able to deduce under the hypothesis
$\Gamma$ the type of every occurrence of $e$.)\vspace{-3mm}}
......@@ -275,6 +211,7 @@ not converge. As an example, consider the (dumb) expression $\tcase
$\Refinef$ yields for $x_1$ a type strictly more precise than the type deduced in the
previous iteration.
\beppe{REWRITE BELOW TILL THE END OF THE SUBSECTION TO STRESS SEMI-DECIDABILITY INSTEAD OF UNCOMPLETENESS}
The solution we adopt here is to bound the number of iterations to some number $n_o$.
From a formal point of view, this means to give up the completeness of the algorithm: $\Refinef$ will be complete (i.e., it will find all solutions) for the deductions of $\Gamma \evdash e t \Gamma'$ of depth at most $n_o$. This is obtained by the following definition of $\Refinef$\vspace{-1mm}
\[
......@@ -330,8 +267,8 @@ We now have all the notions we need for our typing algorithm, which is defined b
{ x\in\dom\Gamma}
\vspace{-2mm}\\
\Infer[Env\Aa]
{ \Gamma\setminus\{e\} \vdashA e : \ts }
{ \Gamma \vdashA e: \Gamma(e) \tsand \ts }
{ \Gamma\setminus\{e\} \vdashA e : t }
{ \Gamma \vdashA e: \Gamma(e) \wedge t }
{ \begin{array}{c}e\in\dom\Gamma \text{ and }\\[-1mm] e \text{ not a variable}\end{array}}
\qquad
\Infer[Const\Aa]
......@@ -340,55 +277,56 @@ We now have all the notions we need for our typing algorithm, which is defined b
{c\not\in\dom\Gamma}
\vspace{-2mm}\\
\Infer[Abs\Aa]
{\Gamma,x:s_i\vdashA e:\ts_i'\\ \ts_i'\leq t_i}
{\Gamma,x:s_i\vdashA e:t_i'\\ t_i'\leq t_i}
{
\Gamma\vdashA\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle\tsfun {\arrow {s_i} {t_i}}_{i\in I}
\Gamma\vdashA\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle\wedge_{i\in I} {\arrow {s_i} {t_i}}
}
{\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e\not\in\dom\Gamma}
\vspace{-2mm}\\
\Infer[App\Aa]
{
\Gamma \vdashA e_1: \ts_1\\
\Gamma \vdashA e_2: \ts_2\\
\ts_1 \leq \arrow \Empty \Any\\
\ts_2 \leq \dom {\ts_1}
\Gamma \vdashA e_1: t_1\\
\Gamma \vdashA e_2: t_2\\
t_1 \leq \arrow \Empty \Any\\
t_2 \leq \dom {t_1}
}
{ \Gamma \vdashA {e_1}{e_2}: \ts_1 \circ \ts_2 }
{ \Gamma \vdashA {e_1}{e_2}: t_1 \circ t_2 }
{ {e_1}{e_2}\not\in\dom\Gamma}
\vspace{-2mm}\\
\Infer[Case\Aa]
{\Gamma\vdashA e:\ts_0\\
{\Gamma\vdashA e:t_0\\
%\makebox{$\begin{array}{l}
% \left\{
% \begin{array}{ll} %\Gamma,
% \Refine + {e,t} \Gamma \vdashA e_1 : \ts_1 & \text{ if } \ts_0 \not\leq \neg t\\
% \ts_1 = \Empty & \text{ otherwise}
% \Refine + {e,t} \Gamma \vdashA e_1 : t_1 & \text{ if } t_0 \not\leq \neg t\\
% t_1 = \Empty & \text{ otherwise}
% \end{array}\right.\\
% \left\{
% \begin{array}{ll} %\Gamma,
% \Refine - {e,t} \Gamma \vdashA e_2 : \ts_2 & \text{ if } \ts_0 \not\leq t\\
% \ts_2 = \Empty & \text{ otherwise}
% \Refine - {e,t} \Gamma \vdashA e_2 : t_2 & \text{ if } t_0 \not\leq t\\
% t_2 = \Empty & \text{ otherwise}
% \end{array}\right.
%\end{array}$}
\Refine {e,t} \Gamma \vdashA e_1 : \ts_1\\
\Refine {e,\neg t} \Gamma \vdashA e_2 : \ts_2}
{\Gamma\vdashA \tcase {e} t {e_1}{e_2}: \ts_1\tsor \ts_2}
\Refine {e,t} \Gamma \vdashA e_1 : t_1\\
\Refine {e,\neg t} \Gamma \vdashA e_2 : t_2}
{\Gamma\vdashA \tcase {e} t {e_1}{e_2}: t_1\vee t_2}
%{\ite {e} t {e_1}{e_2}\not\in\dom\Gamma}
{ \tcase {e} {t\!} {\!e_1\!}{\!e_2}\not\in\dom\Gamma}
\vspace{-2mm} \\
\Infer[Proj\Aa]
{\Gamma \vdashA e:\ts\and \!\!\ts\leq\pair{\Any\!}{\!\Any}}
{\Gamma \vdashA \pi_i e:\bpi_{\mathbf{i}}(\ts)}
{\Gamma \vdashA e:t\and \!\!t\leq\pair{\Any\!}{\!\Any}}
{\Gamma \vdashA \pi_i e:\bpi_{\mathbf{i}}(t)}
{\pi_i e{\not\in}\dom\Gamma}\hfill
\Infer[Pair\Aa]
{\Gamma \vdashA e_1:\ts_1 \and \!\!\Gamma \vdashA e_2:\ts_2}
{\Gamma \vdashA (e_1,e_2):{\ts_1}\tstimes{\ts_2}}%\pair{t_1}{t_2}}
{\Gamma \vdashA e_1:t_1 \and \!\!\Gamma \vdashA e_2:t_2}
{\Gamma \vdashA (e_1,e_2):{t_1}\times{t_2}}%\pair{t_1}{t_2}}
{(e_1,e_2){\not\in}\dom\Gamma}
\end{mathpar}
The side conditions of the rules ensure that the system is syntax
directed, that is, that at most one rule applies when typing a term:
priority is given to \Rule{Eqf\Aa} over all the other rules and to
\Rule{Env\Aa} over all remaining logical rules. Type schemes are
\Rule{Env\Aa} over all remaining logical rules.
\beppe{Modifies till here} Type schemes are
used to account for the type-multiplicity stemming from
$\lambda$-abstractions as shown in particular by rule \Rule{Abs\Aa}
(in what follows we use the word ``type'' also for type schemes). The
......@@ -406,7 +344,7 @@ replaced by the use of type schemes in \Rule{Abs\Aa} and by the rule
expression $e$ by occurrence typing and stored in $\Gamma$ with the
type deduced for $e$ by the logical rules: this is simply obtained by
removing any hypothesis about $e$ from $\Gamma$, so that the deduction
of the type $\ts$ for $e$ cannot but end by a logical rule. Of course
of the type $t$ for $e$ cannot but end by a logical rule. Of course
this does not apply when the expression $e$ is a variable, since
an hypothesis in $\Gamma$ is the only way to deduce the type of a
variable, which is why the algorithm reintroduces the classic rule
......@@ -415,7 +353,7 @@ for variables.
The algorithmic system above is sound with respect to the deductive one of Section~\ref{sec:static}
\begin{theorem}[Soundness]
For every $\Gamma$, $e$, $\ts$, $n_o$, if $\Gamma\vdashA e: \ts$, then $\Gamma \vdash e:t$ for every $t\in\ts$.
For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA e: t$, then $\Gamma \vdash e:t$ for every $t\int$.
\end{theorem}
We were not able to prove full completeness, just a partial form of it. As
anticipated, the problems are twofold: $(i)$ the recursive nature of
......
......@@ -20,7 +20,7 @@
\newif\ifwithcomments
\withcommentstrue
\withcommentsfalse
%\withcommentsfalse
\newif\ifsubmission
\submissiontrue
\submissionfalse
......
......@@ -24,7 +24,7 @@
\definecolor{darkred}{rgb}{0.7,0.4,0.4}
\ifwithcomments
\newcommand{\ignore}[1]{}
\newcommand{\ignore}[1]{{\color{red}\textbf{DELETED:}#1}}
\newcommand{\beppe}[1]{{\bf\color{blue}Beppe: #1}}
\newcommand{\mick}[1]{{\bf\color{gray}Mickael: #1}}
\newcommand{\kim}[1]{{\bf\color{pink}Kim: #1}}
......
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