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

final space revision reintroduced footnote structural rules

parent e66e0e83
......@@ -10,15 +10,13 @@ auxiliary deduction system for paths.
$(i)$. Multiple types have two distinct origins each requiring a distinct
technical solution. The first origin is the presence of
%structural
structural
rules
\iffalse
\footnote{\label{fo:rules}In logic, logical rules refer to a
particular connective (here, a type constructor, that is, either
$\to$, or $\times$, or $b$), while identity rules (e.g., axioms and
cuts) and structural rules (e.g., weakening and contraction) do
not.}
\fi
not.\vspace{-3.3mm}}
such as \Rule{Subs} and \Rule{Inter}. We handle this presence
in the classic way: we define an algorithmic system that tracks the
miminum type of an expression; this system is obtained from the
......@@ -77,18 +75,20 @@ things get 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 and needs the operators $\dom{}$ and $\circ$ we informally described in Section~\ref{sec:ideas} where we also introduced the operator $\worra{}{}$. These three operators are used by our algorithm and formally defined as:\vspace{-2mm}
its domain and the type of the application is more complicated and needs the operators $\dom{}$ and $\circ$ we informally described in Section~\ref{sec:ideas} where we also introduced the operator $\worra{}{}$. These three operators are used by our algorithm and formally defined as:\vspace{-3.5mm}
\begin{eqnarray}
\dom t & = & \max \{ u \alt t\leq u\to \Any\}
\\[-1mm]
\apply t s & = &\,\min \{ u \alt t\leq s\to u\}
\\[-1mm]
\worra t s & = &\,\min\{u \alt t\circ(\dom t\setminus u)\leq \neg s\}\label{worra}
\end{eqnarray}\vspace{-3.75mm}\\
%In short, $\dom t$ is the largest domain of any single arrow that
%subsumes $t$, $\apply t s$ is the smallest domain of an arrow type
%that subsumes $t$ and has domain $s$ and $\worra t s$ was explained
%before.
\end{eqnarray}\vspace{-4.7mm}\\
\iflongversion%
In short, $\dom t$ is the largest domain of any single arrow that
subsumes $t$, $\apply t s$ is the smallest domain of an arrow type
that subsumes $t$ and has domain $s$ and $\worra t s$ was explained
before.
\fi%
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
......@@ -150,7 +150,9 @@ We start by defining the algorithm for each single occurrence, that is for the d
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
in the definition are defined).%
\iflongversion%
\footnote{Note that the definition is
well-founded. This can be seen by analyzing the rule
\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
......@@ -158,7 +160,7 @@ in the definition are defined).\footnote{Note that the definition 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}}
\fi
Each case of the definition of the $\constrf$ function corresponds to the
application of a logical rule
\iflongversion
......
......@@ -23,7 +23,7 @@ and both are issues that the system by~\citet{THF10} can handle. We think that i
to reuse some of their ideas to perform an information flow analysis on top of
our system to remove these limitations.
%
{\color{red}
\iflongversion%
Some of the exensions we hinted to in Section~\ref{sec:practical}
warrant a formal treatment. In particular, the rule [{\sc OverApp}]
only detects the application of an overloaded function once, when
......@@ -33,7 +33,8 @@ process whilst type-checking the inferred arrows (i.e., we would
enrich $\psi$ while using it to find the various arrow types of the
lambda abstraction). Clearly, if untamed, such a process may never
reach a fix point. Studying whether this iterative refining can be
made to converge and, foremost, whether it is of use in practice is among our objectives.}
made to converge and, foremost, whether it is of use in practice is among our objectives.
\fi%
But the real challenges that lie ahead are the handling of side
effects and the addition of polymorphic types. Our analysis works in a
......
......@@ -149,7 +149,7 @@ $\code{number} \land \dyn\simeq \code{number}$ is
not an option, since it would force us to choose between having
the gradual guarantee or having, say,
$\code{number} \land \code{string}$ be more precise than
$\code{number} \land \dyn$.}%
$\code{number} \land \dyn$.\vspace{-2mm}}%
Hence the need for the second part of
Rule~\textsc{[AbsInf+]}: the maximal interpretation of $\code{number} \land \dyn$
is $\code{number}$, and it is clear that, if $\code x$ is given type \code{number},
......
......@@ -435,13 +435,13 @@ $\pair{t'}\Any$ (respectively, $\pair\Any{t'}$).
This concludes the presentation of our type system, which satisfies
the property of safety, deduced, as customary, from the properties
of progress and subject reduction (\emph{cf.} Appendix~\ref{app:soundness}).
of progress and subject reduction (\emph{cf.} Appendix~\ref{app:soundness}).\vspace{-1.5mm}
\begin{theorem}[type safety]
For every expression $e$ such that $\varnothing\vdash e:t$ either $e$
diverges or there
exists a value $v$ of type $t$ such that $e\reduces^* v$.
\end{theorem}
\vspace{-2mm}
......
......@@ -68,8 +68,8 @@ code goes, but we see that the overloaded type precisely captures all
possible cases. Again we use a generalized version of the
\texttt{or\_} connective that accepts and treats any value that is not
\texttt{true} as \texttt{false} and again, we could easily restrict the
domain to \Bool{} if desired.
domain to \Bool{} if desired.\\
\indent
To showcase the power of our type system, and in particular of
the ``$\worra{}{}$''
type operator, we define \texttt{and\_} (Code~6) using De Morgan's
......
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