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.

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.

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

There still "weak" points, where incorrect typing can be introduced, e.g. incorrectly written bindings. Regarding data from HTTP call in theory they can be cast to any type abusing `external` keyword which is meant for binings. But common and recommend approach is to write codes. Codec would perform all the necessary checks to ensure that the data are in correct shape to satisfy the type restrictions. You can see some examples here: https://github.com/greyblake/from-typescript-to-rescript/blo...

For what it's worth, Elm does the runtime checks by means of forcing you to write "de/encoders" that must match the types.

So does TypeScript if you have strict settings. Your input data will be untyped and you will be forced to determine its type before you use it.

TypeScript does nothing like that with any strict settings, because it doesn't provide any JSON parsing alternative, so that is always unsafe.

I bet there are runtime checkers that use some kind of reflection, that would be the next best thing. But I also bet that those force you to annotate/decorate everything.

I do not know of a way to make this a compiler error:

    const user: User = JSON.parse(…);

You can redefine all definitions from lib.d.ts and similar. In my projects, parse function returns unknown, so I need to parse/validate/decode it in runtime to satisfy types.

At this current time rescript is still basically ocaml, and accepts ocaml syntax. So it has the Ocaml typechecker.