What does "soundness" mean here? I love typescript's type system, except for the quirks that are inherited from javascript, which I sometimes find infuriating, and I'm wondering if you're talking about the same thing. For example, the fact that typescript- through javascript- only exposes a single `number` type is so annoying. Sometimes that's fine, but other times it would be nice to be able to say "No, this isn't just any damn number, this is an integer! This is an iterable ID for god's sake!" so you at the very least get a static error when you try to pass in `1.001`, or something that could be `1.001`. And that's just a very basic example of how a collection of number types with more granularity would be an improvement. Especially if they were a little more robust than that and were composable. Imagine being able to type `integer | negativeFloat` or other such wacky composed types. Ideally you could compose your types programmatically, and define shit like "the type is a `float` who's floor value has a % 3 of 0".
Informally, a sound type system is one that never lies to you.
Formally, the usual notion of soundness is defined with respect to an evaluation strategy: a term-rewriting rule, and a distinguished set of values. For pure functional programs this is literally just program execution, whereas effects require a more sophisticated notion of equivalence. Either way, we'll refer to it as evaluating the program.
There are two parts:
- Preservation: if a term `a` has type `T` and evaluates to `b`, then `b` has type `T`.
- Progress: A well-typed term can be further evaluated if and only if it is not a value.
// This can go all the way back to the smallest common type:
listenForEvent("mouse", (event: {}) => { });
Typescript {} is a trap that means "any container of things is fine" (including objects), it's not the empty struct. One of the very ugly oddities of the language..
`Record<string, never>` or something like that is the closest equivalent to an empty struct.
