Type-checking unsoundness: standardize treatment of such issues among TypeScript team/community?

[henryptung]

In various issues, I've seen a tendency to treat some of TypeScript's type checking limitations (see #5786, #7933, #9765, #3410 (comment)) closed as By Design or Design Limitation. (There are more, but I think other folks here know more about them than I do.)

A few arguments I want to posit about this:

• TypeScript is better than nothing/straight JS (I think most here would agree on this)
• TypeScript's mission is to layer type-checking on top of JavaScript coding (taking this from TS's adherence to minimalism on top of ECMAScript, aside from types)
• Its weaknesses can become worse than nothing, with time. Reasoning:
  • Existence of TypeScript reduces community drive to implement another type-checked JS-based language competitor (since one already exists)
  • Anchors the community to both the strengths and the limitations of the TS codebase, due to the above
  • TypeScript type fundamentals only become harder to change with time (more language support = more legacy code); I personally believe there is a cliff here we may have already passed, but I really hope we haven't

What I'm interested in knowing is whether the TypeScript community/team consider type-checking unsoundness as something that should be fixed, given the opportunity. I can see a few different ways to handle these issues, and I'm very interested to hear from the TypeScript team which options they would lean towards (or none of the below):

1. Keep long-lived tickets open for such limitations, with the goal of implementing a fix
   • Pros:
     • Collect use cases/examples in one place
     • Provide a meter to community pressure to implement a fix
     • Tickets can collect discussion on design/impl proposals, pros/cons/lessons learned of previous attempts, etc.
     • Active tickets attract attention, and motivating developers to spend their free time on it
   • Cons:
     • Old ticket "noise"
     • Tickets grow stale (lack of interest?)
     • Easy for a few folks to derail one ticket's discussion
     • Splintering of codebase (not sure when next-major-release branches are cut, but this could become difficult to maintain if the PRs come at the wrong time)
2. Add a compiler flag to warn on known type unsoundness
   • Pros:
     • Probably easiest fix/patch on current code
     • Smooths over a chunk of current developer needs (run the strict build occasionally, review warnings to make sure benign)
   • Cons:
     • Risks stagnation (solving some developers' needs also proportionally reduces the pressure for a proper fix)
     • Not discoverable (warnings wouldn't be on by default, since they'd almost certainly be filled with false positive noise)
3. Don't do anything, treat current design as dogma (but document unsoundness in one place)
   • Pros:
     • Easiest
     • Aligns with mission? (hopefully not)
     • At least provides visibility in one place (i.e. don't-do-this list)
   • Cons:
     • Stagnation
     • Subverts mission? (maybe)
     • Troubling future regarding treatment of "legacy" style bugs
4. Really don't do anything
   • Pros:
     • Easiester
   • Cons:
     • Really?

[zpdDG4gta8XKpMCd]

To my eye TypeScript is only about 80% sound due to:

• bi-variant parameters
• simplified generic instantiation
• implicit coercion
• void matching any result type
• implicit omission of parameters

I think there are only 2 questions to that and everything else is irrelephant:

• budget: Who is going to be paying for fixing it?
• mainstream language for average enthusiasts: Who is going to thank you for fixing it?

But if a problem cannot be fixed it at least should be noted somewhere. There was an idea to make a resource for all known shortcomings and gotchas called ByDesignScript

There is certainly a niche for a better type-checker, but it can't be done as a pet project, it needs some dedication measured in $$$, so we back to the question 1.

[henryptung]

@Aleksey-Bykov I understand the frustration, but I don't want to lean too hard on cynicism here. I can see a motivation in "dev encounters bug that took 2 hours to fix, wants to avoid encountering this bug 10 more times in the future", as well as "dev just likes working on compilers". That said, I agree monetary sponsorship would be helpful getting these fixed - but the aim of my ticket is not necessarily to advocate one way or another, but to canvass opinion and make sure the harder choices about long-term type system design get answers/decisions earlier, rather than later.

[zpdDG4gta8XKpMCd]

I am just being realistic here. You cannot change the direction of the vector of where TypeScript is going and you can't change the magnitude of it. You can only slightly tune it and make things happen a bit earlier.

I am too very much like you all up for TypeScript to be a sound ground for frustration free development. And from what I see, the design team is all reasonable people who want the same. As I said there are only 2 things that drive their decisions: resources and priorities. You can be mad about it, like I was and may people are, your choice. You can take a step forward and do something about it and even submit a couple of pull requests, it's all good things. But when it comes to the core features and critical paths, nothing you can do, but vote and wait. The vote and discussion part is handled by github pretty well. What else can you do?

Let's imagine, you got very motivated to get those frustrating issues fixed. You worked hard to make your point clear and get as many people as you can to think the same way. You made it clear to the design team that there is a certain percentage of people who are very frustrated by the current capabilities of TypeScript. You even got heard and talked back to in a very nicely manner. Then what?

There are things that just need time to progress naturally. You can't have feature F without feature E. And despite you need F very bad you won't get it until feature E is done which is in a long line of D, C, B and A.

I am not trying to talk you out of what you are doing. Just sharing my view on what the situation is.
I am looking forward to seeing the details of the proposition you are going to make. Good luck.

[zpdDG4gta8XKpMCd]

On a constructive note, you can get a lot of things fixed by running your own rules to check the code more thoroughly. You can do it on your own or as a part of a collective effort via contributions to TsLint. All in all this is the fastest way to get what you are missing. There is a good chance something that you miss is already there.

[mhegazy]

Just few thoughts, hopefully it does not sound like incoherent rambling..

TypeScript tries to overlay a type system on JavaScript code. So while safety is an important requirement, usability is another important one. Striking a perfect balance between the two is impossible, I would argue.

Argument bi-variance, functions assignablity allowing sources with less arguments than targets, allowing non-void types to be assigned to void, this having a type any, type assertions representing up and down cast, and the existence of type any and how it behaves were all design decisions that the design team made deliberately. We can go into the details of why each has been made separately, and you can find some of these documented either in the design meeting notes, or in the FAQs like parameter bi-variance. These decisions were made with understanding of limitations, and expectations of drawbacks.

The reason the referenced issues were marked as "by design" or "design limitation" is really because they match the intended design, however imperfect it may be, and not to sweep them under the rug, or ignore them. The reason the issues were closed, is that there were no plan to change the design. leaving them open would indicate otherwise.

A lot of these decisions were done after implementing a change one way, then experimenting with real world code bases, looking at reported errors from the compiler, and looking at what percentage of that are real bugs. this is not really an exact science, nor an objective measurement. but a lot of the changes that were thought to be pure goodness proved to be otherwise when put to the real-world-code test suite.

Now... design decisions can change. New scenarios, or ones that were not considered before could surface forcing to reconsider. So these are not really set in stone.

We did consider a new flag for a "stricter" version (see #274), but it was not clear what that means, and if it would be an ongoing tighten effort or it would stop, and whether you would have --strict: level3 vs. --strict: level5. it also was not clear if everybody wanted to opt into what we have deemed "strict". it was not even clear what was strict and what was just pedantic.

We have shied from flags that change the behavior of the type system; almost all the flags we have today are to add additional checks or suppress error reporting for certain errors. The rational is to limit option fatigue, and more importantly not to fork the language into different "modes".

Also the flags we have added to "tighten" things up are things we like to think of as "transitional"; meaning that we would recommend all users to move to, for instance --noImplictAny, --noImplictThis and --strictNullChecks.

I do believe the community has a big role to play in shaping the road map of an open source project in general and of TypeScript specifically. The best way to move an issue or a feature request forward is to have a clear and concise proposal[1], exploring possible implementation options, and even experimenting with an implementation to demonstrate the cost/benefit of the change. Multiple features of the TS compiler today came to existence this way, for instance the JSX support was done in a separate fork before merged into the main compiler code base.

[RyanCavanaugh]

What I'm interested in knowing is whether the TypeScript community/team consider type-checking unsoundness as something that should be fixed

Just speaking specifically to this point, 100% soundness is not a design goal. Soundness, usability, and complexity form a trade-off triangle. There's no such thing as a sound, simple, useful type system.

I like to speak to a simple example:

// A
function addDogOrCat(arr: Animal[]) {
  arr.push(Math.random() > 0.5 ? new Dog() : new Cat());
}

// B
function hasCat(arr: Animal[]) {
  return arr.some(e => e instanceof Cat);
}
const x: Mammal[] = getMammals();
const y = hasCat(x);

// C
const z: Cat[] = [new Cat()];
addDogOrCat(z); // // Sometimes puts a Dog in a Cat array, sad!

You can solve this problem one of three ways.

Simple, Usable, Unsound

How TypeScript works today.

Simple, Sound, Unusable

Make the type system reject all subtype substitutability. This makes nearly every API unusable, for example Node#addChild would reject anything except a Node.

Sound, Usable, Not simple

Have a notion of mutable/non-mutable objects with co- and contra-variance annotations for generic assignability, like what C++ did with const and C# did with in / out. const correctness is infectious, so all TypeScript libraries would have to be correctly typed for mutability (consider how good people are at writing definition files are today). You'll also need an opt-out system like for things like caches, and everyone will need to agree about what constitutes modifying an object and what doesn't (harder than you'd think).

---

That example also leaves performance of the compiler aside; there are some cases where we could be closer to sound but at the cost of a 10x or 100x decrease in compiler performance. See recent threads on HN about pathological performance in the Swift compiler for how this happens in practice (https://news.ycombinator.com/item?id=11573213, https://news.ycombinator.com/item?id=12108876)

It can be easy to think of soundness as the only goal, but in practice this isn't a good way to make a language. There aren't any low-hanging "fixes" left, just trade-offs that make things harder to use or more complex or significantly slower.

[zpdDG4gta8XKpMCd]

You dont need to opt out, you just make the Cache class implement 2 different interfaces that dont have to be together under the same interface: CacheIn, CacheOut

[henryptung]

@mhegazy @RyanCavanaugh Regarding trade-offs of design and usability, that is compelling and I'm not trying to criticize those decisions - I have not done the work you folks have done to verify, and I will trust your judgment without any contrary evidence of my own. However, I think we've been arguing just (1) - I would like to address (2) and (3) as well.

For clarification: (2) isn't about changing compiler behavior, but adding a verbosity flag to log known unsafe type conversions (e.g. function argument covariance). I don't think this would be either hard to implement, a serious performance hit (probably just logging a check already performed), or a change contrary to compiler behavior consistency. I could believe it to be extremely noisy and not actually useful though; I won't be able to verify that until I do some testing there, but may try on parameter covariance and report back here.

For (3), this is really just documentation, nothing else. Right now, encountering such errors is silent, (potentially) painful to debug, and somewhat disheartening once the root cause is found (since I think many devs begin using TypeScript expecting type soundness, considering the name of the language after all 😄). A specific documentation-about-unsoundness page would give me (and hopefully some others like me) some confidence that I can avoid wild goose chases in the future, by consulting this page first for possible causes outside-the-box.

(spam additions about small notes)

• 100% agree const-correctness isn't ideal, because it's a concern that reaches into implementations, and forces them to be very verbose about their interface (i.e. const-or-not on every property/method). Instead prefer the readonly modifier as currently impl'd, since (with proper usage) it achieves the same with much smaller (only opt-in) cost. You do have to trust the implementation and its semantics, but you had to do that already.

• I can't really parse this line:

  Make the type system reject all subtype substitutability. This makes nearly every API unusable, for example Node#addChild would reject anything except a Node.

  What is "all subtype substitutability", and why would Node#addChild take a non-Node? If you're saying that an Element or Text would no longer be a Node, of course not - that would reduce any type system to laughable simplicity and uselessness.

• Arrays example: Few notes here.

  • Yup, arrays are hard. So is every collection, because it has its type parameter in both covariant (return-value, read) and contravariant (parameter, write) uses. A true Mammal[] or Animal[] is no-variant. You can still put Cats or Dogs into it, you just don't get any promises on read except that it is a Mammal or Animal. Java implemented the same Cat[] -> Animal[] covariant assignability; not sure how others feel, but I think this was a mistake that required runtime-type-checking of arrays (its way to patch the problem at hand). This, however, wasn't possible with type-erased generics, so generic arrays are now unsafe forever; (partially) as a result, List<T>s are much more common in Java APIs than arrays.
  • Speaking also about Java: its fix here is to ask functions writing Ts into a collection to accept an Array<? super T>, and those reading Ts to accept an Array<? extends T>. Agreed though that's a big feature that's not necessarily the ideal solution. (Java's type system is both profoundly expressive and profoundly verbose/unreadable once you get into the weeds.)
  • This example could also be solved by writing returnDogOrCat instead, which would probably be a more usable API anyway (functional vs. side effects). Kind of a straw-man though; requiring callbacks and pure-functional style might eliminate most cases like this, but would also be prescriptive and possibly bad for performance.
  • I find it profoundly strange that arrays are used as the function argument example - arrays have a type issue of their own, and most familiar with e.g. Java know that Mammal[] -> Animal[] is problematic at best, and why. Instead, I think that the function parameter covariance has far-reaching side effects due to TypeScript's duck typing - this indirectly "solves" the array typing problem, because now Mammal[] -> Animal[] is made legal by the change, which in turn prompts the use case to begin with. The whole argument feels a little like pulling myself up by my own socks, so to speak.

[DemiMarie]

I normally use languages which have the property "If it type checks (and you don't use unsafe functions), and it crashes, that's a bug in the implementation". I like this property a lot. But I don't want to end up with Java-esque verbosity – that is ugly.

[rossberg]

@Aleksey-Bykov, TypeScript is already unsound in its most basic subtyping relation: the fact that {a: Sub} < {a: Super} when Sub < Super is a gaping soundness hole because all object properties are mutable by default in JavaScript. Unfortunately, it is pretty much impossible to change that without making the type system incompatible with a large majority of JS APIs and applications.

[DemiMarie]

@rossberg-chromium How does Facebook's Flow handle this? It claims to be sound.

[RyanCavanaugh]

Flow isn't perfectly sound and doesn't claim to be; e.g. #15453 (comment) , https://github.com/facebook/flow/blob/c93897cd9d6ac6db703c8b9f0536f440a03d54f4/website/en/docs/lang/types-and-expressions.md#soundness-and-completeness- , facebook/flow#3702 (comment) etc.

[kitsonk]

Well to point out they don't say they are completely sound in the documentation. They, like you and Mohamed pointed out for TypeScript, make tradeoffs when JavaScript makes full soundness unusable. They say their design goal is to prefer soundness over completeness, unless soundness is too unusable. TypeScripts design goals are not as constraining, in my opinion, allowing room to achieve a different objectives.

Ultimately when dealing with a language that is weakly typed and specifically designed to lack a type system, it is wholly unsurprising you have to pick your battles.

[RyanCavanaugh]

Just to be clear, our default position is also soundness (trivially, we could let you call substr on number | strings, or pass Bases in place of Deriveds, or assume optional properties are present under strictNullChecks, etc.) over completeness. People who want a JS type system that is 100% complete and 0% sound can just choose to use no typechecker whatsoever, after all 😉