[ragnese]

That's not what soundness means in a type system. Of course untyped input has to be parsed and validated.

An unsound type system means that you can write code that compiles, but experiences a runtime error caused specifically by the types (not the values or the business logic conditions) not actually being compatible. The famous example is having an array of a subtype being used as an array of the supertype:

function doStuff(animals: Animal[]) { animals.clear() animals.push(new Cat()) }

const dogs: Dog[] = [new Dog()]

doStuff(dogs)

dogs[0].bark() // <-- type error

In a sound type system, that code would not compile because we know that you can't treat an array of Dog as an array of Animal in general.

[elevader]

I don't think that example would compile in TS either (not 100% confident though). The "issue" with TS is that everything type related completely disappears after the build step and that needs to be kept in mind in development. Some developers struggle with that, especially at the boundaries to external APIs/libs/whatever.

[ragnese]

> I don't think that example would compile in TS either (not 100% confident though).

I believe that code does compile by default.

If you turn on the strict flag, that exact code wouldn't compile. BUT, if you wrote a class method instead of a top-level function in the above snippet, it STILL would compile.

> The "issue" with TS is that everything type related completely disappears after the build step and that needs to be kept in mind in development. Some developers struggle with that, especially at the boundaries to external APIs/libs/whatever.

I agree that a lot of devs struggle with that, but that's not really relevant to the type system being sound, and has nothing to do with the example I wrote. It can be proven to be incorrect at compile-time, so the compiler should reject it.

In fact, most of the "hardcore" statically typed languages you hear about have full type-erasure: Haskell, Rust, ML, etc. Yet, they have reputations for very strong and strict static type systems. None of those languages would let the above garbage compile.