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

Added comparison with Kent

parent e16176c4
......@@ -113,7 +113,7 @@ furthermore $t\leq\Empty\to\Any$, then $t \simeq \bigvee_{i\in
t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n') \not\simeq \Empty$ for all
$i$ in $I$. For such a $t$ and any type $s$ then we have:\svvspace{-1.0mm}
%
\begin{equation}
\begin{equation}\label{worralgo}
\worra t s = \dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P\subseteq P_i\alt s\leq \bigvee_{p \in P} \neg t_p\}}\left(\bigvee_{p \in P} \neg s_p\right) \right)\svvspace{-1.0mm}
\end{equation}
The formula considers only the positive arrows of each summand that
......
......@@ -149,19 +149,75 @@ different language designs and arguing about their usefulness.
\rev{%%%
Highly related to our work is the Andrew M.\ Kent PhD
dissertation~\cite{kent19phd} in particular Chapter 5 whose title is
``A set-theoretic foundation for occurrence typing''. In that chapter
Kent endows the logical techniques of Typed Racket~\cite{THF10} with
the set-theoretic types of semantic subtyping~\cite{Frisch2008}. The
expressivity of set-theoretic types is used
...
%
dissertation~\cite{kent19phd} in particular its Chapter 5 whose title
is ``A set-theoretic foundation for occurrence typing''. In that
chapter Kent endows the logical techniques of Typed
Racket~\cite{THF10} with the set-theoretic types of semantic
subtyping~\cite{Frisch2008}. Kent's work builds on the approach
developed for Typed Racket. This, as recalled above, enriches the
types of the expressions to track under which hypotheses an expression
returns false or not (it considers every non false value to be
``truthy''). This tracking is performed by recording in the type of
the expression two logical propositions that hold when the expression
evaluates to false or not, respectively. The work in~\citet[Chapter
5]{kent19phd} uses set-theoretic types to express type predicates (a
predicate that holds only for a type $t$ has type
$p:(t\to\texttt{True})\land(\neg t\to\texttt{False})$) as well as to
express in a more compact (and, sometimes, more precise) way the types
of several built-in Typed Racket functions. It also uses the
properties of set-theoretic types to deduce the logical types (i.e.,
the propositions that hold when an expressions produces \texttt{false}
or not) of arguments of function applications. To do that it defines
a type operator called \emph{function application inversion}, that
determines the largest subset of the domain of a function for which an
application yield a result of a given type $t$, and then uses it for
when the type $t$ is either \texttt{False} or \texttt{$\lnot$False} so
as to determine the logical type of the argument. For instance, this
operator can be used to deduce that if the application \texttt{boolean?\,x}
yields false, then \texttt{x${\in}\neg$Bool} holds true. The definition
of our \emph{worra} operator that we gave in equation~\eqref{worra} is, in
its inspiration, the same as Kent's \emph{function application inversion}
operator (more precisely, as the operator \textsf{pred} Kent defines in Figure
5.7 of his dissertation), even though the two operators were defined independently from
each other. The exact definitions however are slightly different, since
the algorithm given in~\citet[Figure 5.2]{kent19phd}
for \emph{function application inversion} works only for functions
whose type is an intersection of arrows, whereas our definition
in~\eqref{worralgo} of \emph{worra} works for any function, in
particular, for functions that have a union type, too. The main
difference of Kent's approach with respect to ours is that, since it
builds on the logical propositions approach, then it focus the use of
set-theoretic types and of the worra (or application inversion)
operator to determine when an expression yields a result of
type \texttt{False} or \texttt{$\lnot$False}. We have instead a more
holistic approach since not only our analysis strives to infer type
information by analyzing all types of results (and not
just \texttt{False} or \texttt{$\lnot$False}), but also it tries to
perform this analysis for all possible expressions (and not just for a
restricted set of expressions). So, for instance, in Kent's approach
the analysis of an application \texttt{f\,x} refines the properties of
the argument \texttt{x} but not of the function \texttt{f} (as our
approach does); and when such an application is the argument of a type
test, such as in \texttt{number?\,(f\,x)}, then it is no longer possible
to refine the information on the argument \texttt{x}. The latter is
not is a flaw of the approach but a design choice: as we explain later
on, the Type Racket approach non only focus on the inference of two logical
propositions according to the truthy or false value of an expression,
but it does it only for a selected set of \emph{pure} expressions of
the language, to cope with the possible presence of side effects (and
applications do not belong to this set since they can be be impure).
Finally, Kent's approach inherits all the advantages and
disadvantages that the logical propositions approach has with respect
to ours (e.g., flow sensitive analysis vs.\ user defined type
predicates) that we already discussed at the beginning of this
section.
}%%%rev
\rev{HERE STRESS THAT THE WORK ON SOLVERS IS IN THE SAME VEIN AS THE
WORK OF TYPED RACKET THAT TRACKS FOR EXPRESSIONS WHEN THEY RETURN
FALSE AND WHEN NOT.
}
Another direction of research related to ours is the one of semantic
types. In particular, several attempts have been made recently to map
types to first order formul\ae. In that setting, subtyping between
......
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