[achou]

In type systems there's a tension between expressiveness, soundness, and comprehensibility. A sound type system must exclude all programs that have runtime issues, and, holding that constant, try its best to maximize expressiveness and comprehensibility of the programs that can be written.

But what about programs that can run fine but are excluded by the type system? They are censored. This is what's less visible until you actually try to build something substantial, pushing the boundaries of expression, performance, or scale. Then you'll find that a sound type system can become more and more of a straight-jacket. One that forces you to write code in ways that are limited by what its type designers could envision expressing (or could prove that was safe to express).

The trouble is that it's hard to know when you might reach the point where the type system begins to limit you. It might never happen, as you frolick happily within the walled garden. Or it might happen when you write your first line of code. In a large system that must deal with external requirements, it's something that in my experience becomes inevitable. That's not even touching upon comprehensibility, which becomes an increasing challenge for purely sound type systems as they attempt to increase expressiveness.

The biggest innovation of TypeScript is JavaScript. That is, TypeScript started with a huge established corpus of JavaScript that showed what developers wanted to express and how they wanted to express it. And, crucially, how popular various kinds of expression actually were in the developer community. This forced TypeScript to take practical expressiveness of millions of lines of JS seriously, that ordinarily would have been censored by type system design before the first line of code was written.

That's why it's entirely unfair to harp on TypeScript's unsoundness, without also exploring the corresponding gain in expressiveness and comprehensibility relative to other type systems.

BTW, this line of reasoning is the reason so many "sound" type systems also have their equivalent of "any": Rust has unsafe[1]. C# has unsafe[2]. Flow has any[3]. And all practical languages have strings, which are kind of a lowest common denominator when it comes to dealing with a type system that simply can't express what you need.

[1]: https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html [2]: https://docs.microsoft.com/en-us/dotnet/csharp/language-refe... [3]: https://flow.org/en/docs/types/any/