Suggestion: Improve type reductions with absorption laws

[jcalz]

The type checker currently reduces/compares unions and intersections using the laws of idempotence (e.g., A & A = A), associativity (e.g., (A | B) | C = A | (B | C)), commutativity (e.g., A & B = B & A), and distributivity (e.g., A | (B & C) = (A | B) & (A | C)).

• I think it would be great to introduce the absorption laws: That is, A | (A & B) and A & (A | B) should reduce to A.

• Related are laws of subtype collapsing; that is, if B extends A, then A | B should reduce to A, and A & B should reduce to B. (Issue Spec Preview: Union types #805 implies that this already happens for unions, but I am not seeing the type checker doing an actual reduction.)

• Finally, maybe slightly off-topic, it would be nice to reduce intersections of known-disjoint types to never or undefined|null depending on the strictness of null checks.

---

I should note that currently the type checker does consider all such equivalent types mutually compatible (meaning that a value of type A | (A & B) can be assigned to a variable of type A and vice-versa), even though they don't reduce to the same type. This is good, but actual reductions for absorption laws would:

• improve completeness (right now there are expressions incorrectly flagged as type errors)
• increase transparency/legibility (neither the type checker nor developers should want to drag around such unwieldy beasts as string & (string | number) & (string | object) & (string | {ad: number, nauseum: string}) when string would be better for everyone involved).

I don't know how expensive it would be to perform such reduction rules in the compiler. Before I or anyone looks into that, though, I'd be interested in finding out if such a feature would even be considered useful. Thoughts?

---

Code examples! Everywhere below that produces the error // Error, subsequent variable declarations must have the same type should type-check:

var o = {};

// Absorption Law
function absorption<A, B>() {
  var x: A & (A | B);
  var x: A | (A & B);
  var x: A; // Error, subsequent variable declarations must have the same type.

  // but these assignments work
  var y: A = o as A | (A & B);
  var z: A | (A & B) = o as A;
}

// Subtype Collapsing
function absorptionExtends<A, B extends A>() {
  var x: A & B;
  var x: B; // Error, subsequent variable declarations must have the same type.

  // but these assignments work
  var y: B = o as A & B;
  var z: A & B = o as B;

  var u: A | B;
  var u: A; // Error, subsequent variable declarations must have the same type.

  // but these assignments work
  var v: A = o as A | B;
  var w: A | B = o as A;
}

// Intersections of known-disjoint types:
var x: string & number
x = '0'; // Error as expected
x = 0; // Error as expected
x = undefined; // Error as expected with strictNullChecks 
x = null; // Error as expected with strictNullChecks 
// but
var x: undefined | null; // Error, subsequent variable declarations must have the same type.
var x: never; // Error, subsequent variable declarations must have the same type.

// EDIT: maybe plays badly with tagged types?
var y: string & object;
y = 'hmm'; // Error as expected
y = {}; // Error as expected
y = undefined; // Error as expected with strictNullChecks  
y = null; // Error as expected with strictNullChecks
// but
var y: undefined | null; // Error, subsequent variable declarations must have the same type.
var y: never; // Error, subsequent variable declarations must have the same type.


/*---*/

// if absorptionExtends is too expensive in general, 
// at least some specifics for string/number literals would be nice:
absorptionExtends<string, 'a' | 'b'>();
absorptionExtends<number, 0 | 1>();

// bottoms should absorb all intersections and be absorbed by all unions
// but see https://github.com/Microsoft/TypeScript/issues/16038
function neverAbsorption<T>() {
  absorptionExtends<T, never>();
}

// tops should absorb all unions and be absorbed by all intersections
function emptyObjectAbsorption<T>(){
  absorptionExtends<{}, T>();
}

// I guess "any" is a special case
// as mentioned in https://github.com/Microsoft/TypeScript/issues/10715
function anyAbsorption<T>() {
  absorptionExtends<any, T>();
  absorptionExtends<T, any>();
}

// here we build up a complex type with a simple reduction
var i: string;
var j: typeof i | number;
var k: typeof i | object;
var l: typeof i | { ad: number, nauseum: string };
var m: typeof i & typeof j & typeof k & typeof l;

// let's look at typeof m:
var m: string | (string & { ad: number; nauseum: string; }) | (string & object) |
  (string & object & { ad: number; nauseum: string; }) | (string & number) |
  (string & number & { ad: number; nauseum: string; }) | (string & number & object) |
  (string & number & object & { ad: number; nauseum: string; }); 
// yuck! typeof m should be string
var m: string; // Error, subsequent variable declarations must have the same type.

//  but these assignments work
var n: string;
n = m;
n = null;
m = n;

Cheers!

[jcalz]

Does this issue deserve a "suggestion" tag, or is something wrong with it? 😞 Thanks.

[sandersn]

Nothing's wrong with the proposal, we just have a lot of the team on vacation this summer so we haven't had a chance to look at it.

I'm curious whether you've run into real code that would benefit from this proposal.

[jcalz]

I'd have to go back and look at what I was working on in June to answer definitively, but the problem surfaced for me in some confusing types reported by quickInfo (e.g., string | (string & number) & (string & boolean)).

I have since come to understand that this might not play nicely with excess property checking on object literals (A | (A & B) accepts object literals of type A & B but A in general doesn't), and that inferring never for intersections of known-disjoint types might not play nicely with tagged types (one of the workarounds for nominal typing). Still, there might be some benefit to absorption.

[KiaraGrouwstra]

The nominal typing workaround seems kind of hacky, perhaps there'd be some better way to do that.

[KiaraGrouwstra]

I figured this idea might merit trying in a branch to see how it'd work out, so I tried to think of what it means for two types to clash.

My intuition is they match if they are assignable two each other in either direction, or are objects (non-primitives) and none of their properties/indices clash.

In the latter case perhaps the reduction should be local though, e.g. { a: 1 } & { a: 2 } to { a: never }, so as to reduce information loss.

Then again, can we really reduce to never? For LHS roles this seems okay, as you're just simplifying an impossible requirement. For RHS roles though, if 1 & 2 would reduce to never, that would suddenly also start sub-typing things like boolean, as never sub-types anything.

I'm not sure I'm making sense here. Thoughts, @jcalz?

[jcalz]

So you're saying that the following:

const b: boolean = Object.assign(1 as 1, 2 as 2);

which currently errors (Type '1 & 2' is not assignable to type 'boolean'), would no longer error and that would lead to more confusion and less error catching. Yeah, I don't like that much either.

I also don't like this:

const x = 'x'
if (x !== 'x') {
  const b: boolean = x; // no error
}

which is current TS behavior.

It's times like these I wish there were a difference between warnings and errors in TS (or there were a way to acknowledge and dismiss individual errors). When TS notices that you're shuttling nevers around, it would be nice for it to say something like this expression has reduced to 'never' here; are you sure you want to be using it?, and you could silence the warning by doing something explicit like

const a: boolean = Object.assign(1 as 1, 2 as 2); // error: impossible type; are you sure?
const b: boolean = Object.assign(1 as 1, 2 as 2) as never; // no error

I don't know if this warning-on-never idea is worthy of a separate suggestion that would help TS development in general, or is not really useful unless we start aggressively reducing impossible types to never.

[RyanCavanaugh]

The problem is that never values are created and assigned out in a lot of correct places

function fn(): string {
  switch(something) {
    case A.X: return "";
    default: return Debug.fail("nope"); // Debug.fail returns `never`
}

There'd need to be some very strong distinguishing mechanism that still allows this but disallows some other usage.

[KiaraGrouwstra]

Could valid/bad cases be distinguished using say void vs. never? Just blurting out ideas here.

[jcalz]

I have the vague sense that an explict throw should not warn about never, and neither should any function call whose return value is declared to be never, or any expression which is asserted or declared to be never, but that anything which the type checker narrows from some non-never type to never might warrant a warning. This is making me think I'm asking for two nevers; one which is tagged as explicit, and the other tagged as implicit. Implicit never is a warning; explicit never is not.

[RyanCavanaugh]

@jcalz I think the spirit of this issue is fixed - would you agree?

[jcalz]

Is it? I think that there's definitely been some improvement here, but the basic issue, that something like

type ShouldBeString = string & (string | number | boolean)

expands to string | (string & number) | (string & true) | (string & false) instead of reducing to string persists. Type manipulation tends to produce these things occasionally. I can imagine it's not a priority for anyone though. 🤷‍♂️

[RyanCavanaugh]

The display text shows this, but the behavior is the same as string because the conflicting-intersection types (string & boolean) turn into never and ultimately vanish from the union:

type ShouldBeString = string & (string | number | boolean);
// No error
var t: ShouldBeString = "";

[jcalz]

Wasn't that also true when I originally filed this? When you get down to using actual values with concrete types, it's all good. I think some more aggressive reductions to never have occurred since then, but there are still cases where the type checker complains (the generics in the examples). But as I said, in practice probably few people run into this issue.

One interesting development is that conditional types now allow someone to more closely express these operations like so:

type AbsorbUnion<T, U> = T extends U ? U : U extends T ? T : T | U 
type AbsorbIntersection<T, U> = T extends U ? T : U extends T ? U : T & U

type ShouldBeString = AbsorbIntersection<string, string | number | boolean> // string

which is neat.

[RyanCavanaugh]

It's sounding like there isn't anything concrete in terms of resulting behavior? The intermediate forms the types take during expansion/reduction is sort of an implementation detail as long as the resulting subtype relationships are correct.

[jcalz]

Yes, that's true. The benefit would mostly be in Intellisense quick info and any type-level manipulation that relies on absorption to work (which can probably be worked around with AbsorbUnion/AbsorbIntersection above). And that benefit is questionable in the face of excess property checking, where something like Cat | Animal is observably different from Animal when assigning fresh object literals.

So what do you think? Fixed? Declined?

[RyanCavanaugh]

Fixclined?

[rob3c]

The intermediate forms the types take during expansion/reduction is sort of an implementation detail as long as the resulting subtype relationships are correct.

@RyanCavanaugh Are you saying that the way a type is shown to the user doesn't matter, as long as the compiler evaluates expressions equivalently? I definitely don't want to be mentally reducing type expressions just to figure out what is acceptable in a given context. It doesn't seem to me that anything seen by a user is merely an implementation detail. If the compiler needs some extra time to simplify an expression, I suspect most users would need even more time :-)

[RyanCavanaugh]

Of course it matters.

It's a trade-off. If you write a type alias

type T = some_type_expression;

people will log bugs if a hover on T shows anything but exactly what they wrote.

For a type like T & (A | B | C) it's much preferable to show the original form than T & A | T & B | T & C - the latter is more confusing even though it's the "simplified" internal form.

[masaeedu]

@RyanCavanaugh subjective, but if T showed me anything but exactly what I wrote, I'd probably go "oh, neat" and copy paste that to the RHS (assuming of course that it was simpler than what I wrote).

[RyanCavanaugh]

For example, I think this behavior is bad, even though it's a technically correct "simplification" of the original type

[masaeedu]

@RyanCavanaugh I agree with you that the behavior seen is really ugly, but it seems this is a result of distributing over the components of enum/type types rather than treating them as indivisible. You could still treat enum A as indivisible when simplifying representations and provide the desired behavior of eliminating A & B as never when they're disjoint (or A | B as A when B extends A, etc.). In both cases the resulting type is always shorter than the original type expression whenever the rule is applicable.

PS: Shouldn't that whole type be never?

[masaeedu]

Putting this another way, the debate should be between type T = A & { p: any } showing A & { p: any } and showing never. We don't get A & { p: any } either today (instead we get that exploded type you illustrated), but that's orthogonal to this issue I think.

[rob3c]

haha so I'm glad I misunderstood you, and it's really a matter of the much trickier question of finding the right 'simplification' to show the user.