Commit 1df97067 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

new version

parent 1e464ca5
......@@ -4,7 +4,7 @@ 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]
More importantly, typing the code 6, 7, and 9 in Table 1 is out of reach of the cited systems, even when using the right explicit annotations.
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)$?_
......@@ -60,14 +60,31 @@ We omitted from the implementation what is interesting only from a theoretical v
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.
[^footnote1] : To fully test this in Flow, one has to exclude also the `undefined` case. Both Flow and TypeScript uncorrectly reject the following code
[^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) {
return (typeof(x) === "number")? x++ : x.trim()
}
return (typeof(x) === "number")? x++ : x.trim()
}
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`.
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.
[^footnote 2] : For code 10, Flow fails even to type
```
var f : (number => number) & (any => boolean) = x => {
if (typeof(x) === "number"){ throw "false" } else { return true }
}
```
and so does TypeScript with the equivalent code
```
function f(x: number): number;
function f(x: any): boolean;
function f(x: any) {
if (typeof(x) === "number"){ throw "false" } else { return true }
}
```
and of course, neither detect that one branch cannot ever be selected in `example10`.
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