什么是底层类型？

Question

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

通过Curry-Howard correspondence，底部与数学错误相关联。现在有一个逻辑原则表明从 False 遵循任何命题。对于 Curry-Howard，这意味着 forall a. bottom -> a 类型是有生命的，即存在一系列函数 f :: forall a. bottom -> a。

f 这些函数是什么？它们是否有助于定义底部，也许是所有类型的无限乘积forall a. a？

Answer 1

在数学中

Bottom 是没有价值的一种类型。即：任何空类型都可以起到底层的作用。

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

在编程中

为了方便起见，将一个具体的空类型专用于编程语言库的底部。代码的可读性和兼容性受益于使用与底部相同的空类型的每个人。

在 Haskell 中

让我们用更友好的名称来称呼它们“Bottom” -> “Void”、“f” -> “absurd”。

{-# LANGUAGE EmptyDataDecls #-}
data Void

此定义不包含任何构造函数 => 无法创建它的实例 => 它是空的。

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

在case表达式中，我们不必处理任何case，因为没有。

他们已经是defined in package base