底层类型

在类型理论（数理逻辑中的一种理论）中，类型系统的底层类型是所有其他类型的子类型。

在存在这种类型的情况下，它通常用上粘（⊥）符号表示。当底层类型为空时，一个返回类型为底层的函数不能返回任何值，甚至不能返回一个单元类型的唯 一值。

因此，在这样的语言中，底层类型可以被称为零或永不类型。在Curry-Howard对应关系中，空类型对应于虚假性。

在子类型系统中，底层类型是所有类型的一个子类型。它是顶层类型的对偶，顶层类型横跨系统中所有可能的值。

如果一个类型系统是健全的，那么底层类型是无人居住的，底层类型的术语代表了逻辑上的矛盾。

在这样的系统中，通常不对底层类型和空层类型进行区分，这些术语可以互换使用。如果底层类型是有人居住的，它的术语[s]通常对应于错误条件，如未定义行为、无限递归或不可恢复的错误。

在《有底的有界量化》中，皮尔斯说，Bot有很多用途。在一个有异常的语言中，提高结构的自然类型是提高∈异常->Bot，对于其他控制结构也是如此。

直观地说，Bot在这里是不返回答案的计算的类型。Bot在多态数据结构的叶子节点的类型化中很有用。例如，List(Bot)是nil的一个很好的类型。Bot是Java等语言的空指针值（一个不指向任何对象的指针）的自然类型：在Java中，null类型是引用类型的通用子类型，null是null类型的xxx值；并且它可以被转换为任何引用类型。然而，null类型不是上述的底层类型，它不是int和其他原始类型的子类型。

一个包括Top和Bot的类型系统似乎是类型推理的自然目标，允许用一对边界来捕获被遗漏的类型参数的约束：我们写S<:X<:T意味着X的值必须位于S和T之间。在这样的方案中，一个完全没有约束的参数下面是Bot，上面是Top。

在编程语言中，大多数常用的语言没有办法表示底部类型。有几个值得注意的例外。在Haskell中，用错误构造函数创建的未定义常量或术语可以被赋予任何类型。

试图评估这样的表达式会导致代码不可恢复地中止。在CommonLisp中，NIL类型不包含任何值，是每个类型的一个子类型。名为NIL的类型有时会与名为NULL的类型相混淆，后者有一个值，即符号NIL本身。

在Scala中，底层类型被表示为Nothing。

除了用于只是抛出异常或其他不正常返回的函数外，它还用于共变参数化的类型。例如，Scala的List是一个共变类型构造器，所以List[Nothing]是List[A]的一个子类型，适用于所有类型的A。所以Scala的Nil，即用于标记任何类型列表结束的对象，属于List[Nothing]类型。在Rust中，底层类型被称为never类型，用！来表示。它出现在保证永不返回的函数的类型签名中，例如通过调用panic!()或永远循环。它也是某些控制流关键字的类型，例如break和return，这些关键字不产生一个值，但仍然可以作为表达式使用。在锡兰，底部类型是Nothing。它与Scala中的Nothing相当，表示所有其他类型的交集以及空集。在带有ClosureCompiler注解的JavaScript中，底层类型是！Null（字面意思是Null单元类型的非空成员）。在Dart中，从2.12版开始，随着null安全的更新，Never类型被引入作为底层类型。