Type soundness is overblown. A type system doesn't need to be sound to be useful, and the pragmatic approach taken by TS has turned out to be really useful.

(In the old days, type systems were just purely about correctness, so soundness was key, but those days are long past us, we depend on type systems for many different things now)

In my experience with TS, its unsoundness was very frustrating. If you use it as a replacement for JSDoc where type ascriptions are more like recommendations, sure, but I like to have more confidence than that in a type system. FlowType is much better in that regard. Scala.js has been the best for me so far.

I have a feeling you're talking about an old version of typescript. Versions 2.2+ (currently 2.3.2) are sound (but not fully so, just like flow) with the right flag(s).

Here's the description of the "strict" compiler option that goes a long way to make your program more reliable :

"Enable all strict type checking options. Enabling --strict enables --noImplicitAny, --noImplicitThis, --alwaysStrict and --strictNullChecks."

Typescript (even with all those options on) isn't even close to sound.

Some of the soundness issues are by design (making directly overlayed JS code reasonable to type/interface with), some are due to 'taking too much time/design complexity if implemented'.

I won't go into them one by one, but you can jump into most of the issues here to get a sense:

https://github.com/Microsoft/TypeScript/issues?utf8=&q=Sound...

https://github.com/Microsoft/TypeScript/issues?utf8=&q=unsou...

I won't take a position on the matter other than to say that it's a tricky balance and the TS team are at the very least extremely clear in saying that you should not be looking for a high degree of soundness here (JS interop is a higher priority).

If those things are important, I would recommend Scala.js or PureScript or... anything more self contained (and remember that they're still ultimately dynamically typed on the JS boundary, just not inside the language).

Here's the TS team explaining their position themselves:

https://github.com/Microsoft/TypeScript/issues/9825#issuecom...

https://github.com/Microsoft/TypeScript/issues/13003 (not the most cordial commenter unfortunately)

Oh I know! You also can't control variance and it can display bad behaviors once in a while.

Overall though, getting bitten by the unsoundness is fairly rare , imo.

When I started using Typescript (whilst at the time using Scala, Clojure and Python day to day), I ran into soundness issues constantly (daily).

I think I wrote a lot of code assuming that the type checker was sound and could check my abstractions, only to find that it wasn't and it couldn't.

If it were more sound, I would rely on the language to do more checking.

I don't get bitten as much any more, but I'm pretty sure that's mostly because I know what tradeoffs the language is making and I use other mechanisms to ensure safety.

I used 2.1, it has all the same flags, and I did turn them on because they're not enabled by default. It's completely insane without those flags, but even with them enabled I still ran into many surprises. For example, like the other poster mentioned, its handling of variance is simply appalling.

And no, Flow is MUCH more sound, I have worked with both. Flow's limitations tend to be false negatives (code that should ideally work does not compile as is) whereas Typescript's are false positives (fails to detect type errors).

I'm much more bothered by TS's lack of separate compilation (errors tend to cascade, but this is to be expected from a structural rather than nominal type system).

The killer app for type systems has always been code completion.

   has always been code completion.

I disagree. Code completion is overrated and only of marginal importance in the production of high-quality code. The key advantages of types are:

- Enabling ahead-of-time compilation resulting in efficient code.

- Guarantees on the absence of specific classes of bugs. (This requires soundness.)

- Aiding verification. Types provide a rough classification of program behaviour which drastically simplifies verification. If you don't have types, your program logic needs to make typing information explicit in assertions.

1. Nope, as proven that many people use JavaScript in the first place.

2. Type systems have always been super limited in the kinds of bugs they can eliminate, even with "soundness".

3. This sounds like a type theorists point that is completely detached from most programming experiences.

(1) I'm not sure I understand point. JS has long been without alternative, that's why JS has seen such a massive uptake. Moreover all JS alternatives, from TypeScript to Scala.js to Elm to Flow are adding types.

Anyway JS's popularity is orthogonal to questions about efficient compilation. Types drastically simplify those, for you can work out at compile time how much memory needs to be allocated for each sub-expression of the program under execution. If you don't have types, you can only do that at run-time, and need extremely complicated JIT compiler technology to make this moderately performant.

(2) Sure. Still extremely helpful, all the more so, the bigger the software. If you don't have types to do this, you will have to find those bugs by testing -- much more labour intensive.

(3) Detached, maybe, but still true. To paraphrase Sutton's law: I'm detached from the toils of contemporary bread/butter programmers and look at verification because that's where the interesting open problems are.

For anybody reading this and nodding, here are a few unsoundness samples from Typescript: https://news.ycombinator.com/item?id=14475818

Flowtype isn't sound either. I don't know where this misapprehension comes from or why people keep repeating it; if you simply try to induce an unsoundness in Flow you'll succeed after about 30 seconds of trying.

An actual sound type system built on top of regular JS would be unusable - you'd have to disallow almost everything. The language is too "dynamic" to become properly sound.