Commit 954b5363 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

new version of rebuttal

parent a4b1bf69
......@@ -3,13 +3,13 @@ QUESTIONS&ANSWERS
_**ReviewerA:** Are there idioms that are not typeable with Typescript or Flow today that become typeable with the presented system?_
Short answer: no example in Table 1 can be typed by Typescript/Flow/TypedRacket insofar as we "reconstruct" intersections of arrows and, as far as we know, no other type system does it. The cases typeable in the cited languages require the programmer to explicitly annotate the code with the precise intersection type, while our system can type the unannotated code (annotated with $Any$, which is equivalent). As a consequence, even if Flow and Typescript accept `foo` as defined in the very first page of our work, they both fail to type `(foo("Hello")).trim()` for which our system correctly infers the type `string`.[^footnote1]
Short answer: no example in Table 1 can be typed by Typescript/Flow insofar as we "reconstruct" intersections of arrows and, as far as we know, no other type system does it. The cases typeable in these languages require the programmer to explicitly annotate the code with the precise intersection type, while our system can type the unannotated code (annotated with $Any$, which is equivalent). As a consequence, even if Flow and Typescript accept `foo` as defined in the very first page of our work, they both fail to type `(foo("Hello")).trim()` for which our system correctly infers the type `string`.[^footnote1]
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)$?_
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 by 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._
......@@ -49,11 +49,11 @@ _Canonical_: The order in which we discussed the typing rules was a presentation
_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.
_Preliminary_: We presented two different applications of our system: reconstruction of arrow intersections (and detection of some dead code) and optimization of the compilation of gradually typed languages. We hope the reviewer will convene that this is unusual for a preliminary system.
_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 applicationsreconstruction 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).
**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._
We had to struggle with space constraints (probably the reviewers noticed it) so part of the implementation is presented only in the appendix and the explanation in the text is quite terse.
We had to struggle with space constraints (probably the reviewers noticed it) so part of the implementation is presented only in the appendix, the explanation in the text is quite terse, and comparison with the state of the art rather minimal.
We omitted from the implementation what is interesting only from a theoretical viewpoint but not in practice, that is, inferring negated arrow types for functions, but nothing else. This is exactly the same omission made by the language CDuce w.r.t. the JACM paper.
......@@ -72,7 +72,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 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.
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()`.
----------------------------------------
......@@ -92,3 +94,28 @@ function f(x: any) {
}
```
and of course, neither detect that one branch cannot ever be selected in `example10`.
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
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
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:
```
(Document => false | void)
& (Text => "boo" | void)
& ({ nodeType: 1; childNodes: NodeList} => "foo" | void)
```
even though not a single return type is correct. Likewise TypeScript accepts the following declaration
```
function is_empty_node (x : Document) : false;
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;
function is_empty_node (x : Text) : number;
function is_empty_node (x : Node) : boolean | number
```
So in both cases it is quite easy to end up with a result `false` of type `true`.
\ No newline at end of file
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