Why is never assignable to every type?

Question

The TypeScript documentation says that

The never type is a subtype of, and assignable to, every type

but doesn't mention why.

Intuitively, I would expect code like this to fail:

const useString = (str: string) => console.log('This is definitely a string:', str)
const useNever = (not_a_string: never) => useString(not_a_string)

but there are no errors, because any never value is considered a valid string.

Is this intentional? If yes, then why? :)

Answer 1

The type that TypeScript calls never is what's known in type theory as a bottom type, sometimes referred to with the symbol "⊥". The idea is that it is the (unique) type for which there are no values of that type. You should never find yourself holding a value of that type because it has no values. If you think of types as sets of possible values, then it is the empty set (symbol "∅").

This probably all makes sense to you.

TypeScript also has the notion of subtyping. Just like sets, types can overlap by containing some of the same values. If every value of type A is also a value of type B, then A is a subtype of B. You can also say that A extends B, or symbolically, A <: B. In TypeScript, {a: string} is a subtype of object, because every value of type {a: string} (for example, the value {a: "hello"}) is also a value of type object.

TypeScript's assignability rules are basically related to substitutability. If a variable is of type B, and A <: B, then you can assign a value of type A to that variable, because every value of type A is also a value of type B. You can't necessarily do the reverse, assigning a value of type B to a variable of type A. Unless B <: A, there are some values of type B which are not values of type A.

From the types-as-sets-of-values point of view, A <: B is like saying the set of values of type A is a subset of the set of values of type B, (symbols A ⊆ B).

This probably (I hope) all makes sense to you too.

One more thing we need: the logical principle of explosion. If you start with a statement that is false, then you can prove anything at all from it. So, assuming "the moon is made of cheese" is false, then "If the moon is made of cheese, then today is Wednesday" is true. Also, "if the moon is made of cheese, then today is not Wednesday" is true. There are dire consequences for taking something false to be true: everything explodes. This might be surprising, but is a direct consequence of the equivalence of a conditional statement with its contrapositive. You're probably happy with the sentences "If today is not Wednesday then the moon is not made of cheese" and "If today is Wednesday then the moon is not made of cheese", or their combination into "The moon isn't made of cheese no matter what day it is today".

If you don't accept the principle of explosion (and plenty of mathematicians and logicians have felt the same way) then what follows might not be palatable to you. But at least realize that the principle of explosion is consistent with formal logic and the type theory used in TypeScript. And it has useful consequences which make up for its weirdness.

Now let's put all that together. Let's pick a type T at random, and ask the question: Is never <: T? That is equivalent to the question "is every value of type never also a value of type T?" Or, is the following statement true for all values x: "if x is a value of type never, then it is also a value of type T"? By the definition of never, we know that "x is a value of type never" must always be false. And by the principle of explosion, the statement "if x is a value of type never, then x is a value of type T" must always be true. And therefore, never <: T is true for any T. Even if you have two types X and Y, which are exactly complementary and contain no values in common, never <: X and never <: Y are both true.

In set theory terms, it's basically saying that the empty set is a subset of every set. That is, ∅ ⊆ T for any T. That's a completely non-controversial statement in set theory, but might give you the same sense of wrongness. In any case you'll never find an element of the empty set which isn't also an element of the set T.

So a value of type never can always be assigned to any variable of any other type. Luckily, in practice, at runtime, you won't have any values of the type never. But TypeScript allows the assignment because it is type safe and has some useful consequences.

Note that you can't say the reverse. T <: never is not true unless T is never itself. A value of type string can't be assigned to a variable of type never, since no string value is also a never value. The anything-goes assignability rule is in only one direction.

Okay, I hope that makes sense. I want to go on and on about the top type in type theory and its recent inclusion in TypeScript as unknown, and how it is complentary to never, but this answer will be a textbook if I do that. So I will stop now.

Answer 2

You are not calling the useNever function. If you try to call it with a parameter it will fail since a value can not be never. But as always, you can trick the compiler with typeguards e.g. this will work

const test = (val: string | number) => {
     if (typeof val === "string") {

     } else if (typeof val === "number") {

     } else {
         useNever(val); // works, since val is not number or string it is implicitly never
     }
 }

Answer 3

jcalz's answer was bizarre.

My thinking is that types are bit flags, e.g. 0001, 0010, 0100, 1000.

And unions are combinations of those flags e.g. 1101, which is the result of 0001 | 0100 | 1000. | is bitwise OR.

I identify whether a type such as 0001 is in 1101, we can do bitwise AND then compare: 0001 & 1101 -> 0001. 0001 === 0001 -> true.

If you apply this formula with never, which is the absense of a type, that is 0000, you get 0000 & 1101 -> 0000, 0000 = 0000 -> true.

So based on this simple logic, never is contained within all types. Another way of thinking about it is that typescript is testing with the target type contains the given type. If the given type is 0000, it cannot fail this test, because it has no active bits that can fail.

Why that behaviour isn't overruled with a special rule though, I do not know.

Answer 4

How type-checking works for assignments?

Take the R-value (right side of assignment). Verify if it can assume a value which the L-value (left side of assignment) can not. If any such value exists, then reject the assignment. Otherwise, it's fine.

Let's see examples:

let x: number;
let y: never;

x = y; // OKAY, can assign any given `never` value to a number

y = x; // Not OKAY, x can be, among other values, 1, which is can not be assigned to never

It looks absurb, as an assignment needs to move some data into the designated storage for a given variable, and no value exists, since it's not a runtime type. In practice though, an assignment from never to any other type, while valid, won't actually run (except if you trick TypeScript with type assertions).

Does that make sense?