keyof never should be never

[AnyhowStep]

TypeScript Version: 3.5.1

Search Terms:

keyof never

Code

//Expected: type k = never
//Actual  : type k = string | number | symbol
type k = keyof never

Expected behavior:

keyof never should be never

Actual behavior:

keyof never is string|number|symbol

Intuitively, to me, if no values inhabit never, then the set of keys is the empty set (also never).

Playground Link:

Playground

Related Issues:

Searching "keyof never" brought up 400+ total results, so...

[dragomirtitian]

Should it though ? never is the subtype of all types. You can never create a value of this type that is true. But as the sub-type of all types i would expect it to be index-able by any value that can be an index. This is also supported by value-space behavior:

declare let o: never;
let v1 = o[""]
let v2 = o[1]
let v3 = o[Symbol()]

play

[AnyhowStep]

{ x : any } is a subtype of all types { [k:string]:T}

I wouldn't expect { x : any }[""] to work, though

[RyanCavanaugh]

It some sense, it doesn't matter. string | number | symbol is a correct upper bound on all keys, though, so it's a sensical result. I don't see value in breaking any odd dependencies on the behavior either way.

[jcalz]

If one reasons that keyof (A & B) should always equal keyof A | keyof B, then keyof never needs to be an upper bound on keys, such as string | number | symbol.

[RyanCavanaugh]

@jcalz great point. The dual of that would actually be more important -- if keyof (A | B) is (keyof A) & (keyof B), then setting keyof never === never would break never being the identity operand of union because keyof (A | B | never) would incorrectly be never.

[AnyhowStep]

string | number | symbol is a correct upper bound on all keys

It's a correct upper bound on keyof {x:any}, too.
But the result of that is "x" and not string | number | symbol =P

---

If we take it as an axiom that keyof (A | B) should always equal (keyof A) & (keyof B), then I guess you're right that keyof never === string | number | symbol logically follows.

But why not apply union simplification first?

So keyof (A | never) is just keyof A

You would still get results consistent with current behaviour but keyof never === never.

---

For keyof (A & B) if the intersection is never, shouldn't the result be keyof never and not (keyof A) | (keyof B)?

So, perform intersection simplification to get keyof never and get never.

You would still get results consistent with current behaviour but keyof never === never.

---

I'm not invested in changing the behavior of keyof never, I suppose. I'm just musing about the current behaviour and how there's a different behavior that could still be consistent

---

But I guess there's also keyof unknown which is never at the moment (which I agree makes sense).

And keyof unknown is the dual of keyof never

[AnyhowStep]

I guess it's that vacuous truth thing.

keyof A := { k : ∀x (x ∈ A → k is property of x) } (optional properties count as properties, too)

When A is never, we have a vacuous truth,

∀x (¬x ∈ never)
-----
∴ ∀x (x ∈ never → k is property of x)

So, all keys k are keys of never.

---

Whereas for unknown, there's always a counterexample for every k.

---

Okay, it all makes sense to me now. Thanks for the replies!

[fatcerberus]

Yep, contravariance (w.r.t. keyof) + principle of explosion. never can act as any other type (Haskell's absurd, e.g., is based on this concept)--or rather, we can pretend it does because you can't soundly obtain such a value. Therefore it gets the widest possible key.

It is a bit odd though in that you can't actually index a never. That's probably where the confusion came in.

[weswigham]

FYI, for anyone reading: #30753 for context - back after we introduced keyof, keyof never was never - this caused a bunch of issues (it's internally inconsistent, the result does matter, and it matters quite a bit), so we fixed it back in April.

The current behavior of keyof at its bounds is certainly more correct - you can convince yourself as such with a simple inductive argument:

Suppose I have an object, {}. We know keyof an object type is supposed to return the keys of said object, so keyof {} is never. never theoretically implements every conceivable function or property, but, as a set of allowable values, is empty (therefore, is the result when an object has no keys). Now suppose we add a property to our input object, {x}, and we look at keyof {x}. Out input has become more specific - the set of allowed values is smaller. Conversely, the result of keyof is now "x". So our set of output values is now larger - this inverse relationship continues as you add more and more properties to a type - {x,y} is a smaller set of values than {x}, while "x" | "y" is larger than just "x". Now, remember what I said earlier - never conceptually implements all properties - so the logical extreme - the most specific type we can feed into keyof is never (after all, it has no possible values). That, in turn, produces the broadest possible result - string | number | symbol (the union of all possible properties).

[fatcerberus]

Or just the principle of explosion: never (bottom ⊥) has no inhabitants and therefore having a value of this type puts you in a state of contradiction. Therefore we can prove anything from it, including that it has all possible property keys.

[jack-williams]

String Index Signatures

[StreetStrider]

I still don't get the motivation behind this design, but it seemes like a complicated area. I agree that there may be a reason for current behavior.

However, I got specific scenario in mind which lead me here and this is why I think the current behavior is more broken.
playground.

In short, I got Box type with some encapsulated data which is strongly typed. And I got two helper type functions, Box_Data and Box_Keys. I want the second one to be built on top of the first one to reuse code. However, if the first one resolves to never (which is desired), the second one would return key supertype (string | number | symbol), while I need it to be never as well. I need never because later I need to use Box_Keys in some predicate scenario but extends never and extends string | number | symbol got the opposite results. The second one is incorrect, since it says that my empty boxes are supertypes of my filled boxes, which is incorrect.

To fix this I need to replace line 16 with line 17. The difference is only syntax, but it lead to opposite behaviors. To fix this behavior I need to copy-paste logic. The difference is subtle, but it might took some time to track this down in complex codebases.

I expected TF type to be never, logically similar to keyof {}.

[RyanCavanaugh]

This is one way to think of it: keyof is a contravariant operation, so if its input is from the zero-width part of the triangle (never), then the output has to be whatever the largest possible part of the triangle is (string | number | symbol)

[cevr]

@RyanCavanaugh i honestly could never remember nor understand what those words meant until this diagram. offtopic, but thank you for this

[HansBrende]

@AnyhowStep food for thought: your logic would make complete sense if keyof took the union of keys over a union of objects rather than the intersection of keys over a union of objects. And indeed, if you rewrite keyof to implement the former behavior via distributing over the union:

type KeyOf<T> = T extends unknown ? keyof T : never

Then you get the behavior you are expecting:

KeyOf<never> === never