Home > Blockchain >  TypeScript type narrowing seems to make incorrect assumption
TypeScript type narrowing seems to make incorrect assumption

Time:12-11

There are no TypeScript errors with the following code even though line 4 accesses a property on x that does not exist.

type T = {num1: number, num2: number} | {str1: string, str2: string}
let x: T = {num1: 1, num2: 2, str1: 'hello'};
if('str1' in x) {
  console.log(x.str2.toUpperCase());
}

Is this a bug with TypeScript or can someone point me to documentation explaining this behavior? It seems like either TypeScript shouldn't allow the assignment on line 2 or it shouldn't assume that 'str1' in x implies 'str2' in x.

CodePudding user response:

From a pure soundness perspective, the assignment is correct and in operator narrowing is incorrect. From a pragmatic perspective, in operator narrowing is very useful and the assignment is not. There's a mismatch in these two features, and so you've presented a nice example of TypeScript code for which neither type purists nor idiomatic JS coders would be particularly happy with the behavior of the language.


First let's look at the assignment

let x: T = {num1: 1, num2: 2, str1: 'hello'};

According to structural typing, the initializer for x is definitely a value of type T, and so is {num1: 1, num2: 2, str1: true, randomThingy: "x"}. Extra properties don't violate a type.

But TypeScript does perform excess property checking as a sort of linter rule to catch situations where people are throwing type information away. When you assign const x: {a: string} = {a: "", b: 0}, you are throwing away information about the b property because there is no way for the compiler to recover it; the compiler will forget about b entirely. On the other hand, const y = {a: "", b: 0}; const x: {a: string} = y; is fine because even though x doesn't know about b, y still does. The excess property checking rule is a nod to pragmatism and not type safety.

This rule sometimes makes people think that object types in TypeScript don't allow extra properties, and that they are "exact types" as requested in microsoft/TypeScript#12936. But TypeScript does not have exact types, and the excess property checking rules don't kick in everywhere people think they should.

One such place is when you are assigning to a type like T, a union type which is not a discriminated union. The compiler does not split up the union into its members before performing excess property checking. As long as a property is expected in at least one member of the union, the compiler is happy with it. There is a longstanding open issue at microsoft/TypeScript#20863 asking for this to be changed, but for the foreseeable future this is how it is.

So the assignment is fine if you care mostly about type safety, but not fine if you care about exact types.


Now let's look at the narrowing

if('str1' in x) {
  console.log(x.str2.toUpperCase());
}

This is clearly not sound behavior. Object types in TypeScript are not exact, after all, so if you know that "str1" is a key of x you cannot logically conclude that "str2" is also a key. If you care a lot about type safety, this is very unfortunate.

On the other hand, it is very useful. Even though you can't technically say that "str1" definitely implies the presence of "str2", the correlation between them is probably very strong. Generally when people check for properties only known to exist in one member of a union, they do it because it really does let them discriminate the union in practice, if not in theory.

In microsoft/TypeScript#15256, the pull request that implemented in operator narrowing, there is the following comment by the dev lead for the TS team:

We considered the soundness aspect and it's not very different from existing soundness issues around aliased objects with undeclared properties. ... The reality is that most unions are already correctly disjointed and don't alias enough to manifest the problem. Someone writing an in test is not going to write a "better" check; all that really happens in practice is that people add type assertions or move the code to an equally-unsound user-defined type predicate. On net I don't think this is any worse than the status quo (and is better because it induces fewer user-defined type predicates, which are error-prone if written using in due to a lack of typo-checking).

So in operator narrowing is definitely a case of pragmatism winning out over soundness.


And there you have it... pragmatically speaking nobody would assign a weird union-straddling value to x, and it would be nice if the compiler could warn you when you did. And technically speaking it's wrong to use k in o to imply anything about a key other than k, and the compiler shouldn't do it.

Stepping back, though, this is only really a problem for purists. TypeScript's type system is not fully sound, and is not intended to be (and trying to do that with something that compiles to JavaScript is a "fools errand" according to the same dev lead). The first design goal of TypeScript is to catch probable bugs, and apparently it's rare for someone to accidentally shoot themselves in the foot the way this example does.

The fact that one part of the language favors soundness and another favors pragmatism can be seen as pragmatism of language design: soundness is great to the extent that it helps people write error-free programs, but it will be discarded in favor of something else if it hurts more than it helps. Quoting again:

Ultimately, type systems are tools we've created to help us write correct programs. Provable soundness is a proxy measure for that effort. If your program, by construction, only observes correct types at runtime, then whether or not a computer can prove that that is the case is an academic exercise in both meanings of the phrase.

And that means if you want to see something about this example change, you would have to make the case that mistakes like this are more common than the TS team thinks. Generally with real-world code examples from popular packages that run into it.

  • Related