> A minifier can't guarantee that such expressions won't be used, so it cannot optimize property accesses.
Given TypeScript’s type system is unsound, neither could it even if it tried, right? I guess Flow could, but well, here we are.
Given TypeScript’s type system is unsound, neither could it even if it tried, right? I guess Flow could, but well, here we are.
I'm asking because there's no accepted definition of what an unsound type system is.
What I often see is that the word unsound is used to mean that a type system can accept types different to what has been declared, and in that case there's nothing unsound about ts since it won't allow you to do so.
Typescript is a bit more unsound than most because of the escape hatch `any` and because of the (intentional) disconnect between compiler and runtime environment. Even though "unsound" sounds like a bad thing to be, it's a big part of why Typescript is so successful.
For example if you have a Java expression of type MyClass, and it gets evaluated, then it must either throw (so that it doesn't produce any value) or produce a value of type MyClass: either an instance of MyClass, or of one of its subclasses, or null. It will never produce an instance of some other class, or an int, or anything else that isn't a valid value for the type MyClass.
In addition to helping human readers reason about the code, a sound type system is a big deal for a compiler: it makes it possible to compile the code AOT to fast native code, without inserting a bunch of runtime checks and dynamic dispatching to handle the fact that inevitably some of the types (but you don't know which) are wrong.
The compiler implications are what motivated the Dart language's developers to migrate from an unsound to a sound type system a few years ago: https://dart.dev/language/type-system#the-benefits-of-soundn... so that they could compile Flutter apps AOT. This didn't require anyone to make their code resemble what you'd do in a theorem prover — it just means that, for example, all casts are checked, so that they throw if the value doesn't turn out to have the type the cast wants to return.
TypeScript is unsound because when you have an expression with a type, that tells you nothing at all for sure about what the value of the expression can be — it might be of that type, or it might be anything else. It's still valuable because you can maintain a codebase where the types are mostly accurate, and that's enough to help a lot in reading and maintaining the code.
The purpose of typescript is usefully type as much javascript as possible, to do both this and have a sound type system it would require to change javascript.
A prime example is that if you index into an array of type `T[]`, JS semantics mean the value you get back could be undefined as well as a `T`. So to describe existing JS semantics in a sound type system, the type would have to be `T | undefined`, which would be a big pain. Alternatively you could make the type `T` and have that be sound, but only if you make the runtime semantics be that an out-of-bounds access throws instead of returning undefined.
The problem is that you can arbitrarily narrow types (and any can narrow to any type) eg: https://www.typescriptlang.org/play/?#code/DYUwLgBAzg9grgOwC...
If your type system has at least two types that aren't the same as each other, then adding "any" makes it unsound right there. The essence of "any" is that it lets you take a value of one type and pretend it's of any other type. Which is to say that "any" is basically the purified form of unsoundness.
Consider this example (https://www.typescriptlang.org/play/?ssl=10&ssc=1&pln=1&pc=1...):
function messUpTheArray(arr: Array<string | number>): void {
arr.push(3);
}
const strings: Array<string> = ['foo', 'bar'];
messUpTheArray(strings);
const s: string = strings[2];
console.log(s.toLowerCase())
In Haskell land, where the type system is considered sound you have `head` functions of type `List a -> a` that are unsound too, because the list might be empty.
However this problem as stated is slightly different and has to do with a failure of OOP/subtyping to actually intermingle with our expectations of covariance.
So to just use classic "animal metaphor" OOP, if you have an Animal class with Dog and Cat subclasses, and you create an IORef<Cat>, a cell that can contain a cat, you would like to provide that to an IORef<Animal> function because you want to think of the type as covariant: Cat is a subtype of Animal, F<Cat> should be a subtype of F<Animal>. The problem is that this function now has the blessing of the type system to store a Dog in the cell, which can be observed by the parts that still consider this an IORef<Cat>.
Put slightly differently, in OOP, the methods of IORef<Cat> all accept an implicit IORef<Cat> called `this`, if those methods are part of what define an IORef<x> then an IORef<x> is necessarily invariant, not covariant, in <x>. And then you can't assume subtyping. So to be sound a subtype system would presumably have to actually mark contra/covariance around everything, and TypeScript very intentionally documents that they don't do this and are just trying to make a "best effort" pass because JavaScript has 0 types, and crappy types are better than no types, and we can't wait for perfect types to replace the crappy types.
Haskell's `head` not is not an example of the type system being unsound (I stress this point because we've been talking about type system soundness, not something-else-soundness).
From the view of the type system, `head` is perfectly sound: if the list is empty, the resulting value is ⊥ ("bottom"). And ⊥ is an inhabitant of every type. Therefore, `head` returning ⊥ when given an empty list is perfectly fine. When you force ⊥ (i.e. use it any way whatsoever), an exception is thrown. See https://wiki.haskell.org/Bottom
This is very much not the same thing (or remotely analogous) to what we have in my TypeScript example. There, the code fails at runtime when I attempt to call `toLowerCase`, yes; what's worse is the slightly different scenario where we succeed in calling something we shouldn't:
class Person {
name: string;
constructor(name: string) {
this.name = name;
}
kill() {
console.log("Killing: " + this.name);
}
}
class Murderer extends Person { }
class Innocent extends Person { }
function populatePeopleFromDatabase(people: Array<Innocent | Murderer>): void {
// imagine this came from a real SQL query
people.push(new Innocent("Bob"));
}
function populateMurderersFromDatabase(people: Array<Murderer>): void {
// TODO(Aleck): come back and replace this with a query that only selects murderers.
// i wanted to get the rest of the code in place, and this type checks,
// so I'll punt on this for now and come back later when I wrap my head
// around the proper SQL.
// we're not actually using this anywhere just yet, so no biggie ¯\_(ツ)_/¯
populatePeopleFromDatabase(people);
}
// ... some time later, Bob comes along and implements the murderer execution logic:
const murderers: Array<Murderer> = [];
populateMurderersFromDatabase(murderers);
// Bob is about to have a really shitty day:
murderer.forEach((murderer) => murderer.kill());
Huh?
The cheeky answer would be that the definition here is the one the TypeScript documentation itself uses[1].
The useful answer is that there’s only one general definition that I’ve ever encountered: a type system is sound if no well-typed program encounters type errors during its execution. Importantly, that’s not a statement about the (static) type system in isolation: it’s tied to the language’s dynamic semantics.
The tricky part, of course, is defining “type error”. In theoretical contexts, it’s common to just not define any evaluation rules at all for outwardly ill-typed things (negating a list, say), thus the common phrasing that no well-typed program must get stuck (unable to evaluate further). In practical statically-typed languages, there are on occasion cases that are defined not to be type errors essentially by fiat, such as null pointer accesses in Java, or escape hatches, such as unsafeCoerce in practical implementations of Haskell.
Of course, ECMAScript just defines behaviour for everything (except violating invariants in proxy handlers, in which case, lol, good luck), so arguably every static type system for it is sound, even one that allows var foo: string = 42. Obviously that’s not a helpful point of view. I think it’s reasonable to say that whatever we count as erroneous situations must at the very least include all occurrences of ReferenceError and TypeError.
TypeScript prevents most of them, which is good enough for its linting use case, when the worst possible result is that a buggy program crashes. It would definitely not be good enough for Closure Compiler’s minification use case, when the worst possible result is that a correct program gets silently miscompiled (misminified?).
[1] https://www.typescriptlang.org/docs/handbook/type-compatibil...
If you read the Flow codebase and its Git history, you can see that it's not for lack of trying, either — every couple of years there's an ambitious new engineer with a new plan for how to make it happen. But it's a real tough migration problem — it only works if they can provide a credible, appealing migration path to the other engineers across Facebook/Meta's giant JS codebase. Starting from a language like JS with all the dynamic tricks people use there, that's a tough job.
(And naturally it'd be even harder if they were trying to get any wider community to migrate, outside their own employer.)
I wonder how widely used that option is. As I said in that other comment, it feels to me like the sort of thing that would produce errors all over the place, and would therefore be a real pain to migrate to. (It'd be just fine if the language semantics were that out-of-bounds array access throws, but that's not the semantics JS has.) I don't have a real empirical sense of that, though.
But there are TSconfig options to ensure no use of any so with the right level of strictness it could happen.