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.