[nikeee]

An honorable mention is the string template literal type. It is between the string literal type (-unions); which allow a finite set of strings and the string type which, in theory, is an infinite set of strings. Template literal types can be infinite as well, but only represent a fraction. For example `foo${string}` represent all strings that start with "foo".

Similar to this, I proposed inequality types for TS. They allow constraining a number range. For example, it is possible to have the type "a number that is larger than 1". You can combine them using intersection types, forming intervals like "a number between 0 and 1". Because TS has type narrowing via control flow, these types automatically come forward if you do an "if (a<5)". The variable will have the type "(<5)" inside the if block.

You can find the proposal here [1]. Personally I think the effort for adding these isn't worth it. But maybe someone likes it or takes it further.

[1]: https://github.com/microsoft/TypeScript/issues/43505

[thechao]

We had something like this in Spad — the extension language for the computer algebra system Axiom. They're not terrible to implement; but, utilization was always low. There's amusingly high effort optimizations with range-dependent integral types deduced from flow control around blocks that are tail calls. I mean ... theoretically, yes, we can; but should we?

[klysm]

I have no idea what I’m talking about, but it seems like these restricted cases of inequality flow control type checking are very similar in power to dependent types, but don’t require the same level of complexity. It’s nice being able to write imperative proofs of correctness guided by the compiler.