Here's an example of TypeScript failing to be sound - it should give a type error but it doesn't. I believe Flow does indeed give a type error in this situation:
When a language's type system is sound, that means that if you have an expression with type "string", then when you run the program the expression's value will only ever be a string and never some other sort of value.
Or stated more abstractly: if an expression has type T, and at runtime the expression evaluates to a value v, then v has type T.
The language can still have runtime errors, like if you try to access an array out of bounds. The key is that such operations have to give an error — like by throwing, so that the expression doesn't evaluate to any value at all — rather than returning a value that doesn't fit the type.
Both TypeScript and Flow are unsound, because an expression with type "string" can always turn out to evaluate to null or a number or an object or anything else. Flow had the ambition to be sound, which is honorable but they never accomplished it. TypeScript announced up front that they didn't care about soundness:
https://www.typescriptlang.org/docs/handbook/type-compatibil...
Soundness is valuable because it makes it possible to look at the types and reason about the program using them. An unsound type-checker like TypeScript or Flow can still be very useful to human readers if most of the types in a codebase are accurate, but you always have to keep that asterisk in the back of your head.
One very concrete consequence of soundness that it makes it possible to compile the code to fast native code. That's what motivated Dart a few years ago to migrate from an unsound type system to a sound one:
https://dart.dev/language/type-system
so that it could AOT-compile Flutter apps for speed.
pansa2|1 year ago
https://news.ycombinator.com/item?id=41069695
recursive|1 year ago
price|1 year ago
Or stated more abstractly: if an expression has type T, and at runtime the expression evaluates to a value v, then v has type T.
The language can still have runtime errors, like if you try to access an array out of bounds. The key is that such operations have to give an error — like by throwing, so that the expression doesn't evaluate to any value at all — rather than returning a value that doesn't fit the type.
Both TypeScript and Flow are unsound, because an expression with type "string" can always turn out to evaluate to null or a number or an object or anything else. Flow had the ambition to be sound, which is honorable but they never accomplished it. TypeScript announced up front that they didn't care about soundness: https://www.typescriptlang.org/docs/handbook/type-compatibil...
Soundness is valuable because it makes it possible to look at the types and reason about the program using them. An unsound type-checker like TypeScript or Flow can still be very useful to human readers if most of the types in a codebase are accurate, but you always have to keep that asterisk in the back of your head.
One very concrete consequence of soundness that it makes it possible to compile the code to fast native code. That's what motivated Dart a few years ago to migrate from an unsound type system to a sound one: https://dart.dev/language/type-system so that it could AOT-compile Flutter apps for speed.