Proposal: Interval Types / Inequality Types

[nikeee]

Related Proposals:

• Range as Number type: Suggestion: Range as Number type #15480
• Range type for arrays: https://gist.github.com/rbuckton/5fd81582fdf86a34b45bae82d842304c
• NaN / integer / float type: Add a --strictNaNChecks option, and a NaN / integer / float type to avoid runtime NaN errors #28682

This proposal is partly based on @AnyhowStep's comment and describes the addition of an IntervalType to TypeScript.

📃 Goals / Motivation

Provide developers with a type system that prevents them from forgetting range checks on numbers similar to how we prevent them from forgetting string validation and numeric constant checks.

An interval primitive defines a range of numbers, limited up to a specific value. For example, less than 10 is an interval boundary (this wording may be subject to change).

Non-Goals

• Integer types
• Dependent types
• NaN or (-)Infinity literal type
• Distinction between double and floats

Definitions

The idea is to extend type-narrowing for relational comparisons (<, >, <=, >=), in addition to the currently existing mechanism to narrow by equality (== !=, ===, !==).

The emerging type is one that lays between literal types (a type with a single value) and the number type.

Syntax

NonArrayType := ...
                | IntervalType

IntervalType := '(' RelationalOperator  IntervalTypeLimit ')'
RelationalOperator  := '<' | '<=' | '>' | '>='
IntervalTypeLimit   := NumberLiteral

So, in code we'd do something like this:

export interface IntervalType extends Type {
    limit: IntervalTypeLimit;
    constraint: RelationalOperator;
}

export type RelationalOperator =
    | SyntaxKind.LessThanToken
    | SyntaxKind.LessThanEqualsToken
    | SyntaxKind.GreaterThanToken
    | SyntaxKind.GreaterThanEqualsToken
    ;

Side-Note: There is also a suggestion by @btoo to use the new intrinsic type and generics instead of a distinct syntax (like GreaterThan<5>).

Semantics

// a must be a positive number
let a: (>0) = 1;
a = -1; // Error, cannot assign -1 to (>0)

function takePositiveNumber(v: (>0)) {
    // ...
}
takePositiveNumber(a);
takePositiveNumber(-1); // Error, cannot assign -1 to (>0)

Currently, IntervalTypeLimit can only ba a NumberLiteral. Allowing references to other types would make this feature significantly more different. There may be a useful opportunity when it comes to generics (see below).

Assignability

A variable of type A is assignable to one of type B:

let a: A;
let b: B = a; // ok, iff...

A\B	(> y)	(>= y)	(< y)	(<= y)
(> x)	x >= y	x >= y	false	false
(>= x)	x > y	x >= y	false	false
(< x)	false	false	x <= y	x <= y
(<= x)	false	false	x < y	x <= y

Assignability when constants are involved:

const c: c;
let b: B = c; // ok, iff...

c\B	(> x)	(>= x)	(< x)	(<= x)
number literal k	x < k	x <= k	x > k	x >= k
NaN	false	false	false	false
Infinity	true	true	false	false
-Infinity	false	false	true	true
null	false	false	false	false
undefined	false	false	false	false
any non-number type	false	false	false	false

Since the IntervalType is NumberLike, one can do everything with it what can be done with number.

Control-Flow

The core idea is that we extend type narrowing and combine that with union and intersection types:

let a: number = 12;

if (a > 10) {
    a; // (>10)

    if (a < 20) {
        a; // (>10) & (<20)
    }

    a; // (>10)
}

if (a > 10 || a < 0) {
    a; // (>10) | (<0)
    if (a > 10) {
        a; // (>10)
    } else {
        a; // (<0)
    }
}

Union and Intersection Types

Interval types can be used in an intersection type:

type Probability = (>=0) & (<=1);
function random(): Probability { /* ... */ }

A union or intersection type may only contain at most two interval boundaries:

• (>10) | (>20) will be reduced to (>10)
• (>10) & (>20) will be reduced to (>20)
• (<10) & (>10) will be reduced to never
• (<10) | (>10) will not get simplified, it remains (<10) | (>10)
• ...
• For (>=1) | (<1), see below

Other cases how interval boundaries interact with existing types:

• number | (>1) is reduced to number
• number & (>1) is reduced to (>1)
• (>1) & <any non-number type> is reduced to never

Subject for discussion: Handling of (>1|2|3)

It may be appropriate to expand this as (>1) | (>2) | (>3) (which would be normalized to (>1)). Or we just prohibit this kind of use.

The case of (>=1) | (<1)

Consider this code:

let a: number = 10;
if (a > 9) {
	a; // (>9)
} else {
	a; // number
}

In the else branch, we widen the type back to number instead of narrowing to (<=9). This is because we'd also branch to else, if a would be NaN. So, number implicitly contains NaN.
If a variable's type is/contains an interval boundary, its value cannot be NaN.

This opens up the question on how we should handle (>=1) | (<1). Semantically, it is equivalent to number \ {NaN}, so number would not be equivalent here.

It would feel more natural to the developer if (>=1) | (<1) would become number (including NaN), since not reducing it to number would look weird.

If we'd have negated types (#29317) as well as a NaN type, we could model this as number & not NaN. This may outweigh practical use and would be against the design rules (see the third entry in "Non-Goals"; this is an opinion).
We also don't have a NaN type and there is currently no intent to introduce it.

If we'd decide against the simplification to number, it would make discriminated unions work more easily.

Discriminated Unions via Interval Boundary Types?

Having discriminated unions based on intervals is not yet evaluated that much. Considering the problem with (>=1) | (<1), this may not be possible. For example:

type A = {
    success: (>0.5)
    data: boolean;
};
type B = {
    success: (<=0.5);
    message: string;
};
type Result = A | B;
Result["success"]; // number

declare let res: Result;
if (res.success > 0.5) {
    res.data; // ok
} else {
    res; // still `Result`, because in the `else` branch, res.success is still `number`
}

Discriminated unions would work if the else branch of the example in (>=1) | (<1) would resolve to (<=9). For that to work, we need to drop NaN.

We could also solve this problem by not simplifying (>=1) | (<1) to number, so Result["success"] would be (>0.5) | (<=0.5) instead of number.

Normalization of Unions and Intersections

When n interval boundaries are unified or intersected, the result will always be a single boundary, exactly two boundaries, a number literal, number or never.
Normalization is commutative, so one half of the table is empty.

Normalizing A | B:

A\B	(> y)	(>= y)	(< y)	(<= y)
(> x)	(> min(x, y))	y <= x ? (>= y) : (> x)	y > x ? number : (> x) or (< y)	y < x ? (>= x) or (<= y) : number
(>= x)	-	(>= min(x, y))	y >= x ? number : (>= x) or (< y)	y < x ? (>= x) or (<= y) : number
(< x)	-	-	(< max(x, y))	y < x ? (< x) : (<= y)
(<= x)	-	-	-	(<= max(x, y))

(due to a limitation of markdown tables, we use or instead of |)

Normalizing A & B:

A\B	(> y)	(>= y)	(< y)	(<= y)
(> x)	(> max(x, y))	y <= x ? (> x) : (>= y)	y > x ? (> x) & (< y) : never	y > x ? (> x) & (<= y) : never
(>= x)	-	(>= max(x, y))	y > x ? (>= x) & (< y) : never	y < x ? never : (y == x ? y : (>= x) & (<= y))
(< x)	-	-	(< min(x, y))	x > y ? (<= y) : (< x)
(<= x)	-	-	-	(<= min(x, y))

If an interval is equality-compared to a literal, we either narrow down to the respective literal or never.
Further narrowing a boundary intersection via control flow will not increase the number of interval boundaries present in the type:

let a: number = 10;
if (a > 0) {
    a; // (>0)
    if (a < 10) {
        a; // (>0) & (<10)
        if (a < 5) {
            a; // (>0) & (<5)
            if (a > 4) {
                a; // (>4) & (<5)
                if (a > 5) {
                    a; // never
                }
            }
        }
    }
}

Assertions

• We can do assertions like a as (>1) (where a is a number or another interval), just like with number literal types.

Widening and Arithmetics

Similar to literal types, type-level arithmetics are not supported and coerce to number. For example:

let a: (>1) = 4;
let b = a + 1; // _not_ (>2), but number

Also, applying operators like ++ and -- let the type widen to number:

let a: 1 = 1;
a++;
a; // number

let b: (>=1) = 1;
b++;
b; // number

However, due to the way interval types are always reduced to a maximum of two interval boundaries, it may be feasable to do type-level arithmetics. This proposal currently does not intent to do this.

Loops

With intervals, we can be more exact about loop variables. For example, narrowing a simple c-style for loop would come "for free" if we have flow-based type-narrowing that works for if-then-else:

for (let i = 0; i < 10; ++i) {
	i; // (<10)
}

Explanation on what happens:

for (
	let i = 0; // number
	i < 10; // i -> (<10)
	++i // i -> number again
) { }

// Equivalent to

let i = 0; // number
while (i < 10) {
	i; // (<10)

	++i; // number
}

With a little more work, it may be possible to let i be (>=initial-value) & (<10). But due to the type coercion that ++ causes, this is not possible out-of-the-box.

Enum Interaction

It may be an interesting addition to allow enum literals as limit value, so we can type something like this:

function isListTerminator(kind: (< ParsingContext.Count)): boolean {
    // ...
}

isListTerminator(ParsingContext.Count); // Error
isListTerminator(ParsingContext.ClassMembers); // Ok

type AssignmentOperator = (>=SyntaxKind.FirstAssignment) & (<=SyntaxKind.LastAssignment);
function isAssignmentOperator(token: SyntaxKind): token is AssignmentOperator {
    // (return type could also be inferred here)
    return token >= SyntaxKind.FirstAssignment && token <= SyntaxKind.LastAssignment;
}

It should also be possible to pass interval types to functions that take enums (just like numbers).

Generics

Generics may be valuable to support in this proposal, when they resolve to a literal type.

Consider this implementation of clamp:

function clamp<TMin extends number, TMax extends number>(min: TMin, max: TMax, value: number): (>=TMin) & (<=TMax) {
    if (value < min)
        return min;
    if (value > max)
        return max;
    return value;
}

const v = clamp(1, 2, 3); // (>=1) & (<=2)

const a = 1;
const b = 2;
const c = clamp(a, b, 3); // (>=1) & (<=2)

// if one of the parameters is a `number`, the result would be widened and normalized:
let d: number = 1;
let e: 2 = 2;
let f = clamp(d, e, 3); // (>=number) & (<=2) -> number & (<=2) -> (<=2)

let h: number = 1;
let i: number = 2;
let j = clamp(h, i, 3); // (>=number) & (<=number) -> number & number -> number

💻 Use-Cases

We could statically type/document some APIs more explicitly, for example:

• Math.random
• Math.abs
• clamp
• Number.range
• Math.sin/cos/...
• a % b if a is assignable to (>=0) and b resolves to a number literal (falling back to number otherwise)
• [your example here]

Functions could express their assumptions about parameters.
They would be useful to force the developer to check if they are in range before passing (similar to literal types):

declare let a: number;

function takeProbability(p: (>=0) & (<=1)) { /* ... */ }

takeProbability(a); // Error, cannot assign number to (>=0) & (<=1)
if (a <= 1) {
    takeProbability(a); // Error, cannot assign number to (>=0)
    if (a >= 0) {
        takeProbability(a); // ok
    }
    takeProbability(a); // Error, cannot assign number to (>=0)
}

function takePercentage(p: (>=0) & (<=1)) { /* ... */ }
// in the case of takePercentage, the developer will notice that it expects something in the range of 0-1 instead of 0-100 because he will receive an error.

type SafeIntegerRange = (<= Number.MAX_SAFE_INTEGER) & (>= Number.MIN_SAFE_INTEGER);

Feel free to add more use-cases!

✅ Viability Checklist

• This wouldn't be a breaking change in existing TypeScript/JavaScript code
  • When interval types are not used, TS behaves the same
• This wouldn't change the runtime behavior of existing JavaScript code
• This could be implemented without emitting different JS based on the types of the expressions
• This isn't a runtime feature (e.g. library functionality, non-ECMAScript syntax with JavaScript output, new syntax sugar for JS, etc.)
• This feature would agree with the rest of TypeScript's Design Goals.
  • Subject for discussion

🔍 Search Terms / Keywords

• interval type
• interval primitives, boundaries

[nikeee]

I wanted to get into the TS compiler, so I've implemented a simple prototype of this type system extension. You can play around with it here:
https://nikeee.github.io/typescript-intervals

These features are not implement / have bugs:

• Discriminated unions (see above for reason why)
• Enum support
• Generics
• else branch sometimes does not receive the correct flow type

[captain-kark]

Some other things to explicitly disregard as goals, but may help steer design and discussion:

• positive vs. negative positional vectors
• periodic vs. aperiodic series
• convergent vs. divergent series

These features, if they existed, would allow for compile-time detection of changes to a value in a "direction" that is not supported. For instance, a model of a closed system with some variable representing a range of values for Entropy. Not only is it (>=0) & (<=1), it must always trend in one direction only.

From there, a periodic revolution allows for a "reversing" of the positional vector, but only if they exceed the threshold of the upper limit, and immediately returns to the lower limit. Support for this is not obvious to me, and would be difficult.

The third point is similar in that it's not obvious, but in my opinion would be even more difficult to do correctly. Given a positional vector and a limit, how can brief violations of this constraint be tolerated in order to facilitate convergent series for transcendental computed values, e.g., the approximation of φ from the Fibonacci series?

[RubenVerg]

I'm not sure I can just do this, but I'd like to suggest the % type where x extends (% y) (assuming both x and y are number literals) iff x % y == 0. This would effectively make type integer = (% 1) possible, as well. Interaction with <, > etc should probably be left untouched except maybe (> 0) & (< 5) & (% 3) should become 3, and (> 0) & (< 2) & (% 3) becomes never

Might've also been proposed already, but I couldn't find anything

[Stevemoretz]

So did it ever get implemeneted?

[Shinigami92]

Regarding to the roadmap, no.

[nikeee]

In its current state, it's just a proposal that is subject for discussion. So feel free to post some questions, use-cases and enhancements! :)

[benrbray]

This would be nifty! I ran into a use case while building a Markdown parser, that shows some interaction with template literal types as well. Here's a very simplified version:

type HeadingLevel = 1|2|3|4|5|6;

function makeHeading(level: HeadingLevel): HTMLHeadingElement {
	// already correctly inferred as a HTMLHeadingElement
	return document.createElement(`h${level}` as const);
}

function getHeadingLevel(text: string): HeadingLevel|null {
	let match = /(#{1,6}) (\w+)/.exec(text);
	if(match === null) { return null; }

	let pounds: string = match[1];
	// would be nice if this were inferred to be (>=0)
	let level = pounds.length;
	
	// interval types could help to avoid this cast!
	if(level > 0 && level <= 6) { return level as HeadingLevel; }

	return null;
}

let n = getHeadingLevel("#### heading");
if(n !== null) { makeHeading(n); }

[tamias]

Here's my use case. I want to define a union type for an API result, something like this:

type ApiResult<T> =
  | {
      total_results: 0;
    }
  | {
      total_results: 1;
      data: T;
    }
  | {
      total_results: number; // integer >= 2
      data: T[];
    };

so that I can later narrow the type by checking the value of total_results, e.g.:

let apiResult: ApiResult<string>;

if (apiResult.total_results > 1) {
  // apiResult.data is string[]
} else if (apiResult.total_results === 1) {
  // apiResult.data is string
} else {
  // apiResult.data is not present
}

[nikeee]

Maybe another wording could be something like "Inequality Types" originating from inequalities

[eczn]

is it inferable in extends clause ?

type MinRange<I extends number> = I extends (>= infer T) ? T : never;
type T0 = MinRange<(>= 100)>; // T0 will be 100