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

bla

parent 6574eabc
......@@ -50,15 +50,15 @@ _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 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: 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).
_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._
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 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.
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.
What the implementation wants to demonstrate is that our theory of occurrence typing allows us to infer meaningful intersection types for unannotated functions: this is something nobody did before in our ken. This is probably due to the fact that inference for intersection types is undecidable and that there does not exist a principal type: the most precise type for a function $f$ is the infinite intersection $\bigwedge_{x\in dom(f)} x \to f(x)$. Since such a type cannot be expressed—let alone deduced—, we infer instead an approximation of it, using the type-cases on the parameters (and the applications of other discriminating functions) to drive how to partition the domain of the function, so as to get a meaningful and useful approximation.
What the implementation wants to demonstrate is that our theory of occurrence typing allows us to infer meaningful intersection types for unannotated functions: this is something nobody did before in our knowledge. This is probably due to the fact that inference for intersection types is undecidable and that there does not exist a principal type: the most precise type for a function $f$ is the infinite intersection $\bigwedge_{x\in dom(f)} x \to f(x)$. Since such a type cannot be expressed—let alone deduced—, we infer instead an approximation of it, using the type-cases on the parameters (and the applications of other discriminating functions) to drive how to partition the domain of the function, so as to get a meaningful and useful approximation.
Code 10 in Table 1 demonstrates that our types also detect dead code that passes undetected by the flow analyses implemented by TypeScript and Flow.
......@@ -79,7 +79,7 @@ Oddly, if we remove the keyword `return` from the Flow code above, then `(foo("H
----------------------------------------
[^footnote 2] : For code 10, Flow even fails to type
[^footnote 2] : For Code 10, Flow even fails to type
```
var f : (number => number) & (any => boolean) = x => {
if (typeof(x) === "number"){ throw "false" } else { return true }
......@@ -96,7 +96,7 @@ 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
For Code 8 the issue is more delicate. Both TypeScript and Flow
type the code without annotations, but of course they cannot reconstruct
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
......
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