底層類型

在類型理論（數理邏輯中的一種理論）中，類型系統的底層類型是所有其他類型的子類型。

在存在這種類型的情況下，它通常用上粘（⊥）符號表示。當底層類型為空時，一個返回類型為底層的函數不能返回任何值，甚至不能返回一個單元類型的唯 一值。

因此，在這樣的語言中，底層類型可以被稱為零或永不類型。在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類型被引入作為底層類型。