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

Question

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

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

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

score 4 · Accepted Answer

在数学

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

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

在编程中

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

在哈斯克尔

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

{-# LANGUAGE EmptyDataDecls #-}
data Void

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

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

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

1 回答 1