Consistent intersection type with array and tuple

[Phryxia]

Suggestion

🔍 Search Terms

array, tuple, intersection, covariance, #32926, #33760

✅ Viability Checklist

My suggestion meets these guidelines:

• This wouldn't be a breaking change in existing TypeScript/JavaScript code
• 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.

⭐ Suggestion

I think this is rather theoretical approach for the behavior of intersection types and covariance for the consistency.

If this doesn't meet the design policy, feel free to close this.

📃 Motivating Example

Comprehension check for the intersection type and covariance

With my understanding of TypeScript and set theory, intersection type seems to obey following:

A & B ⊆ A
A & B ⊆ B

Also covariance/contravariance can alter the direction of such relation.

A ⊆ B

If F needs to be covariant:
F<A> ⊆ F<B>

then F<A> & F<B> is equivalent to F<A>

If F needs to be contravariant:
F<A> ⊇ F<B>

then F<A> & F<B> is equivalent to F<B>

Current behavior of finite/infinite computed property

Now consider the following object types

type Small = {
  [k in 'a' | 'b']: number
}

type Big = {
  [k in 'a' | 'b' | 'c']: number
}

let small: Small = { a: 1, b: 1 }
let big: Big = { a: 1, b: 1, c: 1 }

// small = big    // (OK)
// big = small    // (Invalid)

This makes sense. Note that this somehow behaves contravariant, while with the following behaves covariant.

type Big = {
  [k in string]: number
}

Here is the #playground for a glimpse.

What should be T[] & [T]?

It's basically nonsensical to intersect a tuple type with a variable-length array type;

I already read this from #33760 (comment) . But with the theoretical point of view, I just wonder whether this is helpful for the consistent implementation for future or not.

I don't know the implementation detail of this, but along the empirical tests, I think [T] is considered like:

[T] = {
  length: 1
  "0": T
  // and other array's properties
}

And T[] resembles:

T[] = {
  length: number
  [index in number]: T
  // and other array's properties
}

Currently, with TypeScript v4.7.4, the result is a little bit weird. #playground

type T = number[] & [number]
let t: T[1] // ??? no error
let len: T["length"] // 1

Is this because 0 is not computed property? How about [T, T] or [T, T, T]?

💻 Use Cases

Literal type 0 should be considered as finite subset of number, and by "Current behavior of finite/infinite computed property", the computed property of index, should be narrowed into 0. Note that length is already narrowed into 1.

// suggested behavior
type T = number[] & [number]
let t: T[1] // should be error or never
let len: T["length"] // 1

I understand that this might impractical, and nobody do number[] & [number]. But I'm not sure that, there is no guarantee for other complex composition never make such result. I hope this insight would be helpful for TypeScript team.

[RyanCavanaugh]

// suggested behavior
type T = number[] & [number]
let t: T[1] // should be error or never
let len: T["length"] // 1

I think this goes back to what ⊆ is understood to mean. One viewpoint -- not the only one you could have -- is that if an operation is valid on B, and A ⊆ B, then that same operation must be valid on A. T[1] is valid when T is number[], so it must be valid on number[] & [number]

The same subtyping/subsetting behavior might be observed on the indexing expression itself -- if T[number] is legal (which I think it absolutely must be in this case) then it can't be illegal to write T[1], since 1 is a subset of number.

[whzx5byb]

if an operation is valid on B, and A ⊆ B, then that same operation must be valid on A.

I agree but I think T[1] should be never here, as (A & B)[C] should have the same type as A[C] & B[C].

[Phryxia]

if an operation is valid on B, and A ⊆ B, then that same operation must be valid on A

I agree but I think T[1] should be never here, as (A & B)[C] should have the same type as A[C] & B[C].

I understood! As such operation have to be applicable. But its result has to obey the covariance property- never might be the answer.

[mlacorte]

Chiming in here to leave an opinion.

I'm implementing a type system for an unrelated project, and I've been sanity checking it by seeing how TypeScript handles these cases. I consider the following to be inconsistent behavior:

type Error = [1] & [1, 2]; // never
type Valid = { a: 1 } & { a: 1, b: 2 }; // { a: 1, b: 2 }

If differing array.length values should produce a type error, then differing Object.keys(object).length values should too.

Given how useful { a: 1 } & { b: 2 } is, the decision to ignore key length for the purpose of object intersections seems perfectly justifiable, but I think that decision should be applied consistently to tuples as well, unless there's a reason for the discrepancy that I'm not seeing.