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

Some space savings

parent 977e2796
......@@ -51,25 +51,8 @@ For what concerns expressions, we adapt CDuce records to our analysis. In partic
in particular $\recdel e \ell$ deletes the field $\ell$ from $e$, $\recupd e \ell e'$ adds the field $\ell=e'$ to the record $e$ (deleting any existing $\ell$ field), while $e.\ell$ is field selection with the reduction:
\(\erecord{...,\ell=e,...}.\ell\ \reduces\ e\).
To define record type subtyping and record expression type inference we need the following operators on record types (refer to~\citet{alainthesis} for more details):
\vspace{-2mm}
\begingroup
\allowdisplaybreaks
\begin{eqnarray}
\proj \ell t & = & \left\{\begin{array}{ll}\min \{ u \alt t\leq \orecord{\ell=u}\} &\text{if } t \leq \orecord{\ell = \Any}\\ \text{undefined}&\text{otherwise}\end{array}\right.\\
t_1 + t_2 & = & \min\left\{
u \quad\bigg|\quad \forall \ell \in \Labels.\left\{\begin{array}{ll}
\proj \ell u \geq \proj \ell {t_2} &\text{ if } \proj \ell {t_2} \leq \neg \Undef\\
\proj \ell u \geq \proj \ell {t_1} \vee (\proj \ell {t_2} \setminus \Undef) &\text{ otherwise}
\end{array}\right\}
\right\}\\
\recdel t \ell & = & \min \left\{ u \quad\bigg|\quad \forall \ell' \in \Labels. \left\{\begin{array}{ll}
\proj {\ell'} u \geq \Undef &\text{ if }\ell' = \ell\\
\proj {\ell'} u \geq \proj {\ell'} t &\text{ otherwise}
\end{array}\right\}\right\}
\end{eqnarray}
\endgroup
To define record type subtyping and record expression type inference we need three operators on record types: $\proj \ell t$ which returns the type of the field $\ell$ in the record type $t$, $t_1+t_2$ which returns the record type formed by all the field in $t_2$ and those in $t_1$ that are not in $t_2$, and $\recdel t\ell$ which returns the type $t$ in which the field $\ell$ is undefined (see Appendix~\ref{app:recop} for the formal definition and~\citet{alainthesis} for more details).
%
Then two record types $t_1$ and $t_2$ are in subtyping relation, $t_1 \leq t_2$, if and only if for all $\ell \in \Labels$ we have $\proj \ell {t_1} \leq \proj \ell {t_2}$. In particular $\orecord{\!\!}$ is the largest record type.
Expressions are then typed by the following rules (already in algorithmic form).
......
......@@ -410,9 +410,13 @@ by retyping the expression without that assumption (see rule
\Rule{Env\Aa} in Section~\ref{sec:algorules}).
\subsubsection*{Outline} In Section~\ref{sec:language} we formalize the
ideas presented in this introduction: we define the types and
\iflongversion
\subsubsection*{Outline}
\else
\subsubsection*{Outline and Contributions}
\fi
In Section~\ref{sec:language} we formalize the
ideas we just presented: we define the types and
expressions of our system, their dynamic semantics and a type system that
implements occurrence typing together with the algorithms that decide
whether an expression is well typed or not. Section~\ref{sec:extensions} extends our formalism to record
......@@ -421,8 +425,11 @@ arrow types for functions and a static analysis to reduce the number
of casts inserted by a compiler of a gradually-typed
language. Practical aspects are discussed in
Section~\ref{sec:practical} where we give several paradigmatic examples of code typed by our prototype implementation, that can be interactively tested at \url{https://occtyping.github.io/}. Section~\ref{sec:related} presents
related work. A discussion of future work concludes this
related work.
\iflongversion
A discussion of future work concludes this
presentation.
\fi
%
For space reasons several technical definitions and all the proofs are
omitted from this presentation and can be found in the appendix
......@@ -432,7 +439,10 @@ joint to the submission.
available online.
\fi
\subsubsection*{Contributions} The main contributions of our work can be summarized as follows:
\iflongversion
\subsubsection*{Contributions}
\fi
The main contributions of our work can be summarized as follows:
\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
......
\newlength{\sk}
\setlength{\sk}{-1.9pt}
\iflongversion
In this section we formalize the ideas we outlined in the introduction. We start by the definition of types followed by the language and its reduction semantics. The static semantics is the core of our work: we first present a declarative type system that deduces (possibly many) types for well-typed expressions and then the algorithms to decide whether an expression is well typed or not.
\fi
\subsection{Types}
......@@ -147,7 +149,8 @@ core and the use of subtyping, given by the following typing rules:\vspace{-1mm}
% \Gamma \cvdash - e t e_2:t'}
% {\Gamma\vdash \ite {e} t {e_1}{e_2}: t'}
% { }
\vspace{-2mm} \\
\end{mathpar}
\begin{mathpar}\vspace{-4mm}\\
\Infer[Sel]
{\Gamma \vdash e:\pair{t_1}{t_2}}
{\Gamma \vdash \pi_i e:t_i}
......@@ -250,7 +253,8 @@ expression whose type environment contains an empty assumption:
\end{mathpar}
Once more, this kind of deduction was already present in the system
by~\citet{Frisch2008} to type full fledged overloaded functions,
though it was embedded in the typing rule for the type-case. Here we
though it was embedded in the typing rule for the type-case.\pagebreak
Here we
need the rule \Rule{Efq}, which is more general, to ensure the
property of subject reduction.
%\beppe{Example?}
......
......@@ -298,6 +298,12 @@ The authors thank Paul-André Melliès for his help on type ranking.
\label{sec:proofs}
\input{proofs}
\section{Record types operators}\label{app:recop}
\input{record_operations}
\section{A more precise rule for inference}\label{app:optimize}
\input{optimize}
......
\begingroup
\allowdisplaybreaks
\begin{eqnarray}
\proj \ell t & = & \left\{\begin{array}{ll}\min \{ u \alt t\leq \orecord{\ell=u}\} &\text{if } t \leq \orecord{\ell = \Any}\\ \text{undefined}&\text{otherwise}\end{array}\right.\\
t_1 + t_2 & = & \min\left\{
u \quad\bigg|\quad \forall \ell \in \Labels.\left\{\begin{array}{ll}
\proj \ell u \geq \proj \ell {t_2} &\text{ if } \proj \ell {t_2} \leq \neg \Undef\\
\proj \ell u \geq \proj \ell {t_1} \vee (\proj \ell {t_2} \setminus \Undef) &\text{ otherwise}
\end{array}\right\}
\right\}\\
\recdel t \ell & = & \min \left\{ u \quad\bigg|\quad \forall \ell' \in \Labels. \left\{\begin{array}{ll}
\proj {\ell'} u \geq \Undef &\text{ if }\ell' = \ell\\
\proj {\ell'} u \geq \proj {\ell'} t &\text{ otherwise}
\end{array}\right\}\right\}
\end{eqnarray}
\endgroup
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