Repository: TypeScript
Issue: Suggestion: Uniform Type Predicate, or Concrete Types
Labels: Suggestion,In Discussion

## Suggestion: Uniform Type Predicate, or Concrete Types

### Summary 

Narrowing tells us information about a value but not so much about the type of the value, this is because a type may over approximate a value. The over approximation poses a problem when using multiples values of the same type: narrowing information is not sharable because over approximation can allow non-uniform behaviour with respect to operations such as `typeof` or `===`.

As a canonical example:

```ts
function eq<T>(x: T, y: T) {
  if (typeof x === "number") {
    // What do we know about y here?
  }
}
```
Inside the if branch what do we know about `y`, a variable with the same type as `x` that we know to be a number. Sadly, nothing. A caller may instantiate `T` to be `unknown` and therefore `y` could be any other value.

```ts
eq<unknown>(5, "not a number");
```

### Proposal

Support a way to define uniform, or concrete, types. A uniform type is one where all values of that type behave uniformly with respect to some operation. The idea is taken from Julia, where [concrete types](https://docs.julialang.org/en/v1/devdocs/types/index.html#Types-and-sets-(and-Any-and-Union{}/Bottom)-1) are defined as:

_A concrete type T describes the set of values whose direct tag, as returned by the typeof function, is T. An abstract type describes some possibly-larger set of values._

The obvious candidate of operation is `typeof`, but this could be extended to include equality for literal types, or key sets for objects.

### Basic Example

The introduction syntax is very much up for grabs, but for the examples we can use a constraint.

```ts
function eq<T extends Concrete<"typeof">>(x: T, y: T) {
  if (typeof x === "number") {
    // if x is number, then so is y.
  }
}
```

The constraint `Concrete<"typeof">` of `T` says that `T` may only be instantiated with types where all values of that type behave uniformly with respect to `typeof`. When `x` is a number, then so is `y`. The following call-sites demonstrate legal/illegal instantiations.

```ts
eq<unknown>(5, "not a number"); // Illegal: unknown is not concrete
eq<number>(5,4); // ok
eq<number | string>(5, "not a number also"); // Illegal, (number | string) is not concrete.
eq<4 | 2>(4, 2); // ok
```

### Examples from related issues (1)

#27808

```ts
declare function smallestString(xs: string[]): string;
declare function smallestNumber(x: number[]): number;

function smallest<T extends Concrete<number | string, "typeof">>(x: T[]): T {
    if (x.length == 0) {
        throw new Error('empty');
    }
    const first = x[0]; // first has type "T"
    if (typeof first == "string") {
        return smallestString(x); // legal
    }
    return smallestNumber(x);
}
```

We write `Concrete<number | string, "typeof">` for a type that is either a string or number, but is also concrete. As the values of the array are concrete, a single witness for `typeof` is enough to narrow the type of the entire array.

### Examples from related issues (2)

#24085

Here we show a use case for defining uniformity of equality.

```ts
const enum TypeEnum {
	String = "string",
	Number = "number",
	Tuple = "tuple"
}

interface KeyTuple { key1: string; key2: number; }

type KeyForTypeEnum<T extends TypeEnum> 
	= T extends TypeEnum.String ? string
	: T extends TypeEnum.Number ? number
	: T extends TypeEnum.Tuple ? KeyTuple
	: never;

function doSomethingIf<TType extends Concrete<TypeEnum, "===">>(type: TType, key: KeyForTypeEnum<TType>) {
  if (type === TypeEnum.String) {
    doSomethingWithString(key);
  }
  else if (type === TypeEnum.Number) {
    doSomethingWithNumber(key);
  }
  else if (type === TypeEnum.Tuple) {
    doSomethingWithTuple(key);
  }
}	
```

The issue presented here is that over-approximation leads to unsound uses:

```ts
doSomethingIf<TypeEnum>(TypeEnum.String, 42);
```

However with a concrete constraint `Concrete<TypeEnum, "===">` we enforce that the parameter is assignable to `TypeEnum`, however any instantiation must be uniform with respect to equality, restricting instantiations to singleton types. Example calls:

```ts
doSomethingIf<TypeEnum>(TypeEnum.String, 42); // Illegal: TypeEnum is not concrete
doSomethingIf<TypeEnum.String>(TypeEnum.String, "foo");  // Ok
doSomethingIf<TypeEnum.String | TypeEnum.Number>(TypeEnum.String, 42);  // Illegal: (TypeEnum.String | TypeEnum.Number) is not concrete.
```