Commit 26c97a4a authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

more on review

parent a598941f
......@@ -148,14 +148,12 @@ 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 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
Highly related to our work is Andrew M.\ Kent's PhD.\
dissertation~\cite{kent19phd}, in particular its Chapter 5 whose title
is ``A set-theoretic foundation for occurrence typing'' where he endows the logical techniques of~\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
developed for Typed Racket that, as recalled above, consists in enriching the
types of the expressions with information 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
......@@ -170,27 +168,27 @@ 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
application yields a result of a given type $t$, and then uses it for
the special cases 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
yields false, then the logical proposition \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
its spirit, the same as Kent's \emph{function application inversion}
operator (more precisely, the same 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
of worra, given in~\eqref{worralgo}, 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
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
......
......@@ -102,7 +102,7 @@ The thesis is available at https://pnwamk.github.io/docs/dissertation.pdf
work on reimplementing semantic subtyping, but we did not know about
his dissertation and in particular of the work in chapter 5, which
is a pity in light of the topic and of the fact that it heavily
relies on semantic subtyping. Probably another bad consequence of
relies on semantic subtyping. Probably a consequence of
the pandemic.
Of course, the new version of the related work section includes now a
......@@ -114,7 +114,7 @@ disclosed the fact that he is Kent's supervisor to signal a small
error that we think we may have spotted in the dissertation: in Figure
5.2, describing the function application inversion algorithm we
believe that the outer union should be an intersection instead. As it
is defined the current definition seems unsound as the following
is stated the current definition seems unsound as the following
example shows:
```
......
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