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

[aaditmshah]

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

[MartinJohns]

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

#4196

[fatcerberus]

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

Footnotes

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

[aaditmshah]

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

[fatcerberus]

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

All functions are objects in JavaScript.

[aaditmshah]

@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

[RyanCavanaugh]

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.

[fatcerberus]

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.

[fatcerberus]

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.

[aaditmshah]

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.

[aaditmshah]

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

[fatcerberus]

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

[RyanCavanaugh]

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.

[aaditmshah]

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.

1. 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?
2. 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.

[aaditmshah]

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)"?