lambda-calculus - 什么是底部类型？

Question

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

由 Curry-Howard correspondence ，底部与数学错误相关。现在有一个逻辑原则表明，任何命题都从“假”开始。根据 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