5 ms·
I found the comment about soundness in the linked post to be kind of an odd remark. It didn't take me long after reading that to come up with an invalid progra
by evmar 10y ago
I found the comment about soundness in the linked post to be kind of an odd remark.
It didn't take me long after reading that to come up with an invalid program that is accepted by Flow's type checker. (The typechecker normally rejects doing math against strings, but accepts this.)
let array = [1,2];
array.pop();
array.push('hello');
console.log(array[1] - 3);
To be clear, being completely sound is hard! There's a lot of space in type systems and Flow must make some hard decisions itself; whether it's "sound" or not is kinda orthogonal to whether it's useful or not. And I'm sure Flow is useful. So let's not talk about soundness.
(Disclaimer: I work with TypeScript and am pretty fond of it.)
- recursive 10y agoI guess they fixed it. Try it yourself. http://www.typescriptlang.org/play/ http://www.typescriptlang.org/play/ Argument of type 'string' is not assignable to parameter of type 'number' on line 3.
- evmar 10y agoSorry for the confusing comment -- I updated it. I was saying that it is strange for the linked post to talk about soundness being important when it's trivial to find an unsound Flow program. (This particular program is properly rejected by TypeScript but TypeScript is also unsound so there are plenty of other invalid programs that it accepts.)
- recursive 10y agoI think it's a lot harder to get past TypeScript's type checker. It's probably possible, but I can't think of a way to do it off the top of my head without casting to any. It's a lot easier to show correctly executing javascript programs that would be rejected by the type checker.
- evmar 10y agoHere's one that TypeScript gets wrong. It's kind of a canonical example of a program that is difficult to get right in a type system. (It's how I found the Flow example linked upthread.) let x: number[] = []; let y: Object[] = x; y.push('a'); let bad = x.pop(); // bad has type number but is actually a string.