Type-checking unsoundness: standardize treatment of such issues among TypeScript team/community? #9825
Comments
|
To my eye TypeScript is only about 80% sound due to:
I think there are only 2 questions to that and everything else is irrelephant:
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 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. |
|
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 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 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 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. |
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, UnsoundHow TypeScript works today. Simple, Sound, UnusableMake the type system reject all subtype substitutability. This makes nearly every API unusable, for example Sound, Usable, Not simpleHave a notion of mutable/non-mutable objects with co- and contra-variance annotations for generic assignability, like what C++ did with 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 |
|
@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)
|
|
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, TypeScript is already unsound in its most basic subtyping relation: the fact that |
|
@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 |
|
Please change this decision and at least add a command line switch that makes TypeScript FULLY SOUND, meaning that run-time errors are not possible assuming that external code respects the type system. And please also add another switch that inserts runtime checks when calling non-TypeScript code to ensure that invariants are respected, so that if run-time errors still happen, it's possible to pinpoint which non-TypeScript function is responsible for breaking invariants (and thus which type definition is wrong). The reason that the current situation is absolutely terrible is that not only the type system is unsound at compile time, but it's UNSOUND AT RUN-TIME TOO! In other words, not only code that puts a Dog in Cat[] cast to an Animal[] compiles successfully, but it even successfully executes (!!!), since unlike other compile-time-unsound type systems like Java's, TypeScript inserts no runtime checks. So, at runtime you'll end up having code that uses variables of type Cat that are actually a Dog. Let that sink in. Yes, in TypeScript you can really have a Dog object in a Cat variable at runtime. Seriously. This is obviously totally catastrophic and completely destroys any confidence in the proper functioning of a program, or the ability to reason or prove anything about it. In practice, it means you'll get mysterious errors that should be impossible, and the location of the run-time error will be completely unrelated to where the bug is in the source. This means that even once a runtime error happens, there is no easy way to fix it, since it could be caused by garbage being inserted anywhere in the program. Regarding the Cat/Dog example, the solution is obvious: Cat[] should never be castable to Animal[], and in fact Foo[] should never be castable to Bar[] unless Foo = Bar. If you want to cast a Cat[] to an Animal[], just create an Animal[] in the first place instead, or simply create a new Animal[] and copy the elements. |
|
I don't see what the problem with DOM events (or any other browser API) could possibly be? Requiring little code to use them is not an issue since the part of a large and complex application (TypeScript's main target) that deals with any specific API like DOM events is going to be small, and they might often be handled by an UI framework anyway. And of course a sound type system can type them (at worst you can just use object or any for everything), although the types might then require run-time type checks and conversions to use. Obviously this defines "sound type system" in a way that allows people to use typeof, instanceof and ("prop" in obj) at runtime and do the matching type casts if those are successful, while still disallowing programs that produce errors at arbitrary points of the execution and thus disallowing the run-time type of a value not matching its compile-time type. BTW, TypeScript's automatic path-dependent type inference actually makes such code very easy to write and terse, since you only need to do the type check and don't even need to write the cast itself. I also don't see why it's "too late". As far as I can tell all that is needed is to:
TypeScript successfully introduced non-nullable types which are a huge breaking change, so I don't see why full soundness can't be introduced in the same way. |
|
The thing holding us back is not that we haven't thought about the existence of commandline flags. A fully-sound type system built on top of existing JS syntax is simply a fool's errand; it cannot be done in a way that produces a usable programming language. Even Flow doesn't do this (people will claim that it's sound; it isn't; they make trade-offs in this area as well). JS runtime behavior is extremely hostile toward producing a usable sound type system. Getters can return a different value each time they're invoked. The It is much more sane to just start fresh with something like PureScript or other compile-to-JS language that discards JS constructs which prevent sound typing. Lots of projects trying that approach and I'd encourage you to try one if you think soundness is the best possible design goal. |
|
@RyanCavanaugh I think all these things have solutions.
Not sure if I understand what the problem is here: as long as the type of the value they return is correct, why would this be a problem for the type system? C# also has computed properties for instance and it has a working type system. Obviously if you want to do common subexpression elimination or just redundant property access elimination you need to specify in the type system whether a property has a getter or not.
What do you mean? The implementations in Object.prototype and other core types are well defined, and type definitions for any type that overrides them are of course responsible to correctly declare the type they return. (obviously, if they return values of different runtime types, their compile-time return type must be declared as the common supertype of them all, and thus the type system needs to be rich enough to include a common supertype for every set of types)
Why? The compiler knows the types of x and y, and thus knows the types that their implementations of valueOf and toString return, and can thus compute the type of x + y.
First of all, delete obviously cannot change the type (since any object have any number of references in the JavaScript memory model), so all that needs to be determined is when it's allowed to use delete and when it's a compile-time error to do so. And again obviously, it's allowed if and only if the resulting value is a valid instance of the type. In particular, deleting a non-optional property would be a compile-time error, since values without the property would not conform to the type. Obviously optional properties need to be modeled so that "x.optional_property" has a type that is the union of the type of the property in the prototype and the declared type of the optional property.
Only allow computed property names for types that are declared to have them. If a type has computed properties (and an Object prototype), then obj.toString is the union of the computed property value type and the type of Object.prototype (just as if it had an optional toString property), and the 'obj + "oops"' expression thus is probably going to be a compile-time error, since it must only be allowed when obj.toString is known to be a function that takes 0 arguments and returns string. In an optional "very strict" mode, one could just make a + "oops" a compile time error every time unless a is a string.
Why can't TypeScript do the same, at least under a suitable command line flag? It's only a problem for people who want to convert existing JavaScript codebases to TypeScript, which can either disable the soundness mode, or, since they need to change the code to add type information anyway, they can also fix the pathological constructs in the process. |
|
How is Flow unsound?
…On Jun 5, 2017 2:52 PM, "Ryan Cavanaugh" ***@***.***> wrote:
The thing holding us back is not that we haven't thought about the
existence of commandline flags.
A fully-sound type system built on top of existing JS syntax is simply a
fool's errand; it cannot be done in a way that produces a usable
programming language. Even Flow doesn't do this (people will claim that
it's sound; it isn't; they make trade-offs in this area as well).
JS runtime behavior is extremely hostile toward producing a usable sound
type system. Getters can return a different value each time they're
invoked. The valueOf and toString functions are allowed to do literally
anything they want; it's possible that the expression x + y produces a
nondeterministic *type* due to this. The delete operator has side effects
which are extremely difficult to describe with a type system. Arrays can be
sparse. An object with a own property of type undefined behaves
differently from an object with a prototype property of the same value.
What could even be done about code like const x = { ["to" + "String"]: 42
} + "oops"; (disallow *all* computed property names? disallow *all*
primitive values? disallow operator + except when you've... done what,
exactly)?
It is much more sane to just start fresh with something like PureScript or
other compile-to-JS language that discards JS constructs which prevent
sound typing. Lots of projects trying that approach and I'd encourage you
to try one if you think soundness is the best possible design goal.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#9825 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AGGWB8iCSWr0YrGJMed8HWCQ7J4_7mKJks5sBE5agaJpZM4JP_NP>
.
|
|
@DemiMarie it doesn't handle array mutation in general very well, for example. This snippet is an error in TS but not Flow, for example: |
|
In addition to the difficulties of making JavaScript as is sound it is also worth pointing out that the runtime type checks needed to fence against untyped code (or bits typed |
|
TL;DR: There is no single reason to do anything now. The game is lost. One doesn't simply create a policy for type system unsoundness, when unsoundness comes from the mistake in mission statement. It's impossible to create a sound type system that allows generation of arbitrary JS code. Valid JS programs are way too diverse. There is no finite set of type system features to type them all. TS team set a trade-off point to "let's type whatever we can in a practical way" and got overwhelmed by a mass of language features. TS's type system is more advanced than one in Haskell, and it would require inhuman abilities to prove soundness and preservation even for one version. I can perfectly see why @RyanCavanaugh says there is no practical way to make sound type system: the belief in correctness of "type whatever we can" approach is too strong. It seems too weird to restrict ourselves in JS code that we can generate. But I would choose a much lower point of "whatever can be inferred". Such type systems are known to be simple for users and developers, they are (usually) sound, and as a nice side effect there wouldn't be any need in extra syntax (i.e. JS programs written in a modest way would need no changes). As an answer to the question from comments up above: you don't even need to pay to develop anything there. It was already made by Noam Lewis (more). It landed just several years too late to inspire TS and Flow to use the same approach. As indirect evidence that such type systems are good for web development I can link to O'Caml, which is actively popularized for web development now by Facebook (well, they had to make alternative better syntax for it, because original syntax is that bad). The problem with these languages is that they are really different in feature set to what TS has right now. Features like overloading, variadic functions and default arguments are known offenders in type systems, but those languages lack even such popular things as classes. While there is no good reason to keep OOP BS in a programming language, it's a real challenge to make users believe it too, and force anyone to adopt such a restriction. O'Caml has row polymorphism instead, which authors carefully market as if it was OOP. But there was a major breakthrough in type theory since either of those languages were created, which could probably be used to keep classes. McConnell mentions somewhere in first 30 pages of "Code Complete" that bugs in mission statement are hundred times more costly when the product went to production, and this is exactly the case (no snarkiness implied). I hope the next time Microsoft decides to make a programming language to solve the problems of the modern web, they will ask someone from Microsoft Research labs to join the team. Edit: The approach of PureScript, GHCJS, Idris and other such languages restricts the set of supported features of JS too, but it's a hugely different approach. Neither of those languages translates to clean, human-readable JS code. The size of generated JS program is quite bad or unpredictable there. While page load time is still a valid requirement, these languages (unlike, for example, TS) won't be able to fill the whole niche of front-end development. |
|
The approach of removing features from the runtime language until you get something that can be soundly typed is an equally valid one, and one that someone ought to try. I would not go to such a language's issue tracker and say that e.g. not supporting property getters is a "bug" in their mission statement because I believed that supporting 100% of the runtime was the only valid goal a language could have. If you're going to pull JSON off the wire and do operations on it (which I think is a bare minimum for a client JS language), then a truly sound program is indeed going to require hundreds or thousands of lines of generated code - the goal of small generated JS and actual runtime soundness are incompatible. You have to at least compromise to allow typecasts, and once you allow typecasts then any soundness arguments are somewhat moot because the final soundness of the program (i.e. whether or not incorrectly-typed values are observed at runtime) will depend on how often the programmer has to write those casts and how likely they are to get those casts correct. Most bugs in the TypeScript compiler I've recently fixed had to do with incorrect casts in places where a more expressive type system would make those casts unnecessary; bugs sourced in non-casted unsoundness happen maybe once a month at most. The recent paper comparing TS and Flow found no bugs which were only found by Flow because of their slightly stricter soundness. Expressitivity, provable soundness, and typechecking performance are going to be somewhat at odds, especially when describing a type system built on top of a full-featured runtime that you're not willing to pare back. What we've found is that in practice, there are a lot of correct programs which are not provably sound, yet encounter no difficulty in not observing that unsoundness because the type system can correctly express the patterns they use. 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. 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. |
Provable soundness is what distinguishes type systems from static program analyzers. Unsound type system is either a bug or an oxymoron, depending on sense of humor. If we compare harm between not allowing some of idiomatic JS and forcing users to hastily hunt bugs over a megabyte of source code that went to production due to a bug in compiler, I'd choose the former. The trade-off here is of better code vs easier marketing. Luckily, the Overton window moves, and less people think that "idiomatic JS" is a real thing someone could desire.
Not true. You don't need any typecasts. Upcasts lose information, downcasts are unsound. Somehow O'Caml doesn't have to compromise with their row polymorphism and extensible variants. The problem is that TS have already chosen to implement type system with subtyping.
Right from // gets typed as getData :: h.({data: i, ..j} -> i)
function getData(obj) {
return obj.data;
}Did it take hundreds of lines? (Meanwhile...). Edit. Oh, I didn't get the message. Yes, you need hundreds of lines to read and check that JSON, and no, you're not allowed to use typecasts there. Please, ask people at Microsoft Research about F# and type providers, they have solved this problem long ago. |
You seem to think that Microsoft Research is some sort of land of milk and honey that if only people would listen the world would be so much better. You also seem to think that the TypeScript team have no relationship with the Microsoft Research teams. Both would be mistakes to make. You have done your duty of schooling everyone on your opinion of why TypeScript is hopelessly broken. Of course you can ignore the simple fact that JavaScript, as a language, has some fundamental flaws. You can also ignore the billions of lines of code that power the web. You can also ignore the millions of lines of TypeScript that have helped the web run a bit more sanely than they did before. You can ignore how while not perfect, it is a damn site better than what we had before. You can ignore pragmatism versus this land of pure logic you wish to live in. I am not sure you are adding anything to the conversation though other than trying to prove to people how smart you are. Well touché, you are brilliant. For me, I will continue to make things that are practical and are significantly more sound and usable than they were a few short years ago... |
And that was the original message. Pretty much this line:
|
|
If the feedback is unactionable because it's five years late, and it's clear that the project has intentionally different aims from the project you'd like to have seen be made, what exactly are you hoping to achieve here? 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. It's a very long road ahead of you in terms of telling people on issue trackers that they did a terrible job choosing their design goals. We would like these discussions to be constructive in a way that produces usable results. Jumping in to declare that TypeScript is a lost cause for you and there's nothing we can do about it now isn't useful. |
|
Edit: Coming back to this thread years later.. oh my 😅 I think Typescript is fine as a language, and its fine that its type system is unsound. And that picks people up, who would have not choose F#/Fable either way, and stayed on Javascript. With var. One aspect, that many people seem to forget, is that Typescript is not only about features, its also about how features are used. The Typescript community has build up a culture, in which modern features are used, and old, outdated ones are ditched. That alone makes the language worth existing. |
|
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 |
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...
I am sure there are far more capable people than me to do that. I am not sure what your point is. |
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. @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. |
The non-goal 3 from the TypeScript Design Goals:
|
|
@magierjones Thank you! I've never seen that one |
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. |
|
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. ... 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.
|
|
@guillaumebrunerie it should be doable enough - the issue is what you'd be missing out on:
|
|
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:
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. |
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:
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):
The text was updated successfully, but these errors were encountered: