6 ms·

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?

by hasenj 9y ago

alangpierce 9y ago
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
curryhoward 9y ago
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-function-parameters-bivariant https://github.com/Microsoft/TypeScript/wiki/FAQ#why-are-fun...
- besquared 9y ago
  They added contravariant functions in 2.6 using the compiler flag --strictFunctionTypes as described in this PR https://github.com/Microsoft/TypeScript/pull/18654 https://github.com/Microsoft/TypeScript/pull/18654
- reacweb 9y ago
  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.
deleted 9y ago
[deleted]

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?

by hasenj 9y ago

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?

alangpierce 9y ago

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

curryhoward 9y ago

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-function-parameters-bivariant https://github.com/Microsoft/TypeScript/wiki/FAQ#why-are-fun...

besquared 9y ago
They added contravariant functions in 2.6 using the compiler flag --strictFunctionTypes as described in this PR https://github.com/Microsoft/TypeScript/pull/18654 https://github.com/Microsoft/TypeScript/pull/18654
reacweb 9y ago
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.

deleted 9y ago

[deleted]