4 ms·

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

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

afavour 2y ago
Theoretically TS could… until it encounters an ‘any’ type in that code path, then it would have to give up. But there are TSconfig options to ensure no use of any so with the right level of strictness it could happen.
epolanski 2y ago
What do you mean by unsound exactly. 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.
- sharlos201068 2y ago
  That’s not correct, there’s several ways the actual type of a value differs from what typescript thinks it is. But soundness isn’t a goal of typescript.
  - WorldMaker 2y ago
    It's maybe useful to note in this discussion for some that "soundness" of a type system is a bit of technical/theoretical jargon that in some cases has specific mathematical definitions and so "unsound" often sounds harsher (connotatively) than it means. The vast majority of type systems are "unsound" for very pragmatic reasons. Developers don't often care to work in a "sound" type systems. Some of the "most sound" type systems we've collectively managed to build are in things like theorem provers and type assertion systems that some of us don't always even consider useful for "real" software development. 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.
    - price 2y ago
      There's nothing arcane or particularly theoretical about soundness. It means that if you have an expression of some type, and at runtime the expression evaluates to a value, the value will always be of that type. 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-soundness 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.
      - afiori 2y ago
        The key factor is that typescript is not a language, it is a notation system for a completely independent language. 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.
        price 2y ago
        Definitely to get the most ergonomic programming experience, while also having a sound type system, you'd need to change some of the semantics of the language. 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.
- cstrahan 2y ago
  > and in that case there's nothing unsound about ts since it won't allow you to do so Consider this example (https://www.typescriptlang.org/play/?ssl=10&ssc=1&pln=1&pc=1#code/GYVwdgxgLglg9mABAWwKYGd0FUAOAVAC1QEEAnUgQwE8AKC8gLkTMqoB50pSYwBzRAD6IwIZACNUpAHwBKJgDc4MACaIA3gFgAUIl2J6pAHQ4Q6AjQDMMgNzaAvtu0QEnRJ2590TFtQ5cevFKIALyIANoA5MBwcBEANIgRYvQRALq2WmiYuIQk5NQ07gHoNo5azmCuXm7+fCE1HrzoYQBM6U4ucAA2qIZdcLyFhlBwADJwAO6SAMIU6Kg0MjLaQA 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()) Could you explain how this isn't the type system accepting types "different to what has been declared"? Kinda looks like TypeScript is happy to type check this, despite `s` being a `number` at runtime.
  - epolanski 2y ago
    That's a good example, albeit quite of a far-fetched one. 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.
    - crdrost 2y ago
      That option also exists, you can just leave out the `messUpTheArray` lines and you get an error about how `undefined` also doesn't have a `.toLowerCase()` method. 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.
- mananaysiempre 2y ago
  > there's no accepted definition of what an unsound type system is 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-compatibility.html#a-note-on-soundness https://www.typescriptlang.org/docs/handbook/type-compatibil...
RyanCavanaugh 2y ago
Flow's type system isn't sound either FWIW
- price 2y ago
  Yeah, Flow had the ambition to be sound but has never accomplished it. 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.)
  - RyanCavanaugh 2y ago
    Flow doesn't even check that array access is in-bounds, contrast to TypeScript with noUncheckedIndexedAccess on. They're clearly equally willing to make a few trade-offs for developer convenience (a position I entirely agree with FWIW)
    - price 2y ago
      Neat example, thanks! I hadn't known TS had that option. Array access was actually exactly the example that came to mind for me in a related discussion: https://news.ycombinator.com/item?id=41076755 https://news.ycombinator.com/item?id=41076755 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.

afavour 2y ago

Theoretically TS could… until it encounters an ‘any’ type in that code path, then it would have to give up. But there are TSconfig options to ensure no use of any so with the right level of strictness it could happen.

epolanski 2y ago

What do you mean by unsound exactly. 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.

sharlos201068 2y ago
That’s not correct, there’s several ways the actual type of a value differs from what typescript thinks it is. But soundness isn’t a goal of typescript.
- WorldMaker 2y ago
  It's maybe useful to note in this discussion for some that "soundness" of a type system is a bit of technical/theoretical jargon that in some cases has specific mathematical definitions and so "unsound" often sounds harsher (connotatively) than it means. The vast majority of type systems are "unsound" for very pragmatic reasons. Developers don't often care to work in a "sound" type systems. Some of the "most sound" type systems we've collectively managed to build are in things like theorem provers and type assertion systems that some of us don't always even consider useful for "real" software development. 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.
  - price 2y ago
    There's nothing arcane or particularly theoretical about soundness. It means that if you have an expression of some type, and at runtime the expression evaluates to a value, the value will always be of that type. 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-soundness 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.
    - afiori 2y ago
      The key factor is that typescript is not a language, it is a notation system for a completely independent language. 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.
      - price 2y ago
        Definitely to get the most ergonomic programming experience, while also having a sound type system, you'd need to change some of the semantics of the language. 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.
cstrahan 2y ago
> and in that case there's nothing unsound about ts since it won't allow you to do so Consider this example (https://www.typescriptlang.org/play/?ssl=10&ssc=1&pln=1&pc=1#code/GYVwdgxgLglg9mABAWwKYGd0FUAOAVAC1QEEAnUgQwE8AKC8gLkTMqoB50pSYwBzRAD6IwIZACNUpAHwBKJgDc4MACaIA3gFgAUIl2J6pAHQ4Q6AjQDMMgNzaAvtu0QEnRJ2590TFtQ5cevFKIALyIANoA5MBwcBEANIgRYvQRALq2WmiYuIQk5NQ07gHoNo5azmCuXm7+fCE1HrzoYQBM6U4ucAA2qIZdcLyFhlBwADJwAO6SAMIU6Kg0MjLaQA 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()) Could you explain how this isn't the type system accepting types "different to what has been declared"? Kinda looks like TypeScript is happy to type check this, despite `s` being a `number` at runtime.
- epolanski 2y ago
  That's a good example, albeit quite of a far-fetched one. 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.
  - crdrost 2y ago
    That option also exists, you can just leave out the `messUpTheArray` lines and you get an error about how `undefined` also doesn't have a `.toLowerCase()` method. 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.
mananaysiempre 2y ago
> there's no accepted definition of what an unsound type system is 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-compatibility.html#a-note-on-soundness https://www.typescriptlang.org/docs/handbook/type-compatibil...

RyanCavanaugh 2y ago

Flow's type system isn't sound either FWIW

price 2y ago
Yeah, Flow had the ambition to be sound but has never accomplished it. 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.)
- RyanCavanaugh 2y ago
  Flow doesn't even check that array access is in-bounds, contrast to TypeScript with noUncheckedIndexedAccess on. They're clearly equally willing to make a few trade-offs for developer convenience (a position I entirely agree with FWIW)
  - price 2y ago
    Neat example, thanks! I hadn't known TS had that option. Array access was actually exactly the example that came to mind for me in a related discussion: https://news.ycombinator.com/item?id=41076755 https://news.ycombinator.com/item?id=41076755 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.