Hacker News Reader

Comment by weatherlight | Hacker News Reader

Typescript's type system isn't sound. The Set theoretical type system proposed for Elixir is.

For more information about what that means, see this playground [0] from the TypeScript docs. PL people often make a big deal about TypeScript's lack of soundness as though it was some kind of mistake, but it was very much an intentional choice given the trade-offs they were making at the time.

If Elixir can pull off soundness without compromising expressivity that will be a huge feat, and I'm excited to see it!

[0] https://www.typescriptlang.org/play/?strictFunctionTypes=fal...

Yea I never bought this assertion from the TS team, saying “given the trade-offs at the time” is the same as saying “we’re already backed into a corner by previous decisions” - the decision(s) may have been intentional at each step but the design itself probably was not. Given the choice of sound or unsound, considering that the purpose of a type system is to give certain guarantees, a type system design must always choose soundness to be considered reasonable.

That being said, I don’t think it’s possible to “pull off soundness without compromising expressivity” because the expressivity in this context is self-referential types which equate to non-terminating unification logic (and thus, unsoundness). Still, I’m excited to see what they do with this type system! Reminds me a bit of Shen’s type system.

Is the TypeScript team correct in explaining that soundness would exclude functions accepting subtypes as laid out there? If so, it seems like any type system that was meant to be able to type common JavaScript idioms would have to be unsound.

Yes and no - you can't have bi-variant argument types as shown here and be sound, but that does not mean you can't type those idioms. You just need the type system to be able to express a dependency between the name of the event handler and the type of the associated function. It is not exactly straightforward (this is a complex type system feature) though, I don't blame the TS devs for going for an escape hatch there.

(Edit: to be clear, allowing to refine function types in the way they do is part of the solution, the unsound part is that it is not checked afaik)

Sub-types can be represented with algebraic types so I’m not sure that’s necessarily true, for example an abstract class with subclasses can be represented as a sum type

only if there is a fixed set of subclasses, which is not always or even mostly the case.

Reply on news.ycombinator.com