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

final rediting

parent 3e1f0eb0
......@@ -232,7 +232,17 @@ In other terms, we try to find a fixpoint of $\RefineStep{e,t}$ but we
bound our search to $n_o$ iterations. Since $\RefineStep {e,t}$ is
monotone (w.r.t.\ the subtyping pre-order extended to type environments pointwise), then
every iteration yields a better solution.
While this is unsatisfactory from a formal point of view, in practice
the problem is a very mild one. Divergence may happen only when
refining the type of a function in an application: not only such a
refinement is meaningful only when the function is typed by a union
type, but also we had to build the expression that causes the
divergence in quite an \emph{ad hoc} way which makes divergence even
more unlikely: setting an $n_o$ twice the depth of the syntax tree of
the outermost type case should be enough to capture all realistic
......@@ -415,7 +425,7 @@ For every $\Gamma$, $e$, $t$, if $\Gamma \vdash e:t$ is derivable by a rank-0 ne
\noindent This last result is only of theoretical interest since, in
practice, we expect to have only languages with positive
expressions. This is why for our implementation we use the CDuce
library in which type schemes are absent and functions are typed only
expressions. This is why for our implementation we use the library of CDuce~\cite{BCF03}
in which type schemes are absent and functions are typed only
by intersections of positive arrows. We present the implementation in
Section~\ref{sec:practical}, but before we study some extensions.
\subsection{Adding structured types}
\subsection{Record types}
The previous analysis already covers a large gamut of realistic
cases. For instance, the analysis already handles list data
structures, since products and recursive types can encode them as
right associative nested pairs, as it is done in the language
CDuce~\cite{BCF03} (e.g., $X = \textsf{Nil}\vee(\Int\times X)$ is the
CDuce (e.g., $X = \textsf{Nil}\vee(\Int\times X)$ is the
type of the lists of integers): see Code 8 in Table~\ref{tab:implem} of Section~\ref{sec:practical} for a concrete example. And even more since the presence of
union types makes it possible to type heterogeneous lists whose
content is described by regular expressions on types as proposed
by~\citet{hosoya00regular}. Since the main application of occurrence
typing is to type dynamic languages, then it is worth showing how to
extend our work to records. We use the record types as they are
defined in CDuce and which are obtained by extending types with the
extend our work to records. Although we use the record types as they are
defined in CDuce we cannot do the same for CDuce record expressions
which require non-trivial modifications for occurrence typing,
especially because we want to capture record field extension and field
deletion which current radual typing systems fail to capture. CDuce record types are obtained by extending types with the
following two type constructors:\\[1.4mm]
\centerline{\(\textbf{Types} ~~ t ~ ::= ~ \record{\ell_1=t \ldots \ell_n=t}{t}\alt \Undef\)}\\[1.4mm]
......@@ -30,7 +33,7 @@ distinct). Quasi constant functions are the internal representation of
record types in CDuce. These are not visible to the programmer who can use
only two specific forms of quasi constant functions, open record types and closed record types, provided by the
following syntactic sugar and that form the \emph{record types} of our language\footnote{Note that in the definitions ``$\ldots{}$'' is meta-syntax to denote the presence of other fields while in the open records ``{\large\textbf{..}}'' is the syntax that distinguishes them from closed ones.}
\item $\crecord{\ell_1=t_1, \ldots, \ell_n=t_n}$ for $\record{\ell_1=t_1 \ldots \ell_n=t_n}{\Undef}$ (closed records).
\item $\orecord{\ell_1=t_1, \ldots, \ell_n=t_n}$ for $\record{\ell_1=t_1 \ldots \ell_n=t_n}{\Any \vee \Undef}$ (open records).
......@@ -431,7 +431,7 @@ available online.
\subsubsection*{Contributions} The main contributions of our work can be summarized as follows:
\begin{itemize}[left=0pt .. \parindent]
\begin{itemize}[left=0pt .. \parindent,nosep]
\item We provide a theoretical framwork to refine the type of
expressions occurring in type tests, thus removing the limitations
of current approaches which require both the tests and the refinement
......@@ -10,8 +10,8 @@ In this section we formalize the ideas we outlined in the introduction. We start
\textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty
and that satisfy the following conditions\vspace{-.85mm}
and that satisfy the following conditions
\item (regularity) every term has a finite number of different sub-terms;
\item (contractivity) every infinite branch of a term contains an infinite number of occurrences of the
arrow or product type constructors.\vspace{-1mm}
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