Commit 6574eabc authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

word saving

parent c782d366
......@@ -7,37 +7,38 @@ Short answer: no example in Table 1 can be typed by Typescript/Flow insofar as w
More importantly, typing the code 6, 7, 9, and 10 in Table 1 (and even more the code at lines 1114-1115 in our submission) is out of reach of the cited systems, even when using the right explicit annotations.[^footnote2]
_**ReviewerB:** why does $gx \in Bool$ under these assumptions leads to $x:Empty$? Since $Int$ is a subtype of $Any$, it should be fine for $x$ to be an $Int$ if $gx \in Bool$. Or is the type of $f$ and $g$ equivalent to $(Int \to Int) \wedge (\neg Int \to Bool)$?_
_**ReviewerB:** why does $gx\in\,Bool$ under these assumptions leads to $x:Empty$? Since $Int$ is a subtype of $Any$, it should be fine for $x$ to be an $Int$ if $gx{\in}Bool$. Or is the type of $f$ and $g$ equivalent to $(Int\to\,Int)\wedge(\neg\,Int\to\,Bool)$?_
If we assume that $x:Int$ (e.g., because we deduced it by analyzing the lhs of the test) then $g: ((Int \to Int) \wedge (Any \to Bool)) \leq (Int \to Int)$ implies that $g$ applied to an integer returns only integer results. Hence, the application of $g$ to an integer—such as $gx$—can be safely given type $Bool$ only if it diverges, such as for $x:Empty$. The type of $f,g$ is equivalent to $(Int \to Empty) \wedge (\neg Int \to Bool)$, a strict subtype of $(Int \to Int) \wedge (\neg Int \to Bool)$, which better shows why the `then` is never selected (we should probably add it).
If we assume that $x:Int$ (e.g., because we deduced it by analyzing the lhs of the test) then $g:((Int\to Int)\wedge(Any\to Bool))\leq(Int\to Int)$ implies that $g$ applied to an integer returns only integer results. Hence, the application of $g$ to an integer—such as $gx$—can be safely given type $Bool$ only if it diverges, such as for $x:Empty$. The type of $f,g$ is equivalent to $(Int\to Empty)\wedge(\neg Int\to Bool)$, a strict subtype of $(Int\to Int)\wedge(\neg Int\to Bool)$, which better shows why the `then` is never selected (we should probably add it).
_**ReviewerC:** Finally, this reviewer has one question [..] please explain what this reviewer may have missed here._
_Summary of the reviewer example:_
Dynamic test: $(x_1 x_2 \in t) ? e_1 : e_2$
Possible type (at runtime) for $x_1$: $(s_1 \to \neg t) \wedge (s_2 \to \neg t) \wedge (s_3 \to t)$
Inferred type for $x_1$ before the test: $(s_1 \to t) \vee (s_2 \to \neg t)$
Dynamic test: $(x_1x_2\in\,t)\,?\,e_1\,:\,e_2$
Possible type (at runtime) for $x_1$: $(s_1\to\neg\,t)\wedge(s_2\to\neg t)\wedge(s_3\to t)$
Inferred type for $x_1$ before the test: $(s_1\to t)\vee(s_2\to\neg t)$
Inferred type for $x_2$ before the test: $s_3$
As stated by the reviewer, if the tested expression $x_1 x_2$ is typeable,
then the type inferred for $x_1$ in the `then` branch would be $(s_1 \to t)$.
As stated by the reviewer, if the tested expression $x_1x_2$ is typeable,
then the type inferred for $x_1$ in the `then` branch would be $(s_1\to t)$.
However, it is _not_ unsafe to infer this type.
Indeed, if the tested expression $x_1 x_2$ is typeable, then we know that $s_3 \leq s_1$ and $s_3 \leq s_2$,
since $s_3$ must be included in the domain of $(s_1 \to t) \vee (s_2 \to \neg t)$, domain which is $s_1 \wedge s_2$ (_cf._ equation (13)).
Indeed, if the tested expression $x_1x_2$ is typeable, then we know that $s_3{\leq}s_1$ and $s_3{\leq}s_2$,
since $s_3$ must be included in the domain of $(s_1\to t)\vee(s_2\to\neg t)$, domain which is $s_1\wedge s_2$ (_cf._ equation (13)).
Thus, the suggested runtime type for $x_1$, that is,
$(s_1 \to \neg t) \wedge (s_2 \to \neg t) \wedge (s_3 \to t)$
$(s_1\to\neg t)\wedge(s_2\to\neg t)\wedge(s_3\to t)$
is a subtype of
$(s_3 \to \neg t) \wedge (s_3 \to \neg t) \wedge (s_3 \to t) = (s_3 \to (t\wedge \neg t)) = (s_3 \to Empty)$
$(s_3\to\neg t)\wedge(s_3\to\neg t)\wedge(s_3\to t)=(s_3\to(t\wedge\neg t))=(s_3\to Empty)$
As this function always diverges when applied to a value in $s_3$,
we know that the `then` branch is never reached and so it is safe to type $x_1$ with $(s_1 \to t)$ (or with any other type since $x_1 x_2:Empty$).
we know that the `then` branch is never reached and so it is safe to type $x_1$ with $(s_1 \to t)$ (or with any other type since $x_1x_2:Empty$).
As a side note: having a system with the $Empty$ type allows us to track expressions that are statically known to diverge and our system exploits this information via [EFQ]: _if the branch is taken, then the test did not diverge_, as we cursory tried to explain in lines 199-211.
OBSERVATIONS (out of 500 word limit)
============
......@@ -47,9 +48,9 @@ OBSERVATIONS (out of 500 word limit)
_Canonical_: The order in which we discussed the typing rules was a presentation choice, trying to go from simpler to harder, but the definition of the type system is canonical: it closely matches (and, of course, specializes) the type system of JACM 2008 with the only difference that the rules of Abstraction and Type-case here are each split in two distinct rules ([Abs+/Abs-] and [Case/EFQ]), essentially to ease the presentation: see Appendix A1 (w.r.t. JACM, we also added the intersection rule since, contrary to JACM, it is no longer admissible). While typing rules are canonical one of them, [Case], uses a deduction system for occurrences (i.e., $\vdash^{Path}$) which is brand new. Despite its novelty, its form is quite canonical: there is exactly one rule for each different path, plus three structural rules: subsumption, intersection, and a rule to glue the system with the typing rules. Furthermore, our experience is that the non-structural rules are crafted so that any smallest modification to them leads a system that is either unsound or less expressive.
_Definitive_: We did not have the space to argue it, but we *think* that our approach captures all it is possible to deduce by a monomorphic compositional type-system with set-theoretic types, that is, everything that does not need, say, a flow analysis. While we can argue about it, we so far failed to find a formal way to state it. Trade-offs start when trying to include contextual information (give up compositionality) and with polymorphism: the results we have about polymorphism are, in that case, preliminary, which is why, although we find them interesting, we relegated them to the end of the appendix.
_Definitive_: We did not have the space to argue it, but we *think* that our approach captures all it is possible to deduce by a monomorphic compositional type-system with set-theoretic types, that is, everything that does not need, say, a flow analysis. While we can argue about it, we so far failed to find a formal way to state it. Trade-offs start only when trying to include contextual information (give up compositionality) and with polymorphism: the results we have about polymorphism are, in that case, preliminary, which is why, although we find them interesting, we relegated them to the end of the appendix.
_Preliminary_: We reckon that the theory is sufficiently established and complete: even though it can be extended (e.g., polymorphism) it already yielded two different applications—reconstruction of arrow intersections (and detection of some dead code) and optimization of the compilation of gradually typed languages—. We agree, instead, that the implementation is preliminary, insofar as it is applied to a toy language rather than a real-world case. However, the implementation is already developed enough to compare our analysis with (and find several bugs in ... see [^footnote1,^footnote2]) the one performed by, among others, TypeScript and Flow (though space constraints did not allow us to detail this comparison: we will try to remedy this omission).
_Preliminary_: We reckon that the theory is sufficiently established and complete: although it can be extended (e.g., polymorphism), it already yielded two different applications—reconstruction of arrow intersections (and detection of some dead code) and optimization of the compilation of gradually typed languages—. Instead, we agree that our implementation is preliminary, insofar as it is applied to a toy language rather than a real-world case. However, the implementation is already developed enough to compare our analysis with (and find several bugs in ... see [^footnote1,^footnote2]) the one performed by, among others, TypeScript and Flow (though space constraints did not allow us to detail this comparison: we will try to remedy this omission).
**ReviewersAC** _The implementation section is ... only for a simplified version of the presented system ... unclear in what the evaluation of the implementation intended to demonstrate._
......@@ -72,9 +73,9 @@ function foo(x : number | string) {
var y = foo("Hello")
var z = (typeof y !== 'undefined')? y.trim() : "Hello"
```
In particular, `y.trim()` is reject by Flow with the message `Cannot call y.trim because property trim is missing in Number`, while TypeScript rejects both this expression and the expression `(foo("Hello")).trim()` with the message `Property trim does not exist on type string | number. Property trim does not exist on type number`. The code is instead accepted by our system.
In particular, `y.trim()` is rejected by Flow with the message `Cannot call y.trim because property trim is missing in Number`, while TypeScript rejects both this expression and the expression `(foo("Hello")).trim()` with the message `Property trim does not exist on type string | number. Property trim does not exist on type number`. The code is instead accepted by our system.
Oddly, if we remove the keyword `return` from the Flow code above, then `(foo("Hello")).trim()` become (correctly) accepted but so also (wrongly) becomes the call `(foo(42)).trim()`.
Oddly, if we remove the keyword `return` from the Flow code above, then `(foo("Hello")).trim()` become (correctly) accepted by Flow, but so also (wrongly) becomes the call `(foo(42)).trim()`.
----------------------------------------
......@@ -97,10 +98,10 @@ and of course, neither detect that one branch cannot ever be selected in `exampl
For the Code 8 the issue is more delicate. Both TypeScript and Flow
type the code without annotations, but of course they cannot reconstruct
our intersection types. When we add explicit annotations of the intersection
types our system inferred, then both TypeScript and Flow accept these annotations (with the
our intersection type. When we add the intersection
type inferred by our system as an explicit annotation, then both TypeScript and Flow accept these annotations (with the
caveat that for TypeScript one has also to specify the case for unions
of domains since TypeScript fails to do it). The point is that one can
of domains—here the case for `Element`since TypeScript fails to do it). The point is that one can
also give to these annotations completely wrong return types, and they
are accepted all the same. For instance, Flow accepts for
`is_empty_node` the type:
......@@ -114,7 +115,7 @@ even though not a single return type is correct. Likewise TypeScript accepts the
function is_empty_node (x : Document) : true;
function is_empty_node (x : { nodeType : 2; childNodes : Nil }) : false;
function is_empty_node (x : { nodeType : 2; childNodes : { nodeType : Node; next : NodeList } }) : 42;
function is_empty_node (x : Element) : boolean; // covers the union of the two previous cases
function is_empty_node (x : Element) : boolean; //covers the union of the two previous cases
function is_empty_node (x : Text) : number;
function is_empty_node (x : Node) : boolean | number
```
......
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