4 ms·

Thank you for the feedback. I think I should rename the "Sound Mode" to something more honest. "Strict" is already taken so I should think of a better name. Mak

by mohsen1 5mo ago

Thank you for the feedback. I think I should rename the "Sound Mode" to something more honest. "Strict" is already taken so I should think of a better name. Making tsz compatible with tsc and making it sound is mathematically impossible. The history of this stuff (https://hegel.js.org https://hegel.js.org) is telling. If you really make a sound JS checker, nobody will really use it unless you build an entire ecosystem as big as npm with it. TypeScript's decision to embrace existing npm ecosystem and layering .d.ts on top was a very practical decision that made it so successful.

tialaramex 5mo ago
> TypeScript's decision to embrace existing npm ecosystem and layering .d.ts on top was a very practical decision that made it so successful. This is basically the same argument made for C++ and I think it's not a very solid one. We know this worked, but that's not evidence that alternatives couldn't have succeeded. I think in a world where Queen never happened the prevailing wisdom would be that someone like Farrokh Bulsara (Freddie Mercury) can't be a rockstar because that seems ridiculous. Actually speaking of royalty, Prince is an even more extreme case. You cannot use numeral-letter substitutions in song titles, that's something for kids and won't... oh unless you're Prince. Yeah, no, "Nothing Compares 2 U" is fine Prince, thanks.
- mohsen1 5mo ago
  In the Sound Mode page I mentioned that I have some ideas around this. What if we could take .d.ts and project a sound version out of it? How feasible that can be is unclear but the biggest unsoundness criminal is `any` which is relatively safe to project it into `unknown`. And method binvariance stuff are also not impossible to project something more sound out of it. My goal with tsz is to make it practical and useful. I know how difficult it is to convince a tsc user to try something not officially from Microsoft
nextaccountic 5mo ago
> TypeScript's decision to embrace existing npm ecosystem and layering .d.ts on top was a very practical decision that made it so successful. I don't think this is the problem. I mean, ok, the first part of the problem is that typescript can't or won't represent at the type level some real world Javascript constructs. But that's understandable since Javascript can get arbitrarily complicated. (you could do a survey on npm and make a type system strong enough for all existing libraries, but this would probably be too complicated to use) So this is not by itself too bad if, for each instance of non-representable APIs, you wrote a wrapper library that called the bad library but gave you a perfectly good API to work with. Similar to how in Rust you are supposed to wrap unsafe libraries with a safer, higher level API on top. (except it' s not about memory safety, but type safety. but the same reasoning applies, it's just lower stakes since UB is not involved) Bur the other, more fundamental problem is that for some godforsaken reason, Typescript decided it was okay to lie with types. Some operations return the wrong type rather than a more honest type. This is not caused by the fact that Typescript has to work with libraries in npm, it's entirely self inflicted. Elsewhere in the thread someone gave an example: stringArray[0] has type string when it should be string | undefined. This (and all other instances of deliberately lying with types) is why Typescript is unsound. Here's a list of things that cause unsoundness (not sure if complete) https://effectivetypescript.com/2021/05/06/unsoundness/ https://effectivetypescript.com/2021/05/06/unsoundness/ If all those things are patched up, Typescript can be in general mostly sound, even though it has to work with npm libraries and even though you need to trust other people's .d.ts files. To gain full soundness on your application code, you just need to write wrappers to work around the most egregious cases (which should be a minority). Again, the same situation as Rust is supposed to be: it's in general sound but when you need to interact with bad stuff you write a wrapper. (Note: Rust has its shares of unsoundness, but contrary to Typescript, Rust has a plan to eventually patch them up, even if this causes incompatibilities down the line)

by mohsen1 5mo ago

tialaramex 5mo ago

> TypeScript's decision to embrace existing npm ecosystem and layering .d.ts on top was a very practical decision that made it so successful. This is basically the same argument made for C++ and I think it's not a very solid one. We know this worked, but that's not evidence that alternatives couldn't have succeeded. I think in a world where Queen never happened the prevailing wisdom would be that someone like Farrokh Bulsara (Freddie Mercury) can't be a rockstar because that seems ridiculous. Actually speaking of royalty, Prince is an even more extreme case. You cannot use numeral-letter substitutions in song titles, that's something for kids and won't... oh unless you're Prince. Yeah, no, "Nothing Compares 2 U" is fine Prince, thanks.

mohsen1 5mo ago
In the Sound Mode page I mentioned that I have some ideas around this. What if we could take .d.ts and project a sound version out of it? How feasible that can be is unclear but the biggest unsoundness criminal is `any` which is relatively safe to project it into `unknown`. And method binvariance stuff are also not impossible to project something more sound out of it. My goal with tsz is to make it practical and useful. I know how difficult it is to convince a tsc user to try something not officially from Microsoft

nextaccountic 5mo ago

> TypeScript's decision to embrace existing npm ecosystem and layering .d.ts on top was a very practical decision that made it so successful. I don't think this is the problem. I mean, ok, the first part of the problem is that typescript can't or won't represent at the type level some real world Javascript constructs. But that's understandable since Javascript can get arbitrarily complicated. (you could do a survey on npm and make a type system strong enough for all existing libraries, but this would probably be too complicated to use) So this is not by itself too bad if, for each instance of non-representable APIs, you wrote a wrapper library that called the bad library but gave you a perfectly good API to work with. Similar to how in Rust you are supposed to wrap unsafe libraries with a safer, higher level API on top. (except it' s not about memory safety, but type safety. but the same reasoning applies, it's just lower stakes since UB is not involved) Bur the other, more fundamental problem is that for some godforsaken reason, Typescript decided it was okay to lie with types. Some operations return the wrong type rather than a more honest type. This is not caused by the fact that Typescript has to work with libraries in npm, it's entirely self inflicted. Elsewhere in the thread someone gave an example: stringArray[0] has type string when it should be string | undefined. This (and all other instances of deliberately lying with types) is why Typescript is unsound. Here's a list of things that cause unsoundness (not sure if complete) https://effectivetypescript.com/2021/05/06/unsoundness/ https://effectivetypescript.com/2021/05/06/unsoundness/ If all those things are patched up, Typescript can be in general mostly sound, even though it has to work with npm libraries and even though you need to trust other people's .d.ts files. To gain full soundness on your application code, you just need to write wrappers to work around the most egregious cases (which should be a minority). Again, the same situation as Rust is supposed to be: it's in general sound but when you need to interact with bad stuff you write a wrapper. (Note: Rust has its shares of unsoundness, but contrary to Typescript, Rust has a plan to eventually patch them up, even if this causes incompatibilities down the line)