Commit 7caaedf1 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

rewording

parent 1df97067
......@@ -57,9 +57,12 @@ We had to struggle with space constraints (probably the reviewers noticed it).
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 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.
Code 10 in Table 1 demonstrates that our types also detect dead code that pass undetected by the flow analyses implemented by TypeScript and Flow.
----------------------------------------
[^footnote1] : To fully test this in Flow, one has to exclude also the `undefined` case. Both Flow and TypeScript incorrectly reject the following code
```
function foo(x : number | string) {
......@@ -69,10 +72,11 @@ 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 in 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.
----------------------------------------
[^footnote 2] : For code 10, Flow fails even 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 }
......
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