底部类型是什么？

Question

在维基百科中，底部类型被简单地定义为“没有值的类型”。然而，如果 b 是这种空类型，那么乘积类型 (b,b) 也没有值，但似乎与 b 不同。我认为底部是不可居住的，但我认为这个属性不足以定义它。

通过Curry-Howard对应，底部与数学谬误相关联。现在有一个逻辑原则，即从 False 推导出任何命题。根据Curry-Howard，这意味着类型 forall a. bottom -> a 是可居住的，即存在一族函数 f :: forall a. bottom -> a。

那些函数 f 是什么？它们是否有助于定义底部，可能作为所有类型 forall a. a 的无限积？

- V. Semeria

Answer 1

在数学中

底部是一种没有值的类型。也就是说：任何空类型都可以扮演底部角色。

那些 f :: forall a . Bottom -> a 函数是空函数。在函数的集合论定义中称为“空函数”。

在编程中

通过编程语言基础库将具体的空类型指定为底部，是为了方便起见。每个人都使用相同的空类型作为底部，从而提高代码的可读性和兼容性。

在 Haskell 中

让我们用更友好的名称 "Bottom" -> "Void"，"f" -> "absurd" 来引用它们。

{-# LANGUAGE EmptyDataDecls #-}
data Void

这个定义没有包含任何构造函数，因此无法创建它的实例，也就是空的。

absurd :: Bottom -> a
absurd = \ case {}

在case表达式中，我们不需要处理任何情况，因为没有情况需要处理。

它们已经在base包中定义。

- libeako

---

我在命题演算中看到了三种公式。1）永真式，在Heyting代数的每个解释中都为真。2）其否定是永真式的公式，在每个Heyting解释中都为假。3）值取决于解释的公式。根据Curry-Howard，情况2和3都对应于空类型。然而，我认为情况2应该在空类型中被孤立出来：只有那些类型才应该被称为底部。 - V. Semeria