Typescript: `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_