Commit 05e2fd1b authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

more rewriting to move material from the appendix to the main text

parent 6b4f63ef
......@@ -40,7 +40,7 @@ Lemma~\ref{soundness_simple_ts}) and it is thus sound, too. The algorithm of thi
section is not only simpler but, as we discuss in Section~\ref{sec:algoprop},
is also the one that should be used in practice. This is why we preferred to
present it here and relegate the presentation of the system with type schemes to
Appendix~\ref{app:typeschemes}.
\Appendix\ref{app:typeschemes}.
$(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
......@@ -123,7 +123,7 @@ $s$ (since $s$ does not overlap the intersection of the codomains of these arrow
the success of the test cannot depend on these arrows and therefore
the intersection of the domains of these arrows---i.e., the values that would precisely select that set of arrows---can be removed from $\dom t$. The proof
that this type satisfies \eqref{worra} is given in the
Appendix~\ref{app:worra}.
\Appendix\ref{app:worra}.
......@@ -368,7 +368,7 @@ The algorithmic system above is sound with respect to the deductive one of Secti
\begin{theorem}[Soundness]\label{th:algosound}
For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA e: t$, then $\Gamma \vdash e:t$.
\end{theorem}
The proof of this theorem (see Appendix~\ref{sec:proofs_algorithmic_without_ts}) is obtained by
The proof of this theorem (see \Appendix\ref{sec:proofs_algorithmic_without_ts}) is obtained by
defining an algorithmic system $\vdashAts$ that uses type schemes,
that is, which associates each typable term $e$ with a possibly
infinite set of types $\ts$ (in particular a $\lambda$-expression
......@@ -413,7 +413,7 @@ Section~\ref{sec:syntax}, then the algorithmic system of
section~\ref{sec:algorules} is complete. Let say that an expression $e$
is \emph{positive} if it never tests a functional type more precise
than $\Empty\to\Any$ (see
Appendix~\ref{sec:proofs_algorithmic_without_ts} for the formal
\Appendix\ref{sec:proofs_algorithmic_without_ts} for the formal
definition). Then we have:
\begin{theorem}[Completeness for Positive Expressions]
For every type environment $\Gamma$ and \emph{positive} expression $e$, if
......
......@@ -11,12 +11,19 @@ union types it is 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. Although we use the record \emph{types} as they are
defined in CDuce we cannot do the same for CDuce record \emph{expressions}
which require non-trivial modifications for occurrence typing,
especially because we want to capture the typing of record field extension and field
deletion, two widely used record operations that current gradual
typing systems fail to capture.
extend our work to records.
The extension we present in this section is not trivial. Although we use the record \emph{types} as they are
defined in CDuce we cannot do the same for CDuce record
\emph{expressions}. The reasons why we cannot use the record
expressions of CDuce and we have to define and study new one are
twofold. On the one hand we want to capture the typing of record field extension and field
deletion, two operation widely used in dynamic language; on the other
hand we need to have very simple expressions formed by elementary
subexpressions, in order to limit the combinatorics of occurrence
typing. For this reason we build our records one field at a time,
starting from the empty record and adding, updating, or deleting
single fields.
\else%%%%%%%%%%%
Since the main application of occurrence
typing is to type dynamic languages, then it is important to show that our
......@@ -27,7 +34,7 @@ with the records (types and expressions) as they are to be found in the aforemen
CDuce language, where these operations can be precisely typed.
\fi%%%%%
CDuce record \emph{types} can be embedded in our types by adding the
Formally, CDuce record \emph{types} can be embedded in our types by adding the
following two type constructors:\\[1.4mm]
%
\centerline{\(\textbf{Types} \quad t ~ ::= ~ \record{\ell_1=t \ldots \ell_n=t}{t}\alt \Undef\)}\\[1.4mm]
......@@ -63,7 +70,7 @@ field $\ell = t \vee \Undef$%
\fi
For what concerns \emph{expressions}, we cannot use CDuce record expressions
as they are, but we must adapt them to our analysis. In particular, we
as they are, but instead we must adapt them to our analysis. So as anticipated, we
consider records that are built starting from the empty record expression \erecord{} by adding, updating, or removing fields:\svvspace{-0.75mm}
\[
\begin{array}{lrcl}
......@@ -73,7 +80,34 @@ consider records that are built starting from the empty record expression \ereco
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 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 fields 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).
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 fields 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
\iflongversion%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
undefined. They are formally defined as follows (see~\citet{alainthesis} for more details):
\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.\\[2mm]
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\}\\[2mm]
\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
\else%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
undefined
(see \Appendix\ref{app:recop} for the formal definition and~\citet{alainthesis} for more details).
\fi%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
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.
......@@ -107,8 +141,7 @@ To extend occurrence typing to records we add the following values to paths: $\v
\(\recdel e \ell\downarrow r_\ell.\varpi = \occ{e}\varpi\), and
\(\recupd{e_1}\ell{e_2}\downarrow u_\ell^i.\varpi = \occ{e_i}\varpi\)
and add the following rules for the new paths:
\begin{mathpar}\svvspace{-8.7mm}\\
\begin{mathpar}\svvspace{-8.7mm}
\Infer[PSel]
{ \pvdash \Gamma e t \varpi:t'}
{ \pvdash \Gamma e t {\varpi.a_\ell}:\orecord {\ell:t'} }
......@@ -138,6 +171,7 @@ Deriving the algorithm from these rules is then straightforward:\\[1.8mm]
\constr{\varpi.u_\ell^1}{\Gamma,e,t} = \recdel {(\env {\Gamma,e,t} (\varpi))} \ell + \crecord{\ell \eqq \Any}\\[1.8mm]
\end{array}
\)
%% \beppe{Je ne suis absolument pas convaincu par Ext1. Pour moi il devrait donner le field avec le type de $u_\ell^2$ autrement dit pour moi les regles correctes sont:
%% \begin{mathpar}
%% \Infer[PExt1]
......
Typescript and Flow are extensions of JavaScript that allow the programmer to specify in the code type annotations used to statically type-check the program. For instance, the following function definition is valid in both languages
\begin{alltt}\color{darkblue}
function foo(x\textcolor{darkred}{ : number | string}) \{
return (typeof(x) === "number")? x+1 : x.trim(); \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo}
return (typeof(x) === "number")? x+1 : x.trim(); \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo}
\}
\end{alltt}
Apart from the type annotation (in red) of the function parameter, the above is
......@@ -61,7 +61,7 @@ exactly what the \emph{intersection type}
states (intuitively, an expression has an intersection of types, noted \code{\&}, if and only if it has all the types of the intersection) and corresponds in Flow to declaring \code{foo} as follows:
\begin{alltt}\color{darkblue}
var foo : \textcolor{darkred}{(number => number) & (string => string)} = x => \{
return (typeof(x) === "number")? x+1 : x.trim(); \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo2}
return (typeof(x) === "number")? x+1 : x.trim(); \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo2}
\}
\end{alltt}
For what concerns negation types, they are pervasive in the occurrence
......
......@@ -61,10 +61,9 @@ by~\citet{Frisch2008}
\iflongversion
and detailed description of the algorithm to
decide this relation can be found in~\cite{Cas15}. For the reader's
convenince we succintly recall the definition of the subtyping relations in the next subsection.
This subsection can be skipped at first reading and the reader can
jump directly to Subsection~\ref{sec:syntax}, since to understand
what will follow
convenience we succintly recall the definition of the subtyping
relation in the next subsection but it is possible to skip this subsection at first reading andjump directly to Subsection~\ref{sec:syntax}, since to understand
the rest of the paper
\else
to which the reader may refer for the formal
definition (we recall it in \Appendix\ref{sec:subtyping} for the
......@@ -90,9 +89,8 @@ of functions that diverge on every argument). Type connectives
corresponding set-theoretic operators (e.g.,~$s\vee t$ is the
union of the values of the two types). We use $\simeq$ to denote the
symmetric closure of $\leq$: thus $s\simeq t$ (read, $s$ is equivalent to $t$) means that $s$ and $t$ denote the same set of values and, as such, they are semantically the same type.
\iflongversion
The above is formalized as follows.
All the above is formalized as follows.
\subsection{Subtyping}
\label{sec:subtyping}
\input{subtyping}
......@@ -100,7 +98,7 @@ The above is formalized as follows.
\subsection{Syntax}\label{sec:syntax}
The expressions $e$ and values $v$ of our language are inductively generated by the following grammars:\svvspace{-1mm}
The expressions $e$ and values $v$ of our language are inductively generated by the following grammars:\svvspace{-2mm}
\begin{equation}\label{expressions}
\begin{array}{lrclr}
\textbf{Expr} &e &::=& c\alt x\alt ee\alt\lambda^{\wedge_{i\in I}s_i\to t_i} x.e\alt \pi_j e\alt(e,e)\alt\tcase{e}{t}{e}{e}\\[.3mm]
......@@ -109,8 +107,12 @@ The expressions $e$ and values $v$ of our language are inductively generated by
\end{equation}
for $j=1,2$. In~\eqref{expressions}, $c$ ranges over constants
(e.g., \texttt{true}, \texttt{false}, \texttt{1}, \texttt{2},
...) which are values of basic types (we use $\basic{c}$ to denote the
basic type of the constant $c$); $x$ ranges over variables; $(e,e)$
...) which are values of basic types%
\ifelsevierstyle\else
\ (we use $\basic{c}$ to denote the
basic type of the constant $c$)%
\fi%%%%%%5
; $x$ ranges over variables; $(e,e)$
denotes pairs and $\pi_i e$ their projections; $\tcase{e}{t}{e_1}{e_2}$
denotes the type-case expression that evaluates either $e_1$ or $e_2$
according to whether the value returned by $e$ (if any) is of type $t$
......@@ -125,13 +127,20 @@ typed if $\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ has type $s_i\to
t_i$ for all $i\in I$. Every value is associated to a most specific type (mst): the mst of $c$ is $\basic c$; the mst of
$\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ is $\wedge_{i\in I}s_i\to t_i$; and, inductively,
the mst of a pair of values is the product of the mst's of the
values. We write $v\in t$ if the most specific type of $v$ is a subtype of $t$ (see \Appendix\ref{app:typeschemes} for the formal definition of $v\in t$ which deals with some corner cases for negated arrow types).
values. Finally, we write $v\in t$ if and only if the intersection of
$\neg t$ and the most specific type of $v$ is empty.\footnote{This definition may look
complicated but it is necessary to handle some corner cases for
negated arrow types (cf.\ rule \Rule{Abs-} in
Section~\ref{sec:static}). For instance, it states that $\lambda^{\Int{\to}\Int}.x\in
(\Int{\to}\Int)\wedge\neg(\Bool{\to}\Int)$
See \Appendix\ref{app:typeschemes} for an alternative equivalent formal definition of $v\in t$.}
\subsection{Dynamic semantics}\label{sec:opsem}
The dynamic semantics is defined as a classic left-to-right call-by-value reduction for a $\lambda$-calculus with pairs, enriched with specific rules for type-cases. We have the following notions of reduction:\svvspace{-1.2mm}
The dynamic semantics is defined as a classic left-to-right
call-by-value weak reduction for a $\lambda$-calculus with pairs, enriched with specific rules for type-cases. We have the following notions of reduction:\svvspace{-1.2mm}
\[
\begin{array}{rcll}
(\lambda^{\wedge_{i\in I}s_i\to t_i} x.e)\,v &\reduces& e\subst x v\\[-.4mm]
......
......@@ -36,7 +36,7 @@
%\documentclass[sigplan,10pt,review,anonymous]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[hidelinks]{hyperref}
\newif\ifelsevierstyle
\elsevierstyletrue
\newif\ifwithcomments
......@@ -261,14 +261,16 @@ The authors thank Paul-André Melliès for his help on type ranking.
\newpage
\iflongversion\else
\section{Record types operators}\label{app:recop}
\input{record_operations}
\fi%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}
\newpage
\section{A more precise rule for inference}\label{app:optimize}
\input{optimize}
\newpage
\section{A Roadmap to Polymorphic Types}
......
\newcommand{\negspace}{\svvspace{-.5mm}}
As we explained in the introduction, both TypeScript and Flow deduce the type
\code{(number$\vee$string) $\to$ (number$\vee$string)} for the first definition of the function \code{foo} in~\eqref{foo}, and the more precise type\svvspace{-3pt}
As we explained in the introduction, both TypeScript and Flow deduce for the first definition of the function \code{foo} in~\eqref{foo} the type
\code{(number$\vee$string) $\to$ (number$\vee$string)}, while the more precise type\svvspace{-3pt}
\begin{equation}\label{tyinter}
\code{(number$\to$number)$\,\wedge\,$(string$\to$string)}\svvspace{-3pt}
\end{equation}
......
......@@ -3,7 +3,7 @@ Subtyping is defined by giving a set-theoretic interpretation of the
types of Definition~\ref{def:types} into a suitable domain $\Domain$:
\begin{definition}[Interpretation domain~\cite{Frisch2008}]\label{def:interpretation}
The \emph{interpretation domain} $ \Domain $ is the set of finite terms $ d $
produced inductively by the following grammar
produced inductively by the following grammar\vspace{-2mm}
\begin{align*}
d & \Coloneqq c \mid (d, d) \mid \Set{(d, \domega), \dots, (d, \domega)}
\\
......@@ -12,7 +12,6 @@ produced inductively by the following grammar
where $ c $ ranges over the set $ \Constants $ of constants
and where $ \Omega $ is such that $ \Omega \notin \Domain $.
\end{definition}
The elements of $ \Domain $ correspond, intuitively,
to (denotations of) the results of the evaluation of expressions.
In particular, in a higher-order language,
......@@ -42,8 +41,15 @@ so that it satisfies the following equalities,
where $ \Pf $ denotes the restriction of the powerset to finite
subsets and $ \ConstantsInBasicType{}$ denotes the function
that assigns to each basic type the set of constants of that type, so
that for every constant $c$ we have $ c\in \ConstantsInBasicType(\basic {c})$ ($\basic c$ is
that for every constant $c$ we have $
c\in \ConstantsInBasicType(\basic {c})$
\ifelsevierstyle
(we use $\basic{c}$ to denote the
basic type of the constant $c$):
\else
($\basic c$ is
defined in Section~\ref{sec:syntax}):
\fi
\begin{align*}
\TypeInter{\Empty} & = \emptyset&
\TypeInter{t_1 \lor t_2} & = \TypeInter{t_1} \cup \TypeInter{t_2} &
......
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