typescript - 为什么永远不能分配给每种类型？

Question

typescript 文档说

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

但没有提到为什么。

直觉上，我希望这样的代码会失败:

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

但没有错误，因为任何 never value 被视为有效字符串。

这是故意的吗？如果是，那为什么？ :)

Answer 1

TypeScript 调用的类型 never在类型理论中被称为 bottom type ，有时用符号“⊥”表示。这个想法是它是(唯一的)类型，没有该类型的值。您应该never发现自己持有该类型的值，因为它没有值。如果您将类型视为可能值的集合，那么它是 empty set (符号“∅”)。

这对你来说可能都是有意义的。

TypeScript 也有 subtyping 的概念.就像集合一样，类型可以通过包含一些相同的值来重叠。如果 A 类型的每个值也是 B 类型的值，然后 A是 B 的子类型.你也可以说A扩展 B ，或象征性地，A <: B .在 typescript 中，{a: string}是 object 的子类型，因为类型为 {a: string} 的每个值(例如，值 {a: "hello"} )也是类型 object 的值.

TypeScript 的可赋值性规则基本与 substitutability 有关.如果变量的类型为 B , 和 A <: B ，然后您可以分配类型 A 的值到该变量，因为类型为 A 的每个值也是 B 类型的值.您不一定可以反过来，分配类型为 B 的值。到 A 类型的变量.除非 B <: A , 有一些类型为 B 的值不是 A 类型的值.

从类型作为值集的角度来看，A <: B就像说 A 类型的值集是 subset B 类型的值集,(符号 A ⊆ B)。

这可能(我希望)对您也很有意义。

我们还需要一件事:逻辑 principle of explosion .如果你从一个错误的陈述开始，那么你可以从中证明任何事情。所以，假设“月亮是奶酪做的”是假的，那么“如果月亮是奶酪做的，那么今天是星期三”是真的。此外，“如果月亮是由奶酪制成的，那么今天不是星期三”是真的。将错误的事情视为真实会产生可怕的后果:一切都会爆炸。 💥 这可能令人惊讶，但这是条件语句与其 contrapositive 等价的直接结果.您可能对“如果今天不是星期三，那么月亮不是由奶酪制成”和“如果今天是星期三那么月亮不是由奶酪制成”这两个句子感到满意，或者它们组合成“月亮不是由奶酪制成”不管今天是哪一天，都吃奶酪”。

如果你不接受爆炸原理(而且很多数学家和逻辑学家也有同样的感觉)，那么接下来的内容可能对你来说不合口味。但至少要意识到爆炸原理与 TypeScript 中使用的形式逻辑和类型理论是一致的。它具有有用的后果，弥补了它的怪异。

现在让我们把所有这些放在一起。让我们选择一个类型 T随机问一个问题:是never <: T ?这相当于问题“是否每个 never 类型的值也是 T 类型的值？”或者，以下陈述是否适用于所有值 x :“如果 x 是 never 类型的值，那么它也是 T 类型的值“？根据 never 的定义，我们知道“x 是类型 never 的值”必须始终为假。并且根据爆炸原理，“如果 x 是 never 类型的值，那么 x 是 T 类型的值”必须始终为真。因此，never <: T对任何 T 都是如此.即使你有两种类型 X和 Y ，它们完全互补并且不包含共同的值，never <: X和 never <: Y都是真的。

在集合论术语中，它基本上是说空集是每个集合的子集。即，∅ ⊆ T对于任何 T .这在集合论中是一个完全没有争议的陈述，但可能会给你同样的错误感。在任何情况下，你都不会找到一个空集合的元素，它也不是集合的元素 T .

所以类型为 never 的值总是可以分配给任何其他类型的任何变量。幸运的是，实际上，在运行时，您不会有任何类型为 never 的值。 .但是 TypeScript 允许赋值，因为它是类型安全的并且有一些有用的结果。

请注意，您不能反过来说。 T <: never不是真的，除非 T是 never本身。类型为 string 的值不能分配给 never 类型的变量, 因为没有 string值也是 never值(value)。无所不能的可分配性规则仅适用于一个方向。

好的，我希望这是有道理的。我想继续说 top type类型理论及其最近包含在 TypeScript 中的 unknown ，以及它如何补充 never ，但如果我这样做，这个答案将成为教科书。所以我现在就停下来。

希望能帮到你。祝你好运!