Commit 247d4e21 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

more rewording

parent c90a109b
......@@ -289,9 +289,9 @@ Ergo $t_1\setminus (t_2^+\to
Let us see all this on our example \eqref{exptre}, in particular, by showing how this technique deduces that the type of $x_1$ in the positive branch is (a subtype of) $\Int{\vee}\String\to\Int$.
Take the static type of $x_1$, that is $(\Int{\vee}\String\to\Int)\vee(\Bool{\vee}\String\to\Bool)$ and intersect it with
$(t_2^+\to \neg t)$, that is, $\String\to\neg\Int$. Since intersection distributes over unions we
obtain
obtain\vspace{-1mm}
%
\[((\Int{\vee}\String{\to}\Int)\wedge\neg(\String{\to}\neg\Int))\vee((\Bool{\vee}\String{\to}\Bool)\wedge\neg(\String{\to}\neg\Int))\]
\[((\Int{\vee}\String{\to}\Int)\wedge\neg(\String{\to}\neg\Int))\vee((\Bool{\vee}\String{\to}\Bool)\wedge\neg(\String{\to}\neg\Int))\vspace{-1mm}\]
%
and since
$(\Bool{\vee}\String{\to}\Bool)\wedge\neg(\String{\to}\neg\Int)$ is empty
......@@ -310,9 +310,9 @@ This is essentially what we formalize in Section~\ref{sec:language}, in the type
In the previous section we outlined the main ideas of our approach to occurrence typing. However, devil is in the details. So the formalization we give in Section~\ref{sec:language} is not so smooth as we just outlined: we must introduce several auxiliary definitions to handle some corner cases. This section presents by tiny examples the main technical difficulties we had to overcome and the definitions we introduced to handle them. As such it provides a kind of road-map for the technicalities of Section~\ref{sec:language}.
\paragraph{Typing occurrences} As it should be clear by now, not only variables but also generic expressions are given different types in the ``then'' and ``else'' branches of type tests. For instance, in \eqref{two} the expression $x_1x_2$ has type \Int{} in the positive branch and type \Bool{} in the negative one. In this specific case it is possible to deduce these typings from the refined types of the variables (in particular, thanks to the fact that $x_2$ has type \Int{} the positive branch and \Bool{} in the negative one), but this is not possible in general. For instance, consider $x_1:\Int\to(\Int\vee\Bool)$, $x_2:\Int$, and the expression\vspace{-.9mm}
\paragraph{Typing occurrences} As it should be clear by now, not only variables but also generic expressions are given different types in the ``then'' and ``else'' branches of type tests. For instance, in \eqref{two} the expression $x_1x_2$ has type \Int{} in the positive branch and type \Bool{} in the negative one. In this specific case it is possible to deduce these typings from the refined types of the variables (in particular, thanks to the fact that $x_2$ has type \Int{} the positive branch and \Bool{} in the negative one), but this is not possible in general. For instance, consider $x_1:\Int\to(\Int\vee\Bool)$, $x_2:\Int$, and the expression\vspace{-1mm}
\begin{equation}\label{twobis}
\ifty{x_1x_2}{\Int}{...x_1x_2...}{...x_1x_2...}\vspace{-.9mm}
\ifty{x_1x_2}{\Int}{...x_1x_2...}{...x_1x_2...}\vspace{-1mm}
\end{equation}
It is not possible to specialize the type of the variables in the
branches. Nevertheless, we want to be able to deduce that $x_1x_2$ has
......
%% For double-blind review submission, w/o CCS and ACM Reference (max submission space)
%\documentclass[acmsmall,review,anonymous]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
\documentclass[acmsmall,review,anonymous]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
%% For double-blind review submission, w/ CCS and ACM Reference
%\documentclass[acmsmall,review,anonymous]{acmart}\settopmatter{printfolios=true}
%% For single-blind review submission, w/o CCS and ACM Reference (max submission space)
......@@ -8,7 +8,7 @@
%\documentclass[acmsmall,review]{acmart}\settopmatter{printfolios=true}
%% For final camera-ready submission, w/ required CCS and ACM Reference
%% \documentclass[acmsmall,screen]{acmart}\settopmatter{}
\documentclass[acmsmall,screen,nonacm]{acmart}%\settopmatter{printacmref=false}\pagestyle{plain} % removes running headers
%%%%%%%%\documentclass[acmsmall,screen,nonacm]{acmart}%\settopmatter{printacmref=false}\pagestyle{plain} % removes running headers
%
% The following are the instructions for PLDI 2020 submission
%
......@@ -20,7 +20,7 @@
\newif\ifwithcomments
\withcommentstrue
%\withcommentsfalse
\withcommentsfalse
\newif\ifsubmission
\submissiontrue
\submissionfalse
......
We have implemented a simplified version of the algorithm presented in
Section~\ref{ssec:algorithm} that does
not make use of type schemes and is, therefore, incomplete w.r.t. the
system of Section~\ref{sec:static}. In particular, as we
explained in Section~\ref{ssec:algorithm}, \beppe{did we?} in the absence of type
schemes it is not always possible to prove that $\forall v, \forall t,
v \in t \text{~or~} v \not\in \lnot t$. Since this property ceases
to hold only for $\lambda$-abstractions, then not using type schemes
yields less precise typing only for tests $\ifty{e}t{e_1}{e_2}$ where $e$
has a functional type, that is, the value tested will be a $\lambda$-abstraction.
This seems like a reasonable compromise between the
complexity of an implementation involving type schemes and the programs
we want to type-check in practice. Indeed, if we restrict the language
so that the only functional type $t$ allowed in a test $\ifty{e}t{e_1}{e_2}$
is $\Empty{\to}\Any$---i.e., if we allow to check whether a value is a
function but not whether it has a specific function type (\emph{cf.}, Footnote~\ref{foo:typecase})---, then our
implementation becomes complete (see Corollary~\ref{app:completeness} in the appendix for a formal proof).
Our implementation is written in OCaml and uses CDuce as a library to
We have implemented the algorithmic system $\vdashA$. Our implementation is written in OCaml and uses CDuce as a library to
provide the semantic subtyping machinery. Besides a type-checking
algorithm defined on the base language, our implementation supports
record types (Section \ref{ssec:struct}) and the refinement of function types
......
......@@ -28,7 +28,7 @@ in the ``then'' and ``else'' branches of a test. One area where their
work goes further than ours is that the type information also flows
outside of the tests to the surrounding context. In contrast, our type
system only refines the type of variables strictly in the branches of a
test. However, using semantic-subtyping as a foundation we believe our
test. However, using semantic subtyping as a foundation we believe our
approach has several merits over theirs. First, in our case, type
predicates are not built-in. A user may define any type predicate she
wishes by using an overloaded function, as we have shown in
......@@ -45,10 +45,10 @@ the subtyping rule presented in \cite{THF10} is unable to deduce that
$(\texttt{number}\times(\texttt{number}\cup\texttt{bool}))\cup
(\texttt{bool}\times (\texttt{number}\cup\texttt{bool}))$ is a subtype of
(and actually equal to) $((\texttt{number}\cup\texttt{bool})\times\texttt{number})\cup
((\texttt{number}\cup\texttt{bool})\times\texttt{bool})$. For record
((\texttt{number}\cup\texttt{bool})\times\texttt{bool})$ (and likewise for other type constructors). For record
types, we also type precisely the deletion of labels, which, as far as
we know other systems cannot do. On the other hand, the propagation of
logical properties defined in \cite{THF10} is a powerfull tool, that
we know no other system can do. On the other hand, the propagation of
logical properties defined in \cite{THF10} is a powerful tool, that
can be extended to cope with sophisticated language features such as
the multi-method dispatch of the Closure language \cite{Bonn16}.
......@@ -74,38 +74,37 @@ form of dependent typing (and in particular they provide an
implementation supporting bitvector and linear arithmetic theories).
While static invariants that can be enforced by such logic go well
beyond what can be proven by a static ``non dependent'' type
system, it does so at the cost of having the programmer write logical
system as ours, they do so at the cost of having the programmer write logical
annotations (to help the external provers). While this work provides
richer logical statements than those by~\citet{THF10}, it still remains
restricted to refining the types of variables, and not of arbitrary
constructs such as pairs, records or recursive types. The idea to
defer the subtyping check to an SMT solver is not new.
The work of \cite{Bierman10}, presents Dminor, a data oriented
language featuring a {\tt SELECT}-like constructs over
collections. Its typesystems combines semantic subtyping and
refinement types. Syntactic types are mapped to first order formula
The work of \citet{Bierman10} presents Dminor, a data-oriented
language featuring a {\tt SELECT}-like construct over
collections. Its type systems combine semantic subtyping and
refinement types. Syntactic types are mapped to first order formulæ
and subtyping is expressed as logicial implication. An SMT-solver is
then used to (try to) prove the logicial implication. The refinement
types they present go well beyond what can be expressed with the set-theoretic
types we use (as they allow almost any pure expression to occur in
types). However, the system foregoes any notion of completeness
types). However, the system forgoes any notion of completeness
(since satisfiability of first order logic is undecidable) and the
subtyping algorithm is largely dependent on the subtle behaviour of
the SMT solver (which may timeout our give an incorrect model that
the SMT solver (which may timeout or give an incorrect model that
cannot be used as a counter-example to explain the type-error).
As with our work, the typing rule for the {\tt if~$e$ then $e_1$ else
$e_2$} construct
of Dminor refines the type of each branch by remembering that $e$
(resp. $\lnot e$) is true in $e_1$ (resp. $e_2$) but this information
is not propagated to the outer context.
A similar approach is taken in \cite{Chugh12}, and extended to so
called nested refinement types. In these types, an arrow type may
A similar approach is taken in \cite{Chugh12}, and extended to so-called nested refinement types. In these types, an arrow type may
appear in a logical formula (where previous work only allowed formulae
between ``base types''). This is done in the context of a dynamic
on ``base types''). This is done in the context of a dynamic
language and their approach is extended with polymorphism, dynamic
dispatch and record types. As in \cite{Bierman10}, the refined typed
dispatch and record types. As in \cite{Bierman10}, the refined type
of a conditional does not flow to the outer context and the same
provision to using an SMT solver apply.
caveats to using an SMT solver apply.
\citet{Cha2017} present the design and implementation of Flow by formalizing a relevant
......
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