Commit 80e5c250 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

first pass on revision

parent 06fe433e
......@@ -253,14 +253,19 @@ arrow types, as long as these negated types do not make the type deduced for the
% makes the type empty? It should be safe since otherwise intersection
% would not be admissible in semantic subtyping (see Theorem 6.15 in
% JACM), but I think we should doube ckeck it.}
As explained in Section~\ref{sec:challenges}, we need to be able to
deduce for, say, the function $\lambda^{\Int\to\Int} x.x$ a type such
as $(\Int\to\Int)\wedge\neg(\Bool\to\Bool)$ (in particular, if this is
the term $e$ in equation \eqref{bistwo} we need to deduce for it the
type $(\Int\to t)\wedge\neg(\Int\to\neg\Bool)$, that is,
$(\Int\to t)\setminus(\Int\to\neg\Bool)$ ). But the sole rule \Rule{Abs+}
In Section~\ref{sec:challenges} we explained that in order for our
system to satisfy the property of type preservation, the type system
must be able to deduce negated arrow types for functions---e.g. the
type $(\Int\to\Int)\wedge\neg(\Bool\to\Bool)$ for $\lambda^{\Int\to\Int}
x.x$. We demonstrated this with the expression in
equation \eqref{bistwo}, where type preservation holds only if we are
able to deduce for this expression the type
$(\Int\to t)\setminus(\Int\to\neg\Bool)$, that is, $(\Int\to t)\wedge\neg(\Int\to\neg\Bool)$.
But the sole rule \Rule{Abs+}
above does not allow us to deduce negations of
arrows for abstractions: the rule \Rule{Abs-} makes this possible. As an aside, note that this kind
arrows for $\lambda$-abstractions: the rule \Rule{Abs-} makes this possible. As an aside, note that this kind
of deduction is already present in the system by~\citet{Frisch2008}
though in that system this presence was motivated by the semantics of types rather than, as in our case,
by the soundness of the type system.
......@@ -197,7 +197,7 @@ for `y` it will simply be `String \/ Number` (and the initial
typechecking will fail). As in `example14_alt` on page 27, a redundant
test will make inference succeed.
>> Yes indeed
>> Yes indeed, we can add a remark on that
## Smaller Comments
......@@ -213,6 +213,12 @@ test will make inference succeed.
* On page 10, line 20, there's a reference to an explanation in
section 1.3 that does not seem to exist.
Indeed, it is not very clear what we referred to (in the specific case
we meant the need to deduce negated arrow types for type preservation). We
rewrote the sentence to be more clear.
>> Beppe: rewrite to say that in section 1.3 we need sometimes to deduce negated arrows
......@@ -233,7 +239,29 @@ test will make inference succeed.
* In the definition of AbsInf+ on p21, could we exclude from $T$ the
elements \sigma where typechecking succeeds for $\sigmap\Uparrow$?
That seems like it would result in strictly more-precise types.
>> Beppe To BE DONE, but in general the fewer the arrows the less precise is the type (but maybe it is not necessary, check)
**Answer**: proceeding as suggested would result in *less* precise
types. This can be understood in general, since removing types from
an intersection yields larger (i.e., less precise) types. But it can
also be shown by slightly modifying the `foo` example as follows
function foo(x : ?) {
(typeof(x) x== "number") ? x : x.trim()
where we replaced `x` for `x+1` in the "then" branch. Repeating the reasoning
of the paper we would obtain the type
(number ∧ ? → number ∧ ?) ∧ (number → number) ∧ ((?\number) →
removing the first arrow of the intersection would yield less a
precise type: applying the function to an arguement of type `number
∧ ?` would yield a result of the same type which by a cast could be
used in every context where a strict subtype of `number` is
expected, which becomes impossible if we remove that arrow.
......@@ -25,9 +25,11 @@
\newcommand{\rev}[1] {{\color{revision}#1}}
\newcommand{\beppe}[1]{{\bf\color{blue}Beppe: #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