Earlier quoted context omitted.
> 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... ): function messUpTheArray(arr: Array ): void { arr.push(3); } const strings: Array = ['foo', 'bar']; messUpTheArray(strings); const s: string = strings[2]; console.log(s.toLowerCase()) Could you explain how this isn't the type system accepting t…
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.
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, a cell that can contain a cat, you would like to provide that to an IORef function because you want to think of the type as covariant: Cat is a subtype of Animal, F should be a subtype of F. 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.
Put slightly differently, in OOP, the methods of IORef all accept an implicit IORef called `this`, if those methods are part of what define an IORef then an IORef is necessarily invariant, not covariant, in . 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.