TypeScript: It’s getting unpredictable if you hit the language’s “design limits”

If you hit the limits of TS’s inference capabilities it doesn’t necessarily react — as you would hope for — with a graceful degradation (what would be a compiler error “Type instantiation is excessively deep and possibly infinite.(2589)” in this case) but its behavior gets possibly chaotic. I describe here some specific experiences that I have made. Be warned in case you try to construct complex types.

In the example I present here (Playground), I have construed a (generic) convenience type type RangeOfNumbers<From, To> = ... that takes a lower and an upper limit and evaluates to From | From + 1 | ... | To - 1 | To, e.g. RangeOfNumbers<2, 8> evaluates to 2 | 3 | 4 | 5 | 6 | 7 | 8.

This type is complex in the sense that it builds on many other types. I couldn’t find a smaller example where a problem similar to the one I am going to describe here already occurs. However, this makes the problem with TS’s inconsistent behavior so insidious in my eyes. You start to code with rather simple (type) constructions, everything works as intended and then after having written already a lot of code and after possibly having constructed dozens to hundreds of types it makes Boom! And if you are like me, you spend hours with searching the bug in your own code before you find out that the actual culprit is the compiler.

What happened? I have written some tests to convince myself that the mentioned type RangeOfNumbers works as intended (Playground: lines 672–677). Later on, with actual usage, when the numbers get bigger (or rather the ranges get broader), then (if you are beyond some unpredictable limit, here it is RangeOfNumbers<1, 21>) under certain circumstances that I try to reconstruct here TS gets kind of lazy and silently identifies your constructed type that should evaluate to some finite union of numbers with the type number. Note that RangeOfNumbers<1, 20> still works as intended. But even before (i.e. with already smaller ranges) inconsistent TS behavior starts: With RangeOfNumbers<1, 14> everything is still fine. With RangeOfNumbers<1, 15> the IntelliSense type info starts to disagree with the compiler (both my IDE and in the Playground environment): While the compiler still evaluates correctly (Playground: line 807), IntelliSense takes a different view (lines 803 and 804):

IntelliSense thinks the type of variable testRangeTest5_1 evaluates to `false`, while the compiler thinks different (line 807)

The most annoying behavior I have observed occured in my own IDE (IntelliJ) with the program I am currently working on. I cannot reproduce it in the Playground environment but it is connected to the same TS type RangeOfNumbers and I observed such behavior (also with other TS types) consistently: I define a const of a certain explicit type with some value and get no compiler complaint, i.e. the value is considered compatible with its explicitly assigned type. Later I change something in the code that is somehow related to usages (not the definition) of the type in question and suddenly the compiler changes its opinion and flags the value assignment as incompatible with its claimed type. Here are two screenshots of this behavior:

The variable testAtLeastOneKilledPieceCounter1 is assigned the value `true` and TS thinks this is OK (meaning that type `AtLeastOneKilledPieceCounter` works as intended). This view is confirmed by the following variable testAtLeastOneKilledPieceCounter2 that confirms that the type in question, `AtLeastOneKilledPieceCounter` is not evaluating to `number`. Note that an orange underline signals an unused variable, a red one an error.

Now the code is enhanced. Even though the definition/assignment of variable testAtLeastOneKilledPieceCounter1 remains unchanged, the compiler now thinks the unchanged type `AtLeastOneKilledPieceCounter` no longer evaluates to the respective union of numbers but to `number`. Former testAtLeastOneKilledPieceCounter2 that has now become testAtLeastOneKilledPieceCounter4 confirms that changed compiler view.

Ryan Dabler just has written an impressive article where he claims that TS’s isolated type system is Turing complete, i.e. with this type evaluation as computation you can compute everything that can be computed at all — in principle. I have to admit that I didn’t follow Ryan’s proof in detail since taking my observations into consideration TS is at most conceptually Turing complete. That is, if Ryan’s proof is correct, then TS’s type system is expressive enough to be Turing complete. Ryan mentioned a first restriction himself: Under certain circumstances (if your nesting of recursive types exceeds some unspecified limit), then TS complains with a “Type instantiation is excessively deep and possibly infinite.(2589)” error. This is roughly equivalent to restrictions of real computers (which have e.g. limited memory) in comparison to a mathematically defined Turing machine which has a two sides infinite tape as memory at its disposal. So, such an error is what I would call a “graceful degradation”. The issues that I have reported here are more severe (even though I would complain even in the “graceful degradation” case that the recursion limits are not configurable and ridiculously low).

What does this mean with respect to soundness and correctness?

It depends on your reference system: Either the whole TS language or just its type system. As for the whole language I suggest to apply this definition: A type system is sound if no program passes as error free that actually violates some type restrictions. A type system is complete instead if every error free program (w.r.t. typing restrictions) passes the compiler. As it is easy to understand, unsoundness usually is considered a more serious problem than incompleteness.

Even though the TS team sells unsoundness as a feature rather than a bug (a sound or “provably correct” type system is an explicit non-goal for TypeScript (Non-goals, point 3)), I don’t think that they were hinting to the type of issues I report here. Once I had a similar problem and reported it to Microsoft (see also this former article of mine): The reaction was disappointing to me. However, Ryan Cavanaugh, the head of Microsoft’s TS team, claimed that my observation were a case of a (more harmless) incompleteness, rather than one of (a more annoying) unsoundness. I disagree. I show for the case here (the confusion of a finite union of numbers with the type number) that it is simultaneously an instance of both, incompleteness and unsoundness, and claim in addition (without proof) that the case of the bug report is analogous:

Incompleteness: Assume, we have a variable of type RangeOfNumbers<1, 21> and try to feed it as a function parameter that is constrained to be of type 1 | 2 | ... | 30. Then the variable value is compatible with the restriction and still TS wouldn’t let it pass since it thinks the variable has type number what, in fact, is not compatible with the restriction.

Unsoundness: Assume we have a function parameter that we restrict to be of type RangeOfNumbers<1, 21>. If we actually feed in the value 0 for that parameter, then TS thinks it is OK since the parameter constraint evaluates to number, what in fact is compatible with 0.

The TS type system as an isolated calculus: As Ryan Dabler has showed (I assume he is correct), the type system alone is expressive enough to emulate any computer. In particular, it is expressive enough, to interpret type evaluations as arithmetic calculations. In fact, Ryan has suggested just this and I have implemented his ideas, partly to be able to build my convenience type RangeOfNumbers that I have introduced here (you can retrace the connections in the attached Playground example). The reported issues mean in this context that, e.g. arithmetic falsehoods, like 9428 > 9429 (line 654 in Playground) can be derived. Thus, the type system as a calculus is again unsound and incomplete anyway (because of the “Type instantiation is excessively deep and possibly infinite.(2589)” errors which I abbreviate as “recursion too deep” errors when talking about them in my example code).