Dan Vanderkam

> 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)

So 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.…

I think if you're writing code from scratch, this doesn't really apply -- I'm talking about writing a toy language that doesn't use any libraries at all.

(I'm aware of all the terrible experiences people have with TypeScript in the NPM ecosystem. But it's a big, mature tool and you can use it in more than 1 way.)

I just noticed the 'deno check' command I'm using turns strict mode on by default, so that's good.

https://deno.land/manual@v1.4.1/getting_started/typescript

All gradual type systems in production use are unsound because they have to interoperate with untyped code, and the dynamic checks to make it sound are too expensive.

But code written from scratch doesn't have that issue. I'd be interested in a counterexample -- is there a code snippet that passes the strict mode of the compiler, and doesn't interoperate with untyped code, but produces an unexpected runtime error?

I guess by "unexpected" I mean at runtime, and operation is performed on a value which is not allowed, and the program fails

I googled and found this -- https://effectivetypescript.com/2021/05/06/unsoundness/ -- not sure I agree with some points, e.g. array out of bounds isn't unsoundness! The OPERATION is legal, but the data isn't, which isn't something that any type system will tell you.

Similar to divide by zero -- a runtime error does not imply unsoundness.

TypeScript's type system is unsound in a mathematical sense: https://effectivetypescript.com/2021/05/06/unsoundness/ Though this has little bearing on practicality which is probably why the original comment is at the bottom of the pile.

He's also using a stricter mathematical definition of "type safety" whereas tRPC means it in the colloquial way it's used in the TypeScript ecosystem (that is, a fully typed interface between client and server, ideally that's non-duplicative and inferred directly from your code instead of being manually defined).