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

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

#4196

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.

@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;

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.

@somebody1234 Other languages don’t have conditional types like TypeScript does. So, no that analogy doesn’t apply.

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.

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.

That’s what is wrong, and that’s what I want to change.

I’m really not sure how you can see

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

and interpret that as anything other than

typefun NonFunction(T: Type) {
    if (T assignsto Function)
        return never;
    else
        return T;
}

because that’s exactly what that type means. It’s literally an identity function if you pass it anything that’s not currently assignable to Function. The fact that you intersect the resulting type with Function afterwards is irrelevant.

It can’t be narrowed down to this type, because types like !string don’t exist. This would require negated types to be supported first (issue linked earlier).

This is precisely what I wrote in my original post.

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

In fact, if we had negation types then as you pointed out we could simply define NonFunction<A> as A & !Function. Hence, we should have a discussion about negation types. To that end, I’ll close this issue and mark it as a duplicate of #4196.

Anyway, now that we agree on something, could you at least tell me what are your thoughts on narrowing in the false branch of conditional types if negated types were added to TypeScript?

Based on the types support currently existing this is working as intended / not a defect. Undesirable? Sure. But not a bug.

Logically, it is a defect. You wouldn’t expect the true branch of the following if statement to be evaluated right?

const conditionA = true;
const conditionB = true;

if (conditionA && !conditionB) {
  console.log(`
    You wouldn't expect this log to be printed
    because conditionB is not false. Hence, if
    this log's printed that means that there's
    a defect in the JavaScript runtime. In the
    same way NonFunction<A> should evaluate to
    A & !Function. If it evaluated to simply A
    then it should be regarded a major defect.
  `);
}

After this discussion, I’m convinced that not having negation types in TypeScript is indeed a defect. It’s like a baby born without hearing. Deafness is certainly a defect. Similarly, not having negation types in TypeScript is also a defect.

Anyway, I’m closing this issue as a duplicate of #4196.

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>.

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.

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.