Typescript: 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 https://github.com/Microsoft/TypeScript/issues/5786, https://github.com/Microsoft/TypeScript/issues/7933, https://github.com/Microsoft/TypeScript/issues/9765, https://github.com/Microsoft/TypeScript/issues/3410#issuecomment-111646030) 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 https://github.com/Microsoft/TypeScript/issues/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 :smile:). 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. https://github.com/Microsoft/TypeScript/issues/15453#issuecomment-298714271 , https://github.com/facebook/flow/blob/c93897cd9d6ac6db703c8b9f0536f440a03d54f4/website/en/docs/lang/types-and-expressions.md#soundness-and-completeness- , https://github.com/facebook/flow/issues/3702#issuecomment-293360271 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 :wink:

[winsut]

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.

[winsut]

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:

1. Add a "--sound" compiler flag, make it the default in tsconfig.json for new projects
2. Enhance the type checker to reject all unsound code if the flag is set
3. If and where necessary, correct the type definitions to properly type things and bump their semver. Optionally, keep maintaining type definitions compatible with the old ones as a separate package, or introduce some syntax to allow to include definitions for multiple "compatibility levels" in the same file

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.

[RyanCavanaugh]

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.

[winsut]

@RyanCavanaugh I think all these things have solutions.

Getters can return a different value each time they're invoked

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.

The valueOf and toString functions are allowed to do literally anything they want

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)

x + y produces a nondeterministic type due to this

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.

The delete operator has side effects which are extremely difficult to describe with a type system

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.

const x = { ["to" + "String"]: 42 } + "oops"; (disallow all computed property names? disallow all primitive values? disallow operator + except when you've... done what, exactly)?

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.

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

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.

[DemiMarie]

How is Flow unsound?

On Jun 5, 2017 2:52 PM, "Ryan Cavanaugh" [e-mail] 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
https://github.com/Microsoft/TypeScript/issues/9825#issuecomment-306272034,
or mute the thread
https://github.com/notifications/unsubscribe-auth/AGGWB8iCSWr0YrGJMed8HWCQ7J4_7mKJks5sBE5agaJpZM4JP_NP
.

[RyanCavanaugh]

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

const arr = ['1', 0];
arr.sort();
arr[0].substr(0); // Throws, no error in Flow

[rossberg]

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 any) can become _very_ expensive, especially with objects and first-class functions. This is a known problem in the literature on gradual typing, and one that seems impossible to solve, even for more well-behaved languages .

[polkovnikov-ph]

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.

[RyanCavanaugh]

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.

[polkovnikov-ph]

Ultimately, type systems are tools we've created to help us write correct programs. Provable soundness is a proxy measure for that effort.

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.

You have to at least compromise to allow typecasts

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.

then a truly sound program is indeed going to require hundreds or thousands of lines of generated code

Right from infernu readme page:

// 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.

[kitsonk]

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.

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...

[ShalokShalom]

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

[polkovnikov-ph]

@kitsonk Of course, ad hominem attacks were always effective, but this particular case is ludicrous.

• First mention of MR was due to SPJ, and second mention even has exact reason written there. I find especially amusing the fact that MR could add to the language design at least _twice_, yet there is no visible communication between the teams of the same employer.
• I did not ignore flaws of JS. I explicitly told that TS is broken mainly because it keeps all those problematic parts.
• I do not ignore there are billions of lines of JS powering the web. I even tell that it's best to keep using JS in its current syntax with a good type inference system on top.
• I do not ignore it is better than JS. Well, even CoffeeScript is better than JS.
• I do not ignore pragmatism. Type system is a very pragmatic thing, if people managed to implement a sound one.
• There was nothing you could use to infer any of your false claims.
• Opinion is expressed explicitly with words like "I think" or at least something containing "I". Everything else in a discussion is what sides believe to be objectively true. Thus "schooling of opinion" is wrong description of what's happening here. If you believe that something else is true, you're free to disagree. Comparison and agreeing on what to call objective truth is what drives the discussion forward. Not ad hominem attacks.

Now that we have advanced this conversation to 2 extraneous messages, you can try to change the tone towards something constructive.

[zpdDG4gta8XKpMCd]

@polkovnikov-ph what is your constructive point? please make a list of simple todo things:

1. typescript needs to be...
2. also typescript needs to be...
3. and also typescript needs to be...
4. and finally typescript needs to be...

instead of whining that it's not what you want

[polkovnikov-ph]

@aleksey-bykov If this is not clear enough

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

then I can shorten it to "a language with some sound type system with principal types". Should I recommend on a set of type system features too?

[zpdDG4gta8XKpMCd]

well if this wasn't clear enough: typescript is not "a language with some sound type system with principal types", sorry you are late to the train, typescript is what it is, it's too late to change it to something it won't be: a sound and provable system (which it was never meant to be)

it's like being upset that a screwdriver isn't a hammer, we got your frustration, move on to something more constructive or find a language that fits you better: fable or purescript for example

[polkovnikov-ph]

well if this wasn't clear enough: typescript is not "a language with some sound type system with principal types", sorry you are late to the train, typescript is what it is,

And that was the original message. Pretty much this line:

TL;DR: There is no single reason to do anything now. The game is lost.

[RyanCavanaugh]

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.

[ShalokShalom]

it's clear that the project has intentionally different aims from the project

To be honest: It is clear what is the initial goal of Typescript and surprisingly appears here in the thread a comment, which shows to me, that another language walks the same way:

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

Both projects are created since for the target audience group is the javascript syntax habitual, see also these talks to understand such implications.

People are used to their stuff.

I suggest different "compile-to-JS" languages to a friend of mine, who is JavaScript developer and his standard answer is something like:

"I had such a hard time learning JavaScript, why should I learn something new?"

So, in my honest opinion is this point of view understandable and based on bad experiences with exact that technique, which they defend now.

~ Stockholm syndrome ~

And the very same happens here.

Not only that the type inference in FSharp and OCaml is simply more useful, since optional, is the whole syntax more concise and the whole language since decades developed on top of a sound base.

Anyway, you can do, what you want.

[zpdDG4gta8XKpMCd]

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

[kitsonk]

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

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.

[polkovnikov-ph]

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.

@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.

[MartinJohns]

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.

[polkovnikov-ph]

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

[csvn]

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.

[edrd-f]

"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.

[ShalokShalom]

And unit tests are no replacement for property testing

[mindplay-dk]

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?