4 ms·

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 c

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. Here's an example of unsoundness in TypeScript: https://www.typescriptlang.org/play/index.html#src=function%20messUpTheArray(arr%3A%20Array%3Cstring%20%7C%20number%3E)%3A%20void%20%7B%0D%0A%20%20%20%20arr.push(3)%3B%0D%0A%7D%0D%0A%0D%0Aconst%20strings%3A%20Array%3Cstring%3E%20%3D%20%5B'foo'%2C%20'bar'%5D%3B%0D%0AmessUpTheArray(strings)%3B%0D%0A%0D%0Aconst%20s%3A%20string%20%3D%20strings%5B2%5D%3B%0D%0Aconsole.log(s.toLowerCase())%0D%0A 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/#0GYVwdgxgLglg9mABAWwKYGd0FUAOAVAC1QEEAnUgQwE8AKC8gLkTMqoB50pSYwBzRAD6IwIZACNUpAHwBKJgDc4MACaIA3gChE2xPVIA6HCHQEaAZhkBuDQF8NGiAk6JO3PuiYtqHLj15TEAF5EAG0AcmA4ODCAGkQwsXowgF1rNExcQhJyahpXP3Qre0cwZw8XXz4girdedBCAJlSHJzgAG1R9NrhePP0oOAAZOAB3SQBhCnRUGhkZDSA https://flow.org/try/#0GYVwdgxgLglg9mABAWwKYGd0FUAOAVAC1QEEA...

maxbrunsfeld 9y ago
Thanks for the really concise example.
yladiz 9y ago
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.
- alangpierce 9y ago
  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: https://flow.org/try/#0GYVwdgxgLglg9mABAWwKYGd0FUAOAVAC1QEEAnUgQwE8AKC8gLkTMqoB50pSYwBzAPgCUTAG5wYAE0QBvAFCIFieqQB0OEOgI0A5ACMKAL22CA3LIC+s2RASdEnbn3RMW1Dlx4DEAXkQBtbWA4OG0AGkQ9em0AXTM0TFxCEnJqGgdPdFMrGzA7Z3sPPh8Cx150PwAmWOtbOAAbVBU6uF40lSg4ABk4AHdUUgBhCnRUGkFBWSA 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/#0GYVwdgxgLglg9mABAWwKYGd0FUAOAVAC1QEEAnUgQwE8AKC8gLkQBIAlVCgEwHkwAbKmUpUAPOiikYYAOaIAPojAhkAI1SkAfAEomANzgxOiAN4AoRBcQQE6OH1QA6PnGl1yAbQAMAXS0BuUwBfU1NrMHFEcUkZdCYhajEJKWkNRABeRHcAcmA4OCyAGkQslXos7wC0TFxCEnJqGijk9H8QsIjYyKSZdK7o6XR3ACYK0Js7R2dXdAcoOAAZOAB3dQBhCnRUGi0tUyA 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.
  - yladiz 9y ago
    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.
- 9y ago

maxbrunsfeld 9y ago

Thanks for the really concise example.

yladiz 9y ago

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.

alangpierce 9y ago
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: https://flow.org/try/#0GYVwdgxgLglg9mABAWwKYGd0FUAOAVAC1QEEAnUgQwE8AKC8gLkTMqoB50pSYwBzAPgCUTAG5wYAE0QBvAFCIFieqQB0OEOgI0A5ACMKAL22CA3LIC+s2RASdEnbn3RMW1Dlx4DEAXkQBtbWA4OG0AGkQ9em0AXTM0TFxCEnJqGgdPdFMrGzA7Z3sPPh8Cx150PwAmWOtbOAAbVBU6uF40lSg4ABk4AHdUUgBhCnRUGkFBWSA 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/#0GYVwdgxgLglg9mABAWwKYGd0FUAOAVAC1QEEAnUgQwE8AKC8gLkQBIAlVCgEwHkwAbKmUpUAPOiikYYAOaIAPojAhkAI1SkAfAEomANzgxOiAN4AoRBcQQE6OH1QA6PnGl1yAbQAMAXS0BuUwBfU1NrMHFEcUkZdCYhajEJKWkNRABeRHcAcmA4OCyAGkQslXos7wC0TFxCEnJqGijk9H8QsIjYyKSZdK7o6XR3ACYK0Js7R2dXdAcoOAAZOAB3dQBhCnRUGi0tUyA 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.
- yladiz 9y ago
  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.
9y ago