What is soundness, exactly, and how is Typescript unsound?
It seems like a useless academic term that doesn't work so well in the real world, maybe?
It seems like a useless academic term that doesn't work so well in the real world, maybe?
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...
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.
https://flow.org/try/#0GYVwdgxgLglg9mABAWwKYGd0FUAOAVAC1QEEA...
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>`:
https://flow.org/try/#0GYVwdgxgLglg9mABAWwKYGd0FUAOAVAC1QEEA...
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.
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.
https://www.typescriptlang.org/play/index.html#src=function%...
That's because the author told Flow explicitly to expect an array of strings and numbers.
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);