Soundness means that if the type system says that a variable has a particular type, then it definitely has that type at runtime. A sound type system is always correct, and an unsound type system might be incorrect in some cases.
TypeScript incorrectly (but conveniently) says that Array<string> can be assigned to Array<string | number>, and you can exploit that to create an "s" variable that TypeScript thinks is a string but is actually a number.
You can try the same code in Flow and it gives a type error:
So Flow seem to be complaining that number and string are incompatible types for the array elements. I attempted to change your arr.push(3) statement to one that is appending a string, and it gave the same error even though it should not have given an error in that case.
Neither Flow nor TypeScript are correct in this instance. Neither keep track of the actual array element's value, just the general type of the array, which means they actually don't know for sure and do their best guess. So in the Flow example, it complains that the number and string types are incompatible even though it doesn't know that this specific case is incompatible, just the general case. In the TypeScript example, it should keep track of the type of the argument value supplied during the function invocation, not the type for the argument declaration.
In this case I would argue that even though TypeScript is incorrect, it's preferable to Flow because Flow doesn't infer that the types are incompatible from actual usage but theoretical.
Agreed. This is one of the things people hate about type systems is fighting with them saying "I know better".
This example is quite interesting because javascript itself does not provide a way to check the type of an array, unlike a primitive. This is likely due to the fact that an empty array doesn't really have a type for it's items yet.
Here is an example where typescript can infer the type using the `typeof` runtime check but provide compile time checking.
The issue with changing `arr.push(3)` to `arr.push('baz')` is that there's still a type annotation on the function saying `Array<string | number>`. If you get rid of the type annotation or change it to `Array<string>`, flow is ok with it:
Both Flow and TypeScript have good type inference (with Flow's generally being better, I think) and do pretty well with all type annotations removed, but that wasn't shown in my example because I explicitly annotated all types.
Note that if you do want/need to give an explicit type annotation for this sort of thing, Flow provides `$ReadOnlyArray`, where `Array<string>` is assignable to `$ReadOnlyArray<string | number>`:
It sounds like you're arguing that TypeScript is wrong because it's overly-permissive, and Flow is wrong because it's overly-strict, which makes sense. That's probably why people prefer to use the word "sound" to describe Flow rather than "correct". Every sound type system has cases where you can write perfectly correct code that would be rejected by the type system (which is provable because of the halting problem). Opting into a type system always means that you limit the type of code you can write in exchange for better automatic verification.
An issue with $ReadOnlyArray is that if you're doing something that does work on both String and Number types, like using them for some template string, Flow will complain that the types are not compatible even though in this instance they are. This is a bigger issue with both TypeScript and Flow, in that they don't seem to keep enough track of the data in arrays, only the type of the array, to know if the actual types are valid. If TypeScript/Flow kept track of the array elements and their usage, this issue wouldn't occur in the same way.
In the previous paragraph I'm more clear about my meaning, which is that the array elements are not tracked properly, meaning that Flow/TypeScript can't determine if the actual usage is valid 100% accurately.
Just as an example, this program type checks in TypeScript but crashes at runtime:
class Dog {
}
class Greyhound extends Dog {
doGreyhoundThing(): void {
console.log("I am a greyhound!");
}
}
class Poodle extends Dog {
doPoodleThing(): void {
console.log("I am a poodle!");
}
}
function f(g:(Dog) => void) : void {
let hound: Greyhound = new Greyhound();
g(hound);
}
function h(p: Poodle): void {
p.doPoodleThing();
}
f(h);
`f(h);` would be a type error if function types were contravariant in their argument types. TypeScript made the unsound choice to let function types be bivariant in their argument types, which the authors claim is justified for practical reasons. More info here: https://github.com/Microsoft/TypeScript/wiki/FAQ#why-are-fun...
When I was student (1992), a friend noticed exactly the same issue in the eiffel language. They answered also that the incorrect check was more practical.
Here's an example of unsoundness in TypeScript:
https://www.typescriptlang.org/play/index.html#src=function%...
TypeScript incorrectly (but conveniently) says that Array<string> can be assigned to Array<string | number>, and you can exploit that to create an "s" variable that TypeScript thinks is a string but is actually a number.
You can try the same code in Flow and it gives a type error:
https://flow.org/try/#0GYVwdgxgLglg9mABAWwKYGd0FUAOAVAC1QEEA...