7 ms·

I think the even bigger elephant in the room is that TypeScript's type system is unsound. You can have a function whose parameter type is annotated to be String

I think the even bigger elephant in the room is that TypeScript's type system is unsound. You can have a function whose parameter type is annotated to be String and there's absolutely no guarantee that every call to that function will pass it a string. This isn't because of `any` either. The type system itself deliberately has holes in it. So any language that uses TypeScript type annotations to generate faster/smaller code is opening itself to miscompiling code and segfaults, etc.

wk_end 2y ago
So - I know this in theory, but avoided mentioning it because I couldn’t immediately think of any persuasive examples (whereas subtype polymorphism is a core, widely used, wholly unrestricted property of the language) that didn’t involve casts or any/unknown or other things that people might make excuses for. Do you have any examples off the top of your head?
- neongreen 2y ago
  https://counterexamples.org/ https://counterexamples.org/ is a good collection of unsoundness examples in various languages. For TypeScript, they list an example with `instanceof`: https://counterexamples.org/polymorphic-union-refinement.html https://counterexamples.org/polymorphic-union-refinement.htm... In the playground: https://www.typescriptlang.org/play/?#code/GYVwdgxgLglg9mABAdwE4EMAOAeAKgPgAoAPALkV0QB9EBBVDATz3wEpz6mXEBvAKESIYwRCSFgAzlHSQApnBGd0jVolSyoIVEmIBuAWo1akAbWIBdfQF8+fUJFgIhAExYlyudhV4GICKYgSHibmiAC8KBiYJKz6guqa2oEmAAyWfDZ8fpJQiM4wAOYwUEGIYCAAtgBGsqgh4S6EJgDMADSIAIztACzmsXwA9AOI4BJw4M7kAAb5RSVTQhKI6NAg6AA264yIU81TfLPFEgB0MJDrIM6yEoTdsYJDFIyYsgCiDHCo5Iclp+eX10WZTguXQiHs0HgYD4QA https://www.typescriptlang.org/play/?#code/GYVwdgxgLglg9mABA...
- sixbrx 2y ago
  Here's an example I constructed after reading the TS docs [1] about flow-based type inference and thinking "that can't be right...". It yields no warnings or errors at compile stage but gives runtime error based on a wrong flow-based type inference. The crux of it is that something can be a Bird (with "fly" function) but can also have any other members, like "swim" because of structural typing (flying is the minimum expected of a Bird). The presence of a spurious "swim" member in the bird causes tsc to infer in a conditional that checks for a "swim" member that the animal must be a Fish or Human, when it is not (it's just a Bird with an unrelated, non-function "swim" member). type Fish = { swim: () => void }; type Bird = { fly: () => void }; type Human = { swim?: () => void; fly?: () => void }; function move(animal: Fish | Bird | Human) { if ("swim" in animal) { // TSC infers wrongly here the presence of "swim" implies animal must be a Fish or Human onlyForFishAndHumans(animal); } else { animal; } } function onlyForFishAndHumans(animal: Fish | Human) { if (animal.swim) { animal.swim(); // Error: attempt to call "not-callable". } // (receives bird which is not a Fish or Human) } const someObj = { fly: () => {}, swim: "not-callable" }; const bird: Bird = someObj; move(bird); // runtime error: [ERR]: animal.swim is not a function [1] https://www.typescriptlang.org/docs/handbook/2/narrowing.html#the-in-operator-narrowing https://www.typescriptlang.org/docs/handbook/2/narrowing.htm...
  - oxidant 2y ago
    This narrowing is probably not the best. I'm not sure why the TS docs suggest this approach. You should really check the type of the key to be safer, though it's still not perfect. if (typeof animal.swim === 'function') {....}
    - saghm 2y ago
      Compilers don't really have the option of just avoiding non-idiomatic code, though. If the goal is to compile TypeScript ahead of time, the only options are to allow it or to break compatibility, and breaking compatibility makes using ahead-of-time TypeScript instead of some native language that already exists much less compelling.
  - deleted 2y ago
    [deleted]
  - noway421 2y ago
    Here's a simpler repro: type Bird = { id: number }; type Human = { swim?: () => void; id: number }; function move(animal: Bird | Human) { onlyForHumans(animal); } function onlyForHumans(swimmer: Human) { if (swimmer.swim) { swimmer.swim(); } } const someObj = { id: 1, swim: "not-callable" }; move(someObj); `someObj` gets casted as `Bird`, then `animal` gets casted as `Human`. Unfortunately unions here are indeed unsound. As as workaround you could add a property `type` (either `"bird"` or `"human"`) to both `Bird` and `Human`, then TypeScript would be able to catch it.
- kcrwfrd_ 2y ago
  const foo: string[] = ['foo'] // inferred as string // though it is undefined const bar = foo[1]
curtisblaine 2y ago
It might be useful for an interpreter though. I believe that in V8 you have this probabilistic mechanism in which if the interpreter "learns" that an array contains e.g. numbers consistently, it will optimize for numbers and start accessing the array in a more performance way. Typescript could be used to inform the interpreter even before execution. (My supposition, I'm not an interpreter expert)
g15jv2dp 2y ago
> I think the even bigger elephant in the room is that TypeScript's type system is unsound. Can you name a single language that is used for high-performance software and whose type system is sound? To speed up the process, note that none of the obvious candidates have sound type systems.
- IsTom 2y ago
  I'm a little behind times on Haskell (haven't used it for some years) – there always were extensions that made it unsound, but the core language was pretty solid.
  - g15jv2dp 2y ago
    Look at the last example in there: https://counterexamples.org/polymorphic-references.html https://counterexamples.org/polymorphic-references.html
    - IsTom 2y ago
      Well, it does use unsafePerformIO. It's not particularly horrible most of the time, but in this case it obviously is.
- deleted 2y ago
  [deleted]
- MathMonkeyMan 2y ago
  Maybe OCaml, but I haven't studied it much.
  - g15jv2dp 2y ago
    I doubt it's been proved to be sound. It shows up a lot on https://counterexamples.org/ https://counterexamples.org/, although if I skim the issues seem to have been fixed since then.
    - 2y ago

wk_end 2y ago

So - I know this in theory, but avoided mentioning it because I couldn’t immediately think of any persuasive examples (whereas subtype polymorphism is a core, widely used, wholly unrestricted property of the language) that didn’t involve casts or any/unknown or other things that people might make excuses for. Do you have any examples off the top of your head?

neongreen 2y ago
https://counterexamples.org/ https://counterexamples.org/ is a good collection of unsoundness examples in various languages. For TypeScript, they list an example with `instanceof`: https://counterexamples.org/polymorphic-union-refinement.html https://counterexamples.org/polymorphic-union-refinement.htm... In the playground: https://www.typescriptlang.org/play/?#code/GYVwdgxgLglg9mABAdwE4EMAOAeAKgPgAoAPALkV0QB9EBBVDATz3wEpz6mXEBvAKESIYwRCSFgAzlHSQApnBGd0jVolSyoIVEmIBuAWo1akAbWIBdfQF8+fUJFgIhAExYlyudhV4GICKYgSHibmiAC8KBiYJKz6guqa2oEmAAyWfDZ8fpJQiM4wAOYwUEGIYCAAtgBGsqgh4S6EJgDMADSIAIztACzmsXwA9AOI4BJw4M7kAAb5RSVTQhKI6NAg6AA264yIU81TfLPFEgB0MJDrIM6yEoTdsYJDFIyYsgCiDHCo5Iclp+eX10WZTguXQiHs0HgYD4QA https://www.typescriptlang.org/play/?#code/GYVwdgxgLglg9mABA...
sixbrx 2y ago
Here's an example I constructed after reading the TS docs [1] about flow-based type inference and thinking "that can't be right...". It yields no warnings or errors at compile stage but gives runtime error based on a wrong flow-based type inference. The crux of it is that something can be a Bird (with "fly" function) but can also have any other members, like "swim" because of structural typing (flying is the minimum expected of a Bird). The presence of a spurious "swim" member in the bird causes tsc to infer in a conditional that checks for a "swim" member that the animal must be a Fish or Human, when it is not (it's just a Bird with an unrelated, non-function "swim" member). type Fish = { swim: () => void }; type Bird = { fly: () => void }; type Human = { swim?: () => void; fly?: () => void }; function move(animal: Fish | Bird | Human) { if ("swim" in animal) { // TSC infers wrongly here the presence of "swim" implies animal must be a Fish or Human onlyForFishAndHumans(animal); } else { animal; } } function onlyForFishAndHumans(animal: Fish | Human) { if (animal.swim) { animal.swim(); // Error: attempt to call "not-callable". } // (receives bird which is not a Fish or Human) } const someObj = { fly: () => {}, swim: "not-callable" }; const bird: Bird = someObj; move(bird); // runtime error: [ERR]: animal.swim is not a function [1] https://www.typescriptlang.org/docs/handbook/2/narrowing.html#the-in-operator-narrowing https://www.typescriptlang.org/docs/handbook/2/narrowing.htm...
- oxidant 2y ago
  This narrowing is probably not the best. I'm not sure why the TS docs suggest this approach. You should really check the type of the key to be safer, though it's still not perfect. if (typeof animal.swim === 'function') {....}
  - saghm 2y ago
    Compilers don't really have the option of just avoiding non-idiomatic code, though. If the goal is to compile TypeScript ahead of time, the only options are to allow it or to break compatibility, and breaking compatibility makes using ahead-of-time TypeScript instead of some native language that already exists much less compelling.
- deleted 2y ago
  [deleted]
- noway421 2y ago
  Here's a simpler repro: type Bird = { id: number }; type Human = { swim?: () => void; id: number }; function move(animal: Bird | Human) { onlyForHumans(animal); } function onlyForHumans(swimmer: Human) { if (swimmer.swim) { swimmer.swim(); } } const someObj = { id: 1, swim: "not-callable" }; move(someObj); `someObj` gets casted as `Bird`, then `animal` gets casted as `Human`. Unfortunately unions here are indeed unsound. As as workaround you could add a property `type` (either `"bird"` or `"human"`) to both `Bird` and `Human`, then TypeScript would be able to catch it.
kcrwfrd_ 2y ago
const foo: string[] = ['foo'] // inferred as string // though it is undefined const bar = foo[1]

curtisblaine 2y ago

It might be useful for an interpreter though. I believe that in V8 you have this probabilistic mechanism in which if the interpreter "learns" that an array contains e.g. numbers consistently, it will optimize for numbers and start accessing the array in a more performance way. Typescript could be used to inform the interpreter even before execution. (My supposition, I'm not an interpreter expert)

g15jv2dp 2y ago

> I think the even bigger elephant in the room is that TypeScript's type system is unsound. Can you name a single language that is used for high-performance software and whose type system is sound? To speed up the process, note that none of the obvious candidates have sound type systems.

IsTom 2y ago
I'm a little behind times on Haskell (haven't used it for some years) – there always were extensions that made it unsound, but the core language was pretty solid.
- g15jv2dp 2y ago
  Look at the last example in there: https://counterexamples.org/polymorphic-references.html https://counterexamples.org/polymorphic-references.html
  - IsTom 2y ago
    Well, it does use unsafePerformIO. It's not particularly horrible most of the time, but in this case it obviously is.
deleted 2y ago
[deleted]
MathMonkeyMan 2y ago
Maybe OCaml, but I haven't studied it much.
- g15jv2dp 2y ago
  I doubt it's been proved to be sound. It shows up a lot on https://counterexamples.org/ https://counterexamples.org/, although if I skim the issues seem to have been fixed since then.
  - 2y ago