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

more work on the revision

parent d634fb90
......@@ -284,6 +284,16 @@ url={http://www.cduce.org/papers/frisch_phd.pdf}
keywords = {Racket, Refinement types, occurrence typing},
}
@PhdThesis{kent19phd,
author = {Andrew M. Kent},
title = {Advanced Logical Type Systems for Untyped Languages},
school = {Indiana University},
year = 2019,
month = {oct},
url = {https://pnwamk.github.io/docs/dissertation.pdf}}
@article{Bierman10,
author = {Bierman, Gavin M. and Gordon, Andrew D. and
Cătălin Hriţcu and Langworthy, David},
......
......@@ -18,42 +18,72 @@ Occurrence typing was introduced by \citet{THF08} and further advanced
in \cite{THF10} in the context of the Typed Racket language. This
latter work in particular is close to ours, with some key differences.
\citet{THF10} define $\lambda_{\textit{TR}}$, a core calculus for
Typed Racket. In this language types are annotated by logical
Typed Racket. In this language types are annotated by two logical
propositions that record the type of the input depending on the
(Boolean) value of the output. For instance, the type of the
{\tt number?} function states that when the output is {\tt true}, then
the argument has type {\tt Number}, and when the output is false, the
the argument has type {\tt Number}, and when the output is {\tt false}, the
argument does not. Such information is used selectively
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
approach has several merits over theirs. First, in our case, type
test.
\rev{This is particularly beneficial when typing functions since the
logical propositions of Tobin-Hochstadt and Felleisen can record
dependencies on expressions other than the input of a
function. Consider for instance the following example (due
to~\cite{kent19phd}) in JavaScript \code{function
is-y-a-number(x) \{ return(typeof(y)\,===\,"number") \}} which defines
a functions that
disregards its argument and returns whether the variable \code{y} is
an integer or not.\footnote{Although such a function may appear
nonsensical, Kent~\cite{kent19phd} argues that it corresponds a programming
patter that may occurr in Typed Racked due to the the expansion of some
sophisticated macro definitions.} While our approach cannot deduce for this function but the
type $\Any\to\Bool$, the logical approach of Tobin-Hochstadt and
Felleisen can record in the type of \code{is-y-a-number} that fact
when the function returns \texttt{true} then \code{y} is a number, and
the opposite when it returns \texttt{false}. In our approach, the only
possibility to track such a dependency is that the variable \code{y}
is the parameter of an outer function to which our analysis could give
an overloaded type by splitting the type \texttt{Any} of \texttt{y}
into \texttt{Number} and \texttt{$\neg$Number}. Under the hypothesis
of \texttt{y} being of type \texttt{Number} the type inferred
for \code{is-y-a-number} will then be $\Any\to\True$, and
$\Any\to\False$ otherwise, thus capturing the wanted dependency.
%
Although the approach of using logical proposition has the undeniable
advantage over ours of providing more a flow sensitive analysis, we
believe that using semantic subtyping as a foundation as we do
has also several merits over the logical proposition approach.
}%%%rev
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
Section~\ref{sec:practical}. Second, in our setting, {\em types\/} play
the role of formulæ. Using set-theoretic types, we can express the
complex types of variables without resorting to a meta-logic. This
Section~\ref{sec:practical}. Second, in our setting, {\em types\/}
play the role of formulæ. Using set-theoretic types, we can express
the complex types of variables without resorting to a meta-logic. This
allows us to type all but two of their key examples (the notable
exceptions being Example~9 and 14 in their paper, which use the propagation of type
information outside of the branches of a test). While Typed Racket
supports structured data types such as pairs and records only unions
of such types can be expressed at the level of types, and even for
those, subtyping is handled axiomatically. For instance, for pairs,
the subtyping rule presented in \cite{THF10} is unable to deduce that
exceptions being Example~9 and 14 in their paper, which use the
propagation of type information outside of the branches of a
test). While Typed Racket supports structured data types such as pairs
and records only unions of such types can be expressed at the level of
types, and even for those, subtyping is handled axiomatically. For
instance, for pairs, 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})$ (and likewise for other type constructors combined with union types). For record
(\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})$ (and likewise
for other type constructors combined with union types). For record
types, we also type precisely the deletion of labels, which, as far as
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}.
\kim{Remove or merge :
Also, while they
extend their core calculus with pairs, they only provide a simple {\tt
......@@ -114,6 +144,24 @@ are complete with respect to the algorithmic system, thus exploring
different language designs and arguing about their usefulness.
}%%%rev
\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
...
%
}%%%rev
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
......
......@@ -96,7 +96,42 @@ The thesis is available at https://pnwamk.github.io/docs/dissertation.pdf
>> Mickael: premier draft et comparison avec worra
**ANSWER:**
**ANSWER:** First of all we want to thank the reviewer for pointing us
Andrew Kent's PhD dissertation. We were aware of Kent's work on OT
modulo theories we discussed in the related work section and of his
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
the pandemic.
Of course, the new version of the related work section includes now a
detailed comparaison with the (highly related) chapter 5 of the
dissertations, see lines (??-??) and, yes, the function application
inversion of Kent is, in the spirit, the same as our worra
operator. About that, we take the opportunity that the reviewer
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
example shows:
```
inv (((True->False) /\ (False->True)) \/ ((True->True) /\ (False->False)), True)
= Bool \ (True\/False) = Empty
```
However, a function with type `((True->False) /\ (False->True)) \/
((True->True) /\ (False->False))` can definitively give a result in
`True`. The correct result should be `Bool`.
The proof in Coq of the soundness of this definition given in the appendix of the thesis does not cover this case, as any other case in which functions are typed by unions, since it assumes that the disjunctive normal form of a function type is formed only by intersections of arrows and of negations thereof.
If we change the union at issue into an intersection, it becomes equivalent to our algorithmic definition of *worra* (p13) as it can be verified by a simple application of De Morgan's Laws.
We would be grateful if the reviewer could confirm that we did not misinterpret the definition in the dissertation. If it is so, was the author aware of this problem and does there exist a corrected version of the algorithm to which we could refer in our related work section? Thank you in advance.
A. Kent's approach is based on control flow. As soon as a variable is defined, it computes and remember under which constraints this variable can be in True or ~True (Beppe: isn it rather False and ¬False?). Typecases can only be done on variables (Beppe: really???), and the former information is used to refine the context of the then and else branches. A new idea of A. Kent's thesis compared to previous works on occurence typing is the use of semantic types to store these constraints, and the use of an application inversion function to compute them. We also use these ideas in our paper.
(Beppe: where do we use it other than for False and ¬False?) (Beppe: isint (f x) on ne peut rien apprendre sur x )
......@@ -147,9 +182,12 @@ Similarly the need for an explosion
rule in order to circumvent difficulties in proofs of type soundness
is discussed in [22].
**DONE** we added a long discussion on this point in the related work
**DONE** we added a long discussion on this point, namely how to handle the type preservation property, in the related work
section when comparing with [22] (see lines: ??-??)
More generally, we also went more in depth in the comparaison with the
logical approach by THF, to highlight further limitations of our
approach as requested by the reviewers.
## Discussion of pure expressions
......
......@@ -24,7 +24,7 @@
%\definecolor{darkred}{rgb}{0.7,0.4,0.4}
\definecolor{darkred}{rgb}{0.8,0.2,0.2}
\definecolor{pervenche}{RGB}{80,80,100}
\definecolor{revision}{RGB}{0,207,102}
\definecolor{revision}{RGB}{0,143,79}
%\usepackage{lineno}
%\linenumbers
\newcommand{\rev}[1] {{\color{revision}#1}}
......
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