Intersection of conditional types, acting on a generic type, with another type doesn't narrow the generic type

🔎 Search Terms

intersect
conditional
generic
narrow
typeof
function
callable
ts2349

🕗 Version & Regression Information

This is the behavior in every version I tried, and I reviewed the FAQ for entries about narrowing.

⏯ Playground Link

https://www.typescriptlang.org/play?target=99&jsx=0#code/C4TwDgpgBAKgFgVwHYGsA8BBAfFAvFACgEo8cMBuAKEtEigDkB7JAMWQGNgBLZzHfDFAgAPYBCQATAM5Q2STjyRQA-FCQQAbhABOUAFxQK1WtACiwsNr55YiVNYA+DZnIW9sVSu2ZTgQjQCGADYIAWI2fAQilgbmlnxEBoK4WJRQUCaMAGZCFrq4BVAARFkc3MxFKrmWxPrV2lTpAPRN6W3tHZ1dAHq93WlQLVAAtKNj4xOTU9Mzs3PzUwND8Fwy0doQUlKKUKtqjH7swUEBAEZBEAB0S63pTH7HUN5IvlzACOLAMtkZ4NAA5PBkOhsFAnAQmKwyoprAAyWTQ5hEf5QAIbJ7HM4Xa7NW5tGB-KD-SGucpIOEI+RklFwAIyJCMDFBIJQbYAcyQYQQGykl0IACYAMwAFgAnEQbiMFtKZbK5TNJQQwGiAgBbCBibQkdYGIH2UHgkmI8mg+GkxQS3FS+U2212iaUIA

💻 Code

type Thunk<A> = () => A;

type NonFunction<A> = A extends Function ? never : A;

type Expr<A> = Thunk<A> | NonFunction<A>;

const evaluate = <A>(expr: Expr<A>): A =>
  typeof expr === "function" ? expr() : expr;
  //                           ^^^^
  // -------------------------------------------------------------------------------------
  // This expression is not callable.
  //   Not all constituents of type 'Thunk<A> | (NonFunction<A> & Function)' are callable.
  //     Type 'NonFunction<A> & Function' has no call signatures. (2349)
  // -------------------------------------------------------------------------------------
  // (parameter) expr: Thunk<A> | (NonFunction<A> & Function)
  // -------------------------------------------------------------------------------------

🙁 Actual behavior

The parameter expr, which has the type Expr<A>, is being narrowed by the typeof expr === "function" condition. When the condition is true, the type of expr is narrowed to Thunk<A> | (NonFunction<A> & Function). When the condition is false, the type of expr is narrowed to NonFunction<A>.

🙂 Expected behavior

When the condition is true, the type of expr should be simplified to just Thunk<A>.

  Thunk<A> | (NonFunction<A> & Function)
= Thunk<A> | ((A extends Function ? never : A) & Function)          // (1) by definition
= Thunk<A> | (A extends Function ? never & Function : A & Function) // (2) distributivity
= Thunk<A> | (A extends Function ? never : A & Function)            // (3) annihilation
= Thunk<A> | (A extends Function ? never : never)                   // (4) law of non-contradiction
= Thunk<A> | never                                                  // (5) simplification
= Thunk<A>                                                          // (6) identity

The challenging step to understand is step number 4 where we invoke the law of non-contradiction to simplify the type A & Function to never. The law of non-contradiction states that some proposition P and its negation can't both be true. In our case, the proposition is Function. Since A & Function is in the else branch of the conditional A extends Function, it implies that A is not a function. Hence, A and Function are contradictory. Thus, by the law of non-contradiction we should be able to simplify it to never.

In plain English, NonFunction<A> & Function is a contradiction. A type can't both be a Function and a NonFunction<A> at the same time. Hence, the type checker should simplify NonFunction<A> & Function to never.

At the very least, NonFunction<A> & Function should be callable. We shouldn't get a ts2349 error.

Additional information about the issue

I understand that as TypeScript is currently implemented, NonFunction<A> & Function doesn't simplify to never for all possible types A. For example, consider the scenario when A is unknown.

  NonFunction<unknown> & Function
= (unknown extends Function ? never : unknown) & Function // (1) by definition
= unknown & Function                                      // (2) simplification
= Function                                                // (3) identity

This seems to be because in step number 2 we're simplifying unknown extends Function ? never : unknown to just unknown. Instead, we should simplify it to unknown & !Function where the ! denotes negation, i.e. an unknown value which is not a function. Then we can apply the law of non-contradiction to get the correct type.

  NonFunction<unknown> & Function
= (unknown extends Function ? never : unknown) & Function // (1) by definition
= (unknown & !Function) & Function                        // (2) simplification
= unknown & (!Function & Function)                        // (3) associativity
= unknown & never                                         // (4) law of non-contradiction
= never                                                   // (5) annihilation

At the very least, this seems to suggest the need for some sort of negation type.

At the very least, this seems to suggest the need for some sort of negation type.

#4196

It's actually not true that NonFunction<A> & Function is a contradiction in TypeScript. Because object types are not sealed¹, intersecting objects with disjoint sets of properties merges them, and function types have a special pseudo-property called a "call signature". So:

type NonFunction<A> = A extends Function ? never : A;
type Fun = () => void;
type Obj = { foo: string };
type MoreFun = NonFunction<Obj> & Fun;
declare const foo: MoreFun;
foo.foo;  // ok
foo();    // also ok

Which, for those keeping score, also implies that a NonFunction<A> may be a function in reality, and you've just forgotten its call signature. The call signature can be reintroduced via type intersection. ↩

Bruce Pascoe (@fatcerberus)

Bruce Pascoe (@fatcerberus) Can you give me a real life example of how you would construct a value of type MoreFun in JavaScript?

function foo() {
    console.log("you fooey bard!")
}
foo.foo = "foo";

All functions are objects in JavaScript.

Bruce Pascoe (@fatcerberus)

Bruce Pascoe (@fatcerberus) I understand that. In fact, I wrote about this very issue in the Additional information about the issue section.

I understand that as TypeScript is currently implemented, NonFunction<A> & Function doesn't simplify to never for all possible types A.

However, that's what I think is wrong. I think that in your example MoreFun should simplify to never. In fact, I think that NonFunction<T> & F, for all types T and for all types F which extend Function, should simplify to never.

Note that I have no issue with the type Obj & Fun. I only have an issue with the type NonFunction<Obj> & Fun. I think it's a mistake for NonFunction<Obj> to simplify to Obj. I think it should simplify to Obj & !Function. Hence, NonFunction<Obj> & Fun should simplify to never as follows.

  NonFunction<Obj> & Fun
= (Obj & !Function) & Fun // by definition
= Obj & (!Function & Fun) // associativity
= Obj & never             // law of non-contradiction
= never                   // annihilation

It's not practical for every possible non-inhabitable type to be simplified to never -- this requires a potentially unbounded amount of work. Because it can't be done, it's not an invariant you should be trying to take a dependency on.

Note that I have no issue with the type Obj & Fun. I only have an issue with the type NonFunction<Obj> & Fun

But that's the thing - those are the same type. Type aliases are just type-functions - NonFunction<Obj> "returns" Obj, so in the end you are just doing Obj & Fun. TS doesn't go back and reevaluate the conditional type every time you manipulate it - that's not how they work.

I think [NonFunction<Obj>] should simplify to Obj & !Function.

If we had negated types, you could just write the latter directly, but I disagree that that's what the conditional type you wrote should simplify to. Ternary expressions aren't retroactive at runtime, so I wouldn't expect the typespace equivalent to be either.

Note that I have no issue with the type Obj & Fun. I only have an issue with the type NonFunction<Obj> & Fun

But that's the thing - those are the same type. Type aliases are just type-functions - NonFunction<Obj> "returns" Obj, so in the end you are just doing Obj & Fun. TS doesn't go back and reevaluate the conditional type every time you manipulate it - that's not how they work.

Yes, NonFunction<Obj> "returns" Obj currently but that's a defect of the type system, which is why I created this issue.

The type NonFunction<Obj> should return Obj & !Function. You don't need to go back and re-evaluate the conditional type. Just make the conditional type return Obj & !Function.

By simplifying NonFunction<Obj> to just Obj, we're losing type information. In particular, we're losing the information that we checked whether Obj is a function and we found out that it isn't a function. The check is the important part here.

I think [NonFunction<Obj>] should simplify to Obj & !Function.

If we had negated types, you could just write the latter directly, but I disagree that that's what the conditional type you wrote should simplify to. Ternary expressions aren't retroactive at runtime, so I wouldn't expect the typespace equivalent to be either.

True, if we had negated types then I could define NonFunction as follows, which by the way is oh so perfect.

type NonFunction<A> = A & !Function;

However, I disagree with the second part of your statement. A conditional type of the form A extends B ? never : A should simplify to A & !B for all types A and B. And, here's the proof.

First, we need to understand what A extends B denotes. Turns out, extends denotes material implication. If A extends B then we should be able to substitute a value of type A everywhere a value of type B is expected. That is, A should be "assignable" to B. In propositional logic, we would write this as $A \to B$.

Next, the never type denotes falsehood and is represented as $\bot$ in propositional logic. Finally, any conditional type P ? Q : R can be represented as the conjunction of two conditionals $(P \to Q) \land (\neg P \to R)$ in propositional logic.

Putting it all together, the conditional type A extends B ? never : A would be represented in propositional logic as $((A \to B) \to \bot) \land (\neg (A \to B) \to A)$. However, $P \to \bot$ is the same as $\neg P$. Hence, the proposition can be simplified to $\neg (A \to B) \land (\neg (A \to B) \to A)$.

At this point, we can use the modus ponens rule to infer that $A$ is a true proposition. However, inference is not the same as simplification. Yes, $(\neg (A \to B) \land (\neg (A \to B) \to A)) \to A$ is a true proposition. However, $\neg (A \to B) \land (\neg (A \to B) \to A) \neq A$. Since, $P \land (P \to Q)$ simplifies to $P \land Q$, we can simplify $\neg (A \to B) \land (\neg (A \to B) \to A)$ to $\neg (A \to B) \land A$.

Finally, $\neg (A \to B) \land A$ can be simplified to $\neg (\neg A \lor B) \land A$ because $P \to Q$ is equivalent to $\neg P \lor Q$. Next, by De Morgan's law we can further simplify $\neg (\neg A \lor B) \land A$ to $(A \land \neg B) \land A$. And, now we can trivially see that $(A \land \neg B) \land A$ is just $A \land \neg B$.

Now, you might be think that there's some flaw in my argument because I'm treating types as propositions. After all, types are not the same as propositions. But, the Curry—Howard isomorhpism is proof that types and propositions are indeed equivalent. It's one of the seminal theorems of computer science.

In conclusion, A extends B ? never : A should simplify to A & !B. Inference is not the same as simplification. Yes, A extends B ? never : A implies A. However, it also implies !B.

It's not practical for every possible non-inhabitable type to be simplified to never -- this requires a potentially unbounded amount of work. Because it can't be done, it's not an invariant you should be trying to take a dependency on.

I understand that the solution this for this problem might take a lot of work to implement, and therefore it's not something that you want to solve. However, this is indeed a defect of the type system as I demonstrated using propositional logic above. Hence, I don't think the "Not a Defect" label is justified here.

To be fair, I can easily solve this problem using type guards.

type Thunk<A> = () => A;

type NonFunction<A> = A extends Function ? never : A;

type Expr<A> = Thunk<A> | NonFunction<A>;

const isThunk = <A>(expr: Expr<A>): expr is Thunk<A> =>
  typeof expr === "function";

const evaluate = <A>(expr: Expr<A>): A =>
  isThunk(expr) ? expr() : expr;

However, I expected TypeScript to correctly narrow the type of expr to Thunk<A> even without type guards. It's quite obvious that an inhabitant of Expr<A> can only be a function if it's an inhabitant of Thunk<A>.

The type NonFunction<Obj> should return Obj & !Function. You don't need to go back and re-evaluate the conditional type. Just make the conditional type return Obj & !Function.

That would make the conditional type retroactive, which, again, is not how they work. That would be like writing a function:

function nonString(x) {
    // let's assume throw expressions are available for brevity
    return typeof x !== 'string' ? x : throw Error("no strings allowed!");
}

and then expecting it to throw if, at any point, x is transformed into a string, such as by calling String(x). In other words NonFunction<Obj> & Fun is completely analogous to calling String(nonString(x)) at runtime.

A conditional type is a computation done on a type at compile time, not a new kind of "dynamic type".

I understand that the solution this for this problem might take a lot of work to implement, and therefore it's not something that you want to solve

The problem literally isn't computable. It's not for lack of desire to compute BB(12) that I haven't.

That would make the conditional type retroactive, which, again, is not how they work.

I don't understand what you mean by "retroactive". Could you please provide a definition for this term? This is the second time you've used this term and I'm honestly confused as to what you're trying to convey.

Also, could you please elucidate the following statement?

Ternary expressions aren't retroactive at runtime, so I wouldn't expect the typespace equivalent to be either.

Again, I don't understand what you mean by "retroactive" and hence I don't understand what "typespace equivalent" means in this sentence either.

That would be like writing a function:
function nonString(x) {
    // let's assume throw expressions are available for brevity
    return typeof x !== 'string' ? x : throw Error("no strings allowed!");
}
and then expecting it to throw if, at any point, x is transformed into a string, such as by calling String(x). In other words NonFunction<Obj> & Fun is completely analogous to calling String(nonString(x)) at runtime.

Your analogy is wrong. If you want to view types as values then you should reify them as predicates. The predicate takes any value, and returns true if and only if that value satisfies the type that the predicate reifies.

// Analogous to the type `unknown`.
const unknown = () => true;

// Analogous to the type `Function`.
const func = (x) => typeof x === "function";

// Analogous to the type `NonFunction<A> = A & !Function`.
const nonFunc = (t) => (x) => t(x) && !func(x);

// Analogous to the type `A & B`.
const intersect = (t1, t2) => (x) => t1(x) && t2(x);

// Analogous to the type `NonFunction<A> & Function`.
const nonFuncAndFunc = (t) => intersect(nonFunc(t), func);

// Analogous to the type `never`.
const absurd = nonFuncAndFunc(unknown);

console.log(absurd(42));       // false
console.log(absurd(() => 42)); // false

As you can see, the absurd type always returns false no matter what its input is. This is because a value can't both be a non-function and a function at the same time.

Also note that the intersect type constructor requires that the same value satisfy both the types provided. I mention this to refute your statement about x somehow transforming into String(x). x doesn't transform into String(x). They are two separate values. Hence, your analogy fails there.

Anyway, you might have noticed that I defined NonFunction<A> as A & !Function instead of A extends Function ? never : A. This was on purpose because I want to pose two questions two you.

If TypeScript supported negated types and NonFunction<A> was defined as A & !Function, would you agree then that NonFunction<A> & Function should simplify to never? If not, why?
If I showed you a step-by-step mechanical way to simplify A extends Function ? never : A to A & !Function, would you agree that they are indeed equivalent? By mechanical, I mean that I'll provide a computer algorithm which will reduce A extends Function ? never : A to A & !Function in a finite number of steps regardless of the type A. This means that we'll literally be able to implement said algorithm in the TypeScript type system.

A conditional type is a computation done on a type at compile time, not a new kind of "dynamic type".

So is the algorithm I have in mind to simplify A extends Function ? never : A to A & !Function.

The problem literally isn't computable.

Interesting, so you're telling me that this particular problem is undecidable? I would love to understand why. Would you explain it to me?

It's not for lack of desire to compute BB(12) that I haven't.

What is "BB(12)"?

More concretely:

type NonDog<T> = T extends Dog ? never : T;
type Test = NonDog<Animal>;

You asked whether Animal was assignable to Dog. It's true that it isn't. If you then narrow T to T & !Dog in the false branch, you're asserting that Dog is not assignable to the original T, which is false.

Bruce Pascoe (@fatcerberus)

I think I might see where you're coming from here; you envision the A as being narrowed in the false branch due to the extends check, making it not an identity in that context. Even so, what you propose is still incorrect: T = A & !Function implies that F extends T is false for all types F extends Function, which is something that was not checked in the conditional type. So the proposed narrowing is still wrong, even if negated types existed.

Bruce Pascoe (@fatcerberus) Let me formalize what you're saying so that I understand it.

Let's represent the type Function as the proposition $F$.
T = A & !Function can be represented as the proposition $T = \neg (A \to F)$.
F extends Function can be represented as the proposition $G \to F$.
I used $G$ to represent F because $F$ represents Function.
F extends T can be represented as $G \to T$ which is $G \to \neg (A \to F)$.
So, what you're saying is that $\forall A. \neg (A \to F)$ implies $\forall G. (G \to F) \to \neg (G \to \neg (A \to F))$.
In plains words, if A is not a function and G is a function then G can't be assigned to A.

That makes sense to me. I don't see any problem here. $\forall A. \neg (A \to F) \to \forall G. (G \to F) \to \neg (G \to \neg (A \to F))$ is indeed true.

I certainly don't see how the proposed narrowing is wrong.

tl;dr is that, in general, T extends U being true or false only tells you whether T is assignable to U but says nothing about whether U is assignable to T. So it doesn't make sense to set T = T & !U in the false branch of said check.

Why would you even care if U is assignable to T? The proposition T extends U is just material implication. It's equivalent to $T \to U$. The negation of $T \to U$ is not $U \to T$. The negation of $T \to U$ is material nonimplication, i.e. $\neg (T \to U)$.

$T \to U$ is equal to $\neg T \lor U$.
$\neg (T \to U)$ is equal to $\neg (\neg T \lor U)$ which is $T \land \neg U$.

So, it makes perfect sense to set T = T & !U in the false branch.

More concretely:
type NonDog<T> = T extends Dog ? never : T;
type Test = NonDog<Animal>;
You asked whether Animal was assignable to Dog. It's true that it isn't. If you then narrow T to T & !Dog in the false branch, you're asserting that Dog is not assignable to the original T, which is false.

You don't make any sense. If T is Animal, then T & !Dog is Animal & !Dog. It represents the values which are assignable to Animal but not assignable to Dog, which makes perfect sense. Nowhere are we asserting that Dog is not assignable to Animal.

Animal & !Dog is not the same as !(Dog extends Animal) because !(Dog extends Animal) simplifies to Dog & !Animal.

Nowhere are we asserting that Dog is not assignable to Animal.

In fact you are. Animal & !Dog means, as you say, "value which is assignable to Animal but not assignable to Dog", i.e. it's a set which contains no dogs. It is not valid to conclude that, just because T is not a subset of Dog, that T contains no dogs. The conditional type expression operates on the entire type, not individual members of it, or even individual subtypes (modulo distribution over union types)

I literally don't see the check for Dog extends T anywhere in your example. And, Animal & !Dog is literally assignable to Animal.

type Animal = Cat | Dog | Horse;

type NotDog = Animal & !Dog; // equivalent to Cat | Horse

declare const cat: Cat;

const notDog: NotDog = cat;

const animal: Animal = notDog;

It is not valid to conclude that, just because T is not a subset of Dog, that T contains no dogs.

We're not concluding that Animal contains no dogs. We're concluding that Animal & !Dog contains no dogs. There's a very big difference.

You're arguing that !(T extends Dog) always implies T & !Dog, which is not true, because T might be (and is, in my example) Animal. Dog | Cat | Horse is not a subset of Dog, but it still contains dogs. Cat | Horse contains no dogs, so you've changed the meaning of the original type by narrowing it.

You're arguing that !(T extends Dog) always implies T & !Dog, which is not true, because T might be (and is, in my example) Animal.

Yes, !(T extends Dog) always implies T & !Dog, even if T is Animal. It's impossible to assign a Dog to NonDog<Animal>.

type Cat = "cat";
type Dog = "dog";
type Horse = "horse";

type Animal = Cat | Dog | Horse;

type NonDog<T> = T extends Dog ? never : T;

const dog: Dog = "dog";

const nonDog: NonDog<Animal> = dog;
//    ^^^^^^
// Type '"dog"' is not assignable to type '"cat" | "horse"'. (2322)

Playground Link

Dog | Cat | Horse is not a subset of Dog, but it still contains dogs.

What does that have to do with anything?

Cat | Horse contains no dogs, so you've changed the meaning of the original type by narrowing it.

I haven't. You literally can't assign a Dog to NonDog<Animal>.

Aadit M Shah (@aaditmshah)

Aadit M Shah (@aaditmshah) counterexample:
Open in Playground

type Cat = { cat: true };
type Dog = { dog: true };
type Horse = { horse: true };

type Animal = Cat | Dog | Horse;

type NonDog<T> = T extends Dog ? never : T;

const dog = { dog: true, horse: true } satisfies Animal & Dog;

const nonDog: NonDog<Animal> = dog;

somebody1234

somebody1234 Your counterexample has errors.

type Cat = { cat: true };
type Dog = { dog: true };
type Horse = { horse: true };

type Animal = Cat | Dog | Horse;

type NonDog<T> = T extends Dog ? never : T;

const dog: Dog = { dog: true, horse: true };
//                            ^^^^^
// Object literal may only specify known properties, and 'horse' does not exist in type 'Dog'. (2353)

const nonDog: NonDog<Animal> = dog;
//    ^^^^^^
// Type 'Dog' is not assignable to type 'Cat | Horse'.(2322)

Playground link

Listen, as much as I love to argue with random strangers on the internet, I'm going to have to withdraw from this conversation now. It's pointless and unhealthy. Feel free to keep commenting, but I'm not going to reply. In fact, I'm unsubscribing from this thread. I already closed this issue because it's a duplicate of #4196. Have a great day folks.

Aadit M Shah (@aaditmshah)

Aadit M Shah (@aaditmshah) it doesn't have errors, you modified the code so that it produced an error

hmm... i guess the idea doesn't quite check out
my bad.

Aadit M Shah (@aaditmshah)

Aadit M Shah (@aaditmshah) Here is a proper incorrect case:
Open in Playground

type Cat = { animal: true; cat: true };
type Dog = { animal: true; dog: true };
type Horse = { animal: true; horse: true };

type Animal = { animal: true };

type NonDog<T> = T extends Dog ? never : T;

const dog: Dog = { animal: true, dog: true };
const animal: Animal = dog;
const nonDog: NonDog<Animal> = animal;

For arbitrary T and U, "T is not a subset of U" does not imply "T is a set which contains no elements fromU". T & !U means the latter.

Navigation Menu

Repository navigation

Intersection of conditional types, acting on a generic type, with another type doesn't narrow the generic type #57246

🔎 Search Terms

🕗 Version & Regression Information

⏯ Playground Link

💻 Code

🙁 Actual behavior

🙂 Expected behavior

Additional information about the issue

11 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Intersection of conditional types, acting on a generic type, with another type doesn't narrow the generic type #57246

Description

🔎 Search Terms

🕗 Version & Regression Information

⏯ Playground Link

💻 Code

🙁 Actual behavior

🙂 Expected behavior

Additional information about the issue

Activity

MartinJohns commented on Feb 1, 2024

fatcerberus commented on Feb 1, 2024

Footnotes

aaditmshah commented on Feb 1, 2024

fatcerberus commented on Feb 1, 2024

aaditmshah commented on Feb 1, 2024

RyanCavanaugh commented on Feb 1, 2024

fatcerberus commented on Feb 1, 2024

fatcerberus commented on Feb 1, 2024

aaditmshah commented on Feb 2, 2024

aaditmshah commented on Feb 2, 2024

fatcerberus commented on Feb 2, 2024

RyanCavanaugh commented on Feb 2, 2024

aaditmshah commented on Feb 3, 2024

aaditmshah commented on Feb 3, 2024

11 remaining items

fatcerberus commented on Feb 5, 2024

aaditmshah commented on Feb 5, 2024

fatcerberus commented on Feb 5, 2024

aaditmshah commented on Feb 5, 2024

aaditmshah commented on Feb 5, 2024

fatcerberus commented on Feb 5, 2024

aaditmshah commented on Feb 5, 2024

somebody1234 commented on Feb 5, 2024

aaditmshah commented on Feb 5, 2024

aaditmshah commented on Feb 5, 2024

somebody1234 commented on Feb 5, 2024

somebody1234 commented on Feb 5, 2024

somebody1234 commented on Feb 5, 2024

fatcerberus commented on Feb 5, 2024

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions