Uniform Generics for Conditional Type Inference and Type Parameter Narrowing [Experiment]

[jack-williams]

This PR is an experimental implementation of uniform generics: Generic types that can only be instantiated with types that behave uniformly under typeof. This additional constraint makes it possible to apply new reasoning: something abit closer to dependent types.

• Narrowing via typeof applies to all values of a uniform type. See equalityTransUniform.
• Conditional types can be inferred from ternary expressions. See fn.

The notation for uniform generic types is:

function f<T!>(x: T, y: T) {
  ...
}

Type parameter T must be instantiated with a type that behaves uniformly under typeof, such as number, boolean, 1 | 2 | 3, but not number | boolean, any, or unknown.

This feature significantly benefits from #29317 and #29437.

The feature can also be extended to further uniformity constraints such as equality for enum members.

Examples (including ones from #22735 and #24929):

interface DependentPair<T!> {
    x: T;
    y: T extends string ? 1 : 0;
}

function dependentPair<T!>(mutual: DependentPair<T>) {
    let one: 1 = mutual.y; // error;
    const x = mutual.x;
    if (typeof x === "string") {
        one = mutual.y; // ok
    }
    return one;
}

/*
 * Infer conditional type. Propagate types between x1 and x2.
 */
function fn<T! extends string | number | boolean>(x1: T, x2: T): If<T, string, "s", If<T, number, "n", "b">> {
    if (typeof x1 === 'string' && typeof x2 === 'number') {
        return x1; // never, because this can never happen!
    }
    return typeof x1 === "string" ? "s" : typeof  x2 === "number" ? "n" : "b";
}

const tester1: "n" = fn<number>(3, 5)
const tester2: "b" = fn<boolean>(true, false)
const tester3: "s" = fn<string>("hello", "world");
const tester4: unknown = fn<string | number | boolean>(3, "world"); // error Type 'string | number | boolean' does not satisfy uniformity constraint of type 'T'. Values of type 'string | number | boolean'' do not behave identically under typeof [2752]

const enum TypeEnum {
    String = "string",
    Number = "number",
    Tuple = "tuple"
}

/* Example using uniform equality */

declare function doSomethingWithString(key: string): void;
declare function  doSomethingWithNumber(key: number): void;
declare function  doSomethingWithTuple(key: KeyTuple): void;

interface KeyTuple { key1: string; key2: number; }

type KeyForTypeEnum<T extends TypeEnum> 
    = T extends TypeEnum.Number ? number
    : T extends TypeEnum.String ? string
    : T extends TypeEnum.Tuple ? KeyTuple
    : never;

function doSomethingIf<TType~ extends TypeEnum>(type: TType, key: KeyForTypeEnum<TType>) {
    if (type === TypeEnum.Number) {
        // key has type KeyForTypeEnum<TType & TypeEnum.Number>,
        // so we resolve the conditional type
        return doSomethingWithNumber(key); 
    }
    if (type === TypeEnum.String) {
        // key has type KeyForTypeEnum<TType & TypeEnum.String>
        // so we resolve the conditional type
        return doSomethingWithString(key); // ok
    }
    if (type === TypeEnum.Tuple) {
        // key has type KeyForTypeEnum<TType & TypeEnum.Tuple>
        // so we resolve the conditional type
        return doSomethingWithTuple(key); // ok
    }
}

doSomethingIf(TypeEnum.String, "hello"); // ok
doSomethingIf<TypeEnum>(TypeEnum.String, 42); // error: Type 'TypeEnum' does not satisfy uniformity constraint of type 'TType'.

/*
 * Infer conditional type.
 */
function capitalize<T! extends string | string[]>(
  input: T
): If<T, string, string, string[]> {
    return typeof input === "string" ?
        (input[0].toUpperCase() + input.slice(1)) :
        (<T & string[]>input).map(elt => capitalize(elt)); // cast needed without negated types
}

const s: string = capitalize("hello");

/*
 * Type is inferred as If<T, string, T & string, null>
 */
function ensureString<T!>(bar: T) {
    return typeof bar === "string" ? bar : null;
}

const s3: string = ensureString(""); // correctly inferred as string
const null1: null = ensureString(1); // correctly inferred as null
declare function compareN(x: number, y: number): boolean;
declare function compareB(x: boolean, y: boolean): boolean;

function equalityTrans<T>(x: T, y: T): boolean {
    if (typeof x === "number") {
        return compareN(x, y); // error
    }
    if (typeof x === "boolean") {
        return compareB(x, y); // error
    }
    return false;
}

function equalityTransUniform<T!>(x: T, y: T): boolean {
    if (typeof x === "number") {
        return compareN(x, y); // ok: x and y are both T & number
    }
    if (typeof x === "boolean") {
        return compareB(x, y); // ok x and y are both T & boolean
    }
    return false;
}

/**
 * Uniformity constraints prevent bad instantiations
 */
equalityTransUniform(true, 3) // error
equalityTransUniform<boolean | number>(true, 3) // error: Type 'number | boolean' does not satisfy uniformity constraint of type 'T'. Values of type 'number | boolean' do not behave identically under typeof [2752]
equalityTransUniform<unknown>(true, 3) // error:  Type 'unknown' does not satisfy uniformity constraint of type 'T'. Values of type 'unknown' do not behave identically under typeof [2752]
equalityTransUniform<any>(true, true) // error
equalityTransUniform(true, true) // ok

function conditionalNarrow<T!>(x: T, cond: [T] extends [number] ? { x: string } : { y: string }) {
    if (typeof x === "number") {
        return cond.x
    }
    // need negation types
    // return cond.y
    return "foo";
}

conditionalNarrow(3, {x: 'hello'});
conditionalNarrow(true, {y: 'world'});
conditionalNarrow(3, {y: 'world'}); // error
conditionalNarrow<unknown>(3, {y: 'world'}); // error

/*
 * Inferred type is [T] extends [string] ? { x: T & string } : { y: T };
 * or, If<T, string, { x: T & string }, { y: T }>
 */
function foo<T!>(x: T) {
    return typeof x === "string" ? { x: x } : { y: x }
}

const x: { x: string } = foo('hello');
const y: { y: boolean } = foo(false);

[rubenpieters]

Could you expand a bit on how the following example works with your implementation?

function test1<T! extends number | boolean>(
    b: T
): T {
    if (typeof b === "boolean") {
        // unsafe, since T could be false
        return true;
    }
    return b;
}

Does it reject this program? It should be rejected, since if it is accepted it results in unsoundness if T is instantiated as false.

const b = test1<false>(false);
// b === true while it has the type false

[jack-williams]

The test1 function would still fail to type check: this feature still doesn't let you assign concrete values to generic things (a.k.a creating lower bounds on type parameters). In the if branch the type b would be narrowed to T & boolean, but this would still not allow true to be assigned because it doesn't satisfy the type T. Even when the type parameter is constrained to a singleton type, creating a lower bound is abit dubious.

The callsite const b = test1<false>(false); would type-check because the type false satisfies the uniformity constraint, but it's the body that would fail.

[rubenpieters]

Yes, that makes sense. I was just curious to see how it worked.

Even when the type parameter is constrained to a singleton type, creating a lower bound is abit dubious.

Do you have an example in mind where it would be unsound?

[jack-williams]

It depends on your definition of unsound - it's unlikely that code today would go observably wrong. The technical issue is that it violates parametricity, and various nice things you could learn from reading a type no longer apply. For instance.

declare function swap<T extends true>(t: readonly [true, T]): readonly [T, true];

One assertion that holds today might be that swap(x) !== x for all x because the input is readonly and you have to swap the input to get a T in the first position. If you allowed lower bounds this wouldn't be true:

function swap<T extends true>(t: readonly [true, T]): readonly [T, true] {
    if (t[1] === true) {
        return t; // as true <: T, and T <: true, therefore [true, T] <: [T, true]
    }
    return [t[1], t[0]];
}

I also generates issues if you ever add name subtyping, where you could have a named subtype like flow.

opaque type valid: true; // valid is a subtype of true, but true is not a subtype of valid

The claim then that narrowing a generic T using === true to yield true <: T would be false because T could be valid.

[sandersn]

This experiment is pretty old, so I'm going to close it to reduce the number of open PRs.

[typescript-bot]

This PR doesn't have any linked issues. Please open an issue that references this PR. From there we can discuss and prioritise.