Everyday TypeScript: Type Soundness

• The goal of a static type system is to detect and prevent mistakes. But many statically typed languages have holes in their type safety: they'll allow some code that definitely isn't correct when we look closely. TypeScript is one such language.

• The technical term for this is "soundness", a term that comes from mathematics. A sound type system only accepts programs with correct types. If a type system accepts some programs that violate their stated types then we say that it's "unsound". This seems strange at first: isn't the type system's job to only accept correct programs?

• Let's examine a TypeScript example to see an example of unsoundness. We'll build up to the unsound operation in a few steps, starting with a simple array of strings:

• >

  let names: string[] = ['Amir', 'Betty'];

• We can assign our array to a new variable of type (string | number)[]. If an array contains only strings, then it seems OK to treat it as an array of string | number! This particular array of string | number just happens to have no numbers in it right now.

• Note: this code example reuses elements (variables, etc.) defined in earlier examples.

  >

  let unsoundNames: (string | number)[] = names;

• Our array variables have different types, but the underlying array is the same. What happens if we push a number onto the second array of type (string | number)[]? It seems like that shouldn't be allowed, because the number will also show up in the first array variable of type string[]. However, TypeScript allows this, violating the names variable's string[] type!

• >

  let names: string[] = ['Amir', 'Betty'];
  let unsoundNames: (string | number)[] = names;
  
  // This is unsound! It causes the "names" array to contain a number!
  unsoundNames.push(5);
  names;

  Result:

  ['Amir', 'Betty', 5]

• This is very bad, and unfortunately there's no way to fix it. All code in this course runs with TypeScript's strict mode enabled, but this is still allowed even in strict mode.

• We saw another example of unsoundness in an earlier lesson, though we didn't call it by name then. When we index beyond the end of an array, we get undefined out. This is true even if the type of the array is string[]!

• >

  const names: string[] = ['Amir', 'Betty'];
  const name: string = names[2];
  name;

  Result:

  undefined

• Again, TypeScript has allowed us to violate the static types. It allows name to type check as a string, but undefined is definitely not a string!

• This may trigger a crisis of confidence. Why add all of this static type machinery, and the additional tools required, and the complexity that we have to learn, if TypeScript still allows incorrect code in some cases? The answer is that TypeScript has made an intentional trade-off, like other popular statically typed languages.

• TypeScript was designed to work with existing web technologies. That includes all of the quirky JavaScript code that exists in the wild. TypeScript can successfully express the types of some very strange real-world JavaScript code that wasn't designed with static type systems in mind... but at what cost? One cost is that TypeScript's type system can't be designed for perfect soundness.

• There are many sound programming languages that compete with TypeScript. Yet TypeScript is the one that's most compatible with the existing ecosystem, so it became the most popular, which is surely part of the reason that you're here reading this.

• There's a conspicuous correlation between unsoundness and popularity. C, Java, C#, Scala, and TypeScript all have unsound type systems to varying degrees. Elm, Haskell, and Reason all have sound type systems.

• That comparison shouldn't be read as a value judgement, and we shouldn't assume that sound languages can't become wildly popular. No programmer in a static language would say "I'm glad that my type system allows some incorrect types!" The best we can say is "I accept the trade-offs that my language has made for now."

• The bad news is that TypeScript's soundness holes can cause real problems in real applications. But the good news is that those problems are relatively infrequent. For every soundness-related bug that sneaks through, TypeScript will probably save you from hundreds of "cannot read property of undefined" errors.