On: Node.js adds experimental support for TypeScript

[cstrahan]

No, TypeScript is not unsound because it uses structural typing.

A language has a sound type system if every well-typed program behaves as defined by the language's semantics during execution.

Go is structurally typed, and yet it is sound: code that successfully type checks is guaranteed to abide the semantics of the language.

TypeScript is unsound because code that type checks does not necessarily abide the semantics of the language:

  function messUpTheArray(arr: Array<string | number>): void {
      arr.push(3);
  }
  
  const strings: Array<string> = ['foo', 'bar'];
  messUpTheArray(strings);
  
  const s: string = strings[2];
  console.log(s.toLowerCase())

`strings` is declared as a `Array<string>`, but TypeScript is happy to insert a `number` into it. This is a contradiction, and an example of unsoundness.

`s` is declared as `string`, but TypeScript is happy to assign a `number` to it. This is a contradiction, and an example of unsoundness.

This code eventually fails at runtime when we try to call `s.toLowerCase()`, as `number` has no such function.

What we're seeing here is that TypeScript will readily accept programs which violate its own rules. Any language that does this, whether nominally typed or structurally typed, is unsound.