Commit 9c1632ab authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

final strikes back?

parent 220b5f00
......@@ -3,20 +3,20 @@ 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 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]
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], and likewise for the other code.
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_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)$
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$
......@@ -25,15 +25,15 @@ 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_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)).
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_1x_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.
......@@ -44,7 +44,7 @@ REMARKS & REVIEWERS' CONCERNS (out of the 500-word limit)
================================
**ReviewerC:** _Strenghts_ and _Weaknesses_ in the review are exactly the same: is this wanted or a cut&paste problem?
**ReviewerC:** In this reviewer's review _Strenghts_ and _Weaknesses_ are exactly the same: is this wanted or a cut&paste problem?
**ReviewerA:** _Is the formulation of the type system canonical, definitive, preliminary?_
......@@ -54,7 +54,7 @@ _Definitive_: We did not have the space to argue it, but we *think* that our app
_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/flaws 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._
**ReviewersA&C:** _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, the explanation in the text is quite terse, and comparison with the state of the art is rather minimal.
......
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