Negated types

[weswigham]

Long have we spoken of them in hushed tones and referenced them in related issues, here they are:

Negated Types

Negated types, as the name may imply, are the negation of another type. Conceptually, this means that if string covers all values which are strings at runtime, a "not string" covers all values which are... not. We had hoped that conditional types would by and large subsume any use negated types would have... and they mostly do, except in many cases we need to apply the constraint implied by the conditional's check to it's result. In the true branch, we can just intersect the extends clause type, however in the false branch we've thus far been discarding the information. This means unions may not be filtered as they should (especially when conditionals nest) and information can be lost. So that ended up being the primary driver for this primitive - it's taking what a conditional type false branch implies, and allowing it to stand alone as a type.

Syntax

not T

where T is another type. I'm open to bikeshedding this, or even shipping without syntax available, but among alternatives (!, ~) not reads pretty well.

Identities

These are little tricks we do on negated type construction to help speed things along (and give negations on algebraic types canonical forms).

• not not T is T
• not (A | B | C | ...) is not A & not B & not C & not ...
• not (A & B & C & ...) is not A | not B | not C | not ...
• not unknown is never
• not never is unknown
• not any is any (since any is the NaN of types and behaves as both the bottom and top)

Assignability Rules

Negated types, for perhaps obvious reasons, cannot be related structurally - the only sane way to relate them is in a higher-order fashion. Thus, the rules governing these relations are very important.

• A negated type not S is related to a negated type not T if T is related to S.
  This follows from the set membership inversion that a negation implies - if normally a type S and a type T would be related if S is a subset of T, when we take the complements of those sets, not S and not T, those sets share an inverse relationship to the originals.
• A type S is related to a negated type not T if the intersection of S and T is empty
  We want to check if for all values in S, none of those values are also in T (since if they are, S is not in the negation of T). The intersection of S and T, when simplified and evaluated, is exactly the description of the common domain of the two. If this domain is empty (never), then we can conclude that there is no overlap between the two and that S must lie within not T.
• A negated type not S is not related to a type T.
  A negated type describes a set of values that reaches from unknown to its bound, while a normal type describes values from its bound to never - it's impossible for a negated type to satisfy a normal type

Assignability Addendum for Fresh Object Types

Frequently we want to consider a fresh object type as a singleton type (indeed, some examples in the refs assume this) - it corresponds to one runtime value, not the bounds on a value (meaning, as a type, both its upper and lower bounds are itself). Using this, we can add one more rule that allows fresh literal types to easily satisfy negated object types.

• A fresh object type S is related to a negated type not T if S is not related to T.
  Since S is a singleton type, we can assume that so long as it's type is not in T, then it is in not T.

Examples

Examples of negated type usage can be found in the tests of this PR (there's a few hundred lines of them, and probably some more to come for good measure), but here's some of the common ones, pulled from the referenced issues:

declare function ignore<T extends not (object & Promise<any>)>(value: T): void;
declare function readFileAsync(): Promise<string>;
declare function readFileSync(): string;
ignore(readFileSync());     // OK
ignore(readFileAsync());    // Should error

declare function map<T, U extends not void>(values: T[], map: (value: T) => U) : U[]; // validate map callback doesn't return void

function foo() {}

map([1, 2, 3], n => n + 1); // OK
map([1, 2, 3], foo);        // Should error

function asValid<T extends not null>(value: T, isValid: (value: T) => boolean) : T | null {
    return isValid(value) ? value : null;
}

declare const x: number;
declare const y: number | null;
asValid(x, n => n >= 0);    // OK
asValid(y, n => n >= 0);    // Should error

function tryAt<T extends not undefined>(values: T[], index: number): T | undefined {
    return values[index];
}

declare const a: number[];
declare const b: (number | undefined)[];
tryAt(a, 0);    // OK
tryAt(b, 0);    // Should error

Fixes #26240.
Allows #27711 to be cleanly fixed with a lib change (example in the tests).

Ref #4183, #4196, #7648, #12215, #18280

[DanielRosenwasser]

I'm not complaining, but why'd this go away?

[weswigham]

I accidentally fixed a bug where we duplicated the elaboration - this is as the same as the line above.

[DanielRosenwasser]

First take, without having tried this out:

• Intersections appear to be the correct mechanism to check for potential overlap, but that also means almost no object type can satisfy a negated object type. If we add negated types, I would prefer not to give the check up at all though.
• I find it weird, but understandable, that you treat fresh object types differently. But it's clearly weird that these are the only exception to the above issue.

I do have some reservations on the feature for these reasons. If you think about our features trying to satisfy convenience, intent, and safety, then I don't know if this appropriately weighs convenience and intent.

[weswigham]

Intersections appear to be the correct mechanism to check for potential overlap, but that also means almost no object type can satisfy a negated object type. If we add negated types, I would prefer not to give the check up at all though.

not (object & SomeInterface)

It works just dandy~

[DanielRosenwasser]

It works just dandy~

What do you mean? Yesterday you mentioned that you couldn't assign an array to a not PromiseLike<any>.

[weswigham]

Nope, you can't, because you can trivially make a

interface PromiseLikeArray extends Array<any> implements PromiseLike<any> { /*...*/ }

so, if you go to the example, I just state that I explicitly return an array that isn't PromiseLike - that is T[] & not PromiseLike<any>

[weswigham]

Per offline feedback from @ahejlsberg I've changed from ~ unary operator to a not keyword type operator (and updated all the text in this PR thus far to match). It does read nicer.

[Jessidhia]

Can this be used as a way to restrict the potential type of unbounded types? For example, number & not 0 to allow any number except the literal 0.

This doesn't look very useful at first glance but it can be powerful on mapped types. For example, [key in string and not keyof CSS.Properties<any>] in https://github.com/DefinitelyTyped/DefinitelyTyped/blob/e836acc75a78cf0655b5dfdbe81d69fdd4d8a252/types/styled-components/index.d.ts#L16-L25 could allow the constrained index signature to not have to include CSS.Properties<string | number>[keyof CSS.Properties<string | number>].

[weswigham]

Can this be used as a way to restrict the potential type of unbounded types? For example, number & not 0 to allow any number except the literal 0.

Yep. That's a primary driver for 'em.

[Jessidhia]

type Exact<T extends object> = T & Partial<Record<not keyof T, never>>

🤔

[jack-williams]

Is there an outline of how not interacts with narrowing? Might we have something like?

function foo(x: unknown) {
  if (typeof x === "number") {
    const num: number = x;
  } else {
    const numNot: not number = x;
  }
}

---

Assignability Addendum for Fresh Object Types

Is there a short example that demonstrates wanting a not for an object literal?

---

@DanielRosenwasser Do you mean something like { x: number } is not assignable to not { x: boolean } because { x : number} & { x: boolean } does not get reduced to never.

Meta question for @DanielRosenwasser: You say:

convenience, intent, and safety

that seem like some internal principles the TS team have for designing features? Is there a public description of these? I think it would help feature proposals if external contributors could frame their suggestions with the same language used internally.

---

@Kovensky I'm not sure that will type-check. The type not keyof T includes any type which isn't one of the keys, such as boolean. You might need:

type Exact<T extends object> = T & Partial<Record<(not keyof T) & string, never>>

though I'm not sure what the semantics will be for not types appearing in mapped type constraints.

[weswigham]

Is there an outline of how not interacts with narrowing? Might we have something like?

In this PR no negated types are produced by control flow yet; however we've talked over it and negated types make the lib type facts PR elegant to implement, since we can skip using conditionals (which don't compose well) and just filter with intersections of negated types :D

Is there a short example that demonstrates wanting a not for an object literal?

Aye, a test case with an example I pulled from a related issue:

// from https://github.com/Microsoft/TypeScript/issues/4183
type Distinct<A, B> = (A | B) & not (A & B);
declare var o1: {x};
declare var o2: {y};

 declare function f1(x: Distinct<typeof o1, typeof o2>): void;

 f1({x: 0});         // OK
f1({y: 0});         // OK
f1({x: 0, y: 0});   // Should error

though I'm not sure what the semantics will be for not types appearing in mapped type constraints.

Right now they're quietly dropped (aside from filtering out mismatching concrete types), like symbol for the same reason. There's no non-generic concept to map them into. I have a test to that effect. The arbitrary index signatures PR fixes this and would allow an index signature of a, say, string & not "". With that in place mapped types work correctly with 'em, since the intersections trivially desugar to an index signature.

[jack-williams]

@weswigham Thanks! And this PR is very cool :)

Re: the object literal example. Should that not be a case where EPC raises an error? I know it doesn't right now because there is no discriminant, but it probably should. Will using negation types become the canonical way of dealing with examples like this? If not, and assuming EPC does get fixed, are there many other use-cases for the special object literal relation.

[weswigham]

Re: the object literal example. Should that not be a case where EPC raises an error? I know it doesn't right now because there is no discriminant, but it probably should. Will using negation types become the canonical way of dealing with examples like this? If not, and assuming EPC does get fixed, are there many other use-cases for the special object literal relation.

Even if excess property checking makes defining a type like Distinct unneeded, you'd still need the relationship to allow a type like Distinct to be satisfiable (with fresh object types) should one be used.

[SalathielGenese]

Good job so far, I delayed some projects to wait for this feature - for more than a year.

[jack-williams]

Do these identities hold?
T & (not T) is never.
T & (not U) is T when T and U are disjoint.
"2b" | (not "2b") is unknown, or generally T | (not T) is unknown.

Just wondering what it would take to fix #28131

[weswigham]

T & (not T) is never.

Yes. More generally, when U extends T, U & not T is never.

T & (not U) is T when T and U are disjoint.

Yes.

"2b" | (not "2b") is unknown, or generally T | (not T) is unknown

More generally when U extends T, T | not U is just unknown (quite literally the opposite of the intersection into never rule). That's correct though I don't remember if I'd actually implemented this one yet - afaik we don't currently have any union identities that cause unions to "simplify" to unknown yet so I remember thinking about how it's best accomplished for a bit.

[DanielRosenwasser]

Do you really need to use this symbol? It almost sounds like a joke, but this could affect memory footprint when bootstrapping the compiler since modern engines can avoid full UTF16 representations https://blog.mozilla.org/javascript/2014/07/21/slimmer-and-faster-javascript-strings-in-firefox/

[peter-leonov]

A minification step will simply remove this line. The article suggests to minify the code to utilise the inline strings and also help with strings interning. I guess, v8 should not be so much different in this sense and also win from code minification.

[jack-williams]

@weswigham Seems to work, right?

type UnionToInterWorker<T> = not (T extends T ? not T : never);
type UnionToInter<T> = [T] extends [never] ? never : UnionToInterWorker<T>;

Not quite sure what should happen here:

type NotInfer<T> = T extends not (infer U) ? U : never;
type NotString = NotInfer<string> // string extends not U ? U : never;

Currently it doesn't reduce; maybe infer types should be disallowed under not?

[weswigham]

It doesn't reduce because we don't reduce reducible conditionals with infer's in them right now. IMO, it certainly still makes sense to allow an infer inside a not, since not A extends not infer B ofc should infer A for B.

[jack-williams]

Yep, you're right. I guess it could infer U = not string?

[qwelias]

Love coming back to this PR about once or twice a year because of not being able to do something.
Is there a chance to get any update on the state of it?

[kevinbarabash]

Would support for negated types make type inference involving conditional types easier and/or more powerful?

[sandersn]

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

[jsejcksn]

@sandersn Is that a "no" to negated types, or will the concept be tracked somewhere else now? If the latter, I'd like to know where so that I can subscribe to the new conversation.

[sandersn]

Not "no", but discussion should happen on an issue, #4196 probably, instead of a PR. PRs go stale.

[weswigham]

(Though admittedly the proposal in the PR description is admittedly way more concrete and detailed than anything in that issue rn, and the blockers for this are less about the syntax and behavior and more about implementation and performance + language complexity concerns, all of which are more tied to this PR specifically than the original idea)

[dimitropoulos]

while I certainly can relate to wanting to keep the PR count down to a manageable number (we have the same problem over on insomnia), I would like to echo the above from @weswigham. I've been following this conversation very closely for years, since it and #29729 are the two features I am the most interested in.

I guess at the end of the day as long as this PR isn't locked we can all keep talking here, but it'd be fantastic to have a better understanding of what needs to happen next for negated types to rise-the-ranks a little in the prioritization. I don't want to spam iteration plans (e.g. #49074) with my wants-and-needs... but I'm not sure what else to do at this point.

I hit the need for negated types on a weekly basis. Should I just drop those use-cases in here whenever I hit them?

[sandersn]

@dimitropoulos #49220 addresses the scenario in #29729 in a different way.

[falfiya]

Thanks for mentioning #49220. I didn't even know I had this problem till I read it. What I'm hearing is that I should follow future discussion of negated types in #4196? They'd be absolutely wonderful to have for stuff like "number without NaN".

[Autumn-one]

Why was such a basic and important feature rejected for a type system? That's a pity!

[MartinJohns]

@Autumn-one It wasn't rejected, the issue is still open: #4196

As to why it's not implemented yet? Priorities, time constraints, language constraints, limited resources. Feel free to fork the TypeScript repo and try to implement it, you'll see that it's not an easy task.