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

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):

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)
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)
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
Really don't do anything
- Pros:
  - Easiester
- Cons:
  - Really?

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.

Aleksey-Bykov

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.

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.

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.

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.

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.

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

Mohamed Hegazy (@mhegazy)

Mohamed Hegazy (@mhegazy) Ryan Cavanaugh (@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.

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.

Aleksey-Bykov

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.

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

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.

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.

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 😉

jeeze TS syntax sucks too... you guys clearly missed your turn on the way here

TS is a superset of JS so JS syntax is a part of it not much anyone can do about it, unless we start all over off 1995

ShalokShalom (@ShalokShalom)

unless we start all over off 1995

And many many many many people have attempted this. I am not sure how well that is going for them. Many people are still angry at Google for spending time making a Dart runtime, specifically blaming Google wasting years of development effort starting off 1995 again instead of improving what was already there.

No matter what pure research says, I have learned time and time again that pragmatism wins the day. Look how long it took to get away from quirks mode...

ShalokShalom (@ShalokShalom)

Could you explain the differences - in specific the advantages of Typescript - to Fable?

I am sure there are far more capable people than me to do that. I am not sure what your point is.

Ryan Cavanaugh (@RyanCavanaugh)

There are literally hundreds of compile-to-JS languages that intentionally didn't implement a soundly-typed subset of JS; TypeScript is merely one of them.

If you can't make the system 100% sound - which I think is a given if you're going to type idiomatic JS - then the best thing you can do is add more expressitivity so that the type system can define the scope of behavior in a way that plausible errors are caught.

If I were to put an analogy here, this is akin to saying that if there is a car that you have to push for a mile every hundred miles, it's just a design decision. This might seem like a disagreeable experience, of course, but it's still a viable solution to leave it and walk.

Ryan Cavanaugh (@RyanCavanaugh) Do I get it right, that TypeScript is not supposed to have sound type system? I would be happy to share an official answer to other confused people that stumble upon this design decision.

Do I get it right, that TypeScript is not supposed to have sound type system? I would be happy to share an official answer to other confused people that stumble upon this design decision.

The non-goal 3 from the TypeScript Design Goals:

Apply a sound or "provably correct" type system. Instead, strike a balance between correctness and productivity.

@magierjones Thank you! I've never seen that one

If I were to put an analogy here, this is akin to saying that if there is a car that you have to push for a mile every hundred miles, it's just a design decision. This might seem like a disagreeable experience, of course, but it's still a viable solution to leave it and walk.

As Typescripts non-goal hints at, and Ryan has tried to explain: This is not a case of needing to push a car one mile every hundred miles vs driving a hundred miles. It's pusing a car one mile every hundred miles vs driving billions of miles. Productivity would suffer to much for developers writing code in a sounds type system, so they made it a non-goal and instead focus on being mostly correct and productive.

If you are worried about soundness, there are plenty of steps that can be taken by yourself. E.g. creating linting rules to disallow certain code patterns, creating code style conventions to help avoid type issues, using code reviews, etc. A sound type system is also not a replacement for unit-testing, which can often catch cases where types have been incorrectly used.

"Productivity" is quite counterintuitive. A sound type system doesn't make developers less productive, it just shifts the development effort towards compile-time instead of runtime. The less the compiler is able to prevent, the more work the programmer has at runtime (e.g. debugging errors caused by unexpected behavior), and this results in productivity loss.
I believe the realization that shifting towards compile-time is more productive - because it's the cheapest form of feedback - is what made statically typed languages popular again, but type system unsoundness goes in the opposite direction.
TypeScript made this decision and it's totally fine, but it's not fair to justify it as a decision made to enhance productivity.

And unit tests are no replacement for property testing

Someone is attempting a sound type-checker, it's called Hegel:

https://www.infoq.com/news/2020/05/hegel-type-checking-javascript/

It reuses TS syntax, and it claims to be compatible with .d.ts files.

I haven't tried it yet, but it looks interesting?

@polkovnikov-ph re: #51362 (comment) - good news! there's a solution for you!

(it's called ReScript.)

note that removing every single possible bug is a non-goal of TypeScript - if you really want that then go use Dafny and target JS.
the real goal of TypeScript is to make development faster and safer. not trading development speed for safety...

... also there's nothing wrong with making TypeScript fully sound - but good luck patching the 30,000 line checker.ts to be fully sound, without losing half the features (very difficult if not plain impossible), and updating all 8,800+ packages in DefinitelyTyped to be fully sound (because realistically, the number of people that are that concerned about soundness is extremely low relative to the size of the DT community - and even a project as massive as DT often struggles to keep types up to date...)

tl;dr it's so easy to talk about something without so much as a proof of concept. yet somehow when it comes round to implementation they're not willing to do it

Has anyone tried to make a ESLint plugin/configuration which would disallow all/most known sources of unsoundness? It would effectively create a subset of Typescript, but seems a lot easier and more sustainable than actually creating a whole new language.

typescript-eslint already has a bunch of rules that could be reused, like disallowing as and any, and surely one could easily create other rules that would for instance forbid unsafe uses of subtyping, forbid functions from modifying variables in their outer scope, and so on. There would probably be some unsoundness left that cannot be easily detected from a linter, but maybe not that much?

Guillaume Brunerie (@guillaumebrunerie)

Guillaume Brunerie (@guillaumebrunerie) it should be doable enough - the issue is what you'd be missing out on:

overloads
method inheritance
non-deeply-readonly function parameters
the readonly modifier on objects
the builtin definition of Array - and probably most other container types other than maybe typed arrays
and i'm sure there's tons of stuff i've forgotten about

I just read this entire thread for fun (Friday night wooo) and wanted to make one correction: MSR and product teams actually do talk quite frequently. MSR reaches out to product teams whenever there's a concept to be proven, and by my estimate 1% of those proofs-of-concept end up shipping. Don't just take my word for it:

Individual contributors are incentivized to prove impact of their research beyond conference and journal papers, because that's how you become a manager.
M2 and M3 managers are incentivized to turn proofs-of-concept into durable product features, because that's how you get product teams to fund 1–20 research headcounts for years at a time, and having more headcount is how you become an M++.

To your own point, MSR somehow made its way into F#.

God knows I love a cynical rant as much as the next fellow, but let's not besmirch the good name of Microsoft cross-org impact! Now that I've soundly proven (due to how money works) that, to the contrary, MSR is quite incentivized to talk early and often to product teams, we can focus on the actual discussion, such as how MSR has invented a mythical (highly-cited, too!) Turing-complete grammar that describes all possible arrangements of quanta in the universe (using fewer than the number of quanta in the universe to do so, at that!) — but Big Cavanaugh simply refuses to ship it because he knows us mere mortals aren't ready for it yet.

N.B. How many people use F#, and how many people use TypeScript? I've used both, the former in a college class titled (I'm paraphrasing) Esoteric Programming Languages.

Navigation Menu

Repository navigation

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

Simple, Usable, Unsound

Simple, Sound, Unusable

Sound, Usable, Not simple

19 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

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

Description

Activity

zpdDG4gta8XKpMCd commented on Jul 19, 2016

henryptung commented on Jul 20, 2016

zpdDG4gta8XKpMCd commented on Jul 20, 2016

zpdDG4gta8XKpMCd commented on Jul 20, 2016

mhegazy commented on Jul 20, 2016

RyanCavanaugh commented on Jul 20, 2016

Simple, Usable, Unsound

Simple, Sound, Unusable

Sound, Usable, Not simple

zpdDG4gta8XKpMCd commented on Jul 21, 2016

henryptung commented on Jul 24, 2016

DemiMarie commented on Jul 26, 2016

rossberg commented on Sep 22, 2016

DemiMarie commented on May 19, 2017

RyanCavanaugh commented on May 19, 2017

kitsonk commented on May 19, 2017

RyanCavanaugh commented on May 19, 2017

19 remaining items

zpdDG4gta8XKpMCd commented on Dec 12, 2017

kitsonk commented on Dec 13, 2017

reverofevil commented on Jun 19, 2020

MartinJohns commented on Jun 19, 2020

reverofevil commented on Jun 19, 2020

csvn commented on Jun 22, 2020

edrd-f commented on Jul 31, 2020

ShalokShalom commented on Jul 31, 2020

mindplay-dk commented on Oct 22, 2020

somebody1234 commented on Feb 10, 2023

somebody1234 commented on Feb 10, 2023

guillaumebrunerie commented on Feb 25, 2023

somebody1234 commented on Feb 25, 2023

jimmy-zhening-luo commented on Nov 23, 2024

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions