什么是底部类型？

Question

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

通过库里 - 霍华德的对应,底部与数学虚假相关联.现在有一个逻辑原则说明从False跟随任何命题.通过库里 - 霍华德,这意味着这种类型forall a. bottom -> a是有人居住的,即存在一系列功能f :: forall a. bottom -> a.

那些功能是f什么？它们是否有助于定义底部,可能是所有类型的无限产品forall a. a？

Answer 1

在数学中

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

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

在编程中

编程语言基础库指定一个具体的空类型作为底层是为了方便。代码的可读性和兼容性受益于每个人都使用相同的空类型作为底部。

在哈斯克尔

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

{-# LANGUAGE EmptyDataDecls #-}
data Void

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

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

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