Data.Void.absurd 与 ⊥ 有何不同？答案

【问题标题】：How is Data.Void.absurd different from ⊥?Data.Void.absurd 与 ⊥ 有何不同？
【发布时间】：2016-07-24 20:35:10
【问题描述】：

我今天早些时候看到了Inverse of the absurd function，虽然我很清楚drusba :: a -> Void 的任何可能实现永远不会终止（毕竟，不可能构造Void），但我不明白为什么会这样absurd :: Void -> a 不是这样。考虑 GHC 实施：

newtype Void = Void Void

absurd :: Void -> a
absurd a = a `seq` spin a where
   spin (Void b) = spin b

spin，在我看来，正在无休止地解开Void 新类型包装器的无限系列，即使你能找到Void 来传递它，也永远不会返回。无法区分的实现类似于：

absurd :: Void -> a
absurd a = a `seq` undefined

鉴于此，为什么我们说absurd 是一个应该存在于Data.Void 中的适当函数，但是

drusba :: a -> Void
drusba = undefined

是一个不可能被定义的函数吗？是不是像下面这样？

absurd 是一个总函数，对于其（空）域中的任何输入给出非底部结果，而 drusba 是部分函数，对于其域中的某些（实际上是所有）输入给出底部结果。

【问题讨论】：

除此之外，永远不会调用荒谬的函数。它很少需要，但有它的用途。

标签： haskell

【解决方案1】：

由于历史原因，任何 Haskell 数据类型（包括newtype）都必须至少有一个构造函数。

因此，要在“Haskell98”中定义Void，需要依赖类型级递归newtype Void = Void Void。这种类型没有（非底部）值。

absurd 函数必须依赖（值级别）递归来处理 Void 类型的“怪异”形式。

在更现代的 Haskell 中，通过一些 GHC 扩展，我们可以定义零构造函数数据类型，这将导致更合理的定义。

{-# LANGUAGE EmptyDataDecls, EmptyCase #-}
data Void
absurd :: Void -> a
absurd x = case x of { }    -- empty case

这个案例很详尽——它确实处理了Void 的所有构造函数，它们都为零。因此它是全部的。

在其他一些函数式语言中，如 Agda 或 Coq，上述情况的变体在处理像 Void 这样的空类型时是惯用的。

【讨论】：

我们现在确实这样做了；看我的回答。
data Void : Set where MkVoid : Void → Void 在 Agda 中是一个完全有效的定义。 Coq 中的 Inductive Void : Type := MkVoid : Void -> Void. 也是如此。并且可以定义对应的absurd函数就好了。
EmptyDataDecls 是 Haskell 2010 的一部分。遗憾的是，EmptyCase 不是。

【解决方案2】：

Data.Void 从void 包移动到基本版本4.8 (GHC 7.10) 中的base。如果您查看 void 的 Cabal 文件，您会发现它仅包含旧 base 版本的 Data.Void。 Now, Void is defined as chi suggests:

data Void

absurd :: Void -> a
absurd a = case a of {}

这是完全有效的。

我认为旧定义背后的想法是这样的：

考虑类型

data BadVoid = BadVoid BadVoid

这种类型无法完成工作，因为实际上可以使用该类型定义一个非底部（共归纳）值：

badVoid = BadVoid badVoid

我们可以通过使用严格注解来解决这个问题，这会强制类型为归纳：

data Void = Void !Void

在实际上可能成立或不成立但至少在道德上成立的假设下，我们可以合法地对任何归纳类型进行归纳。所以

spin (Void x) = spin x

如果假设我们有 Void 类型的东西，则总是会终止。

最后一步是用新类型替换单严格构造函数数据类型：

newtype Void = Void Void

这也是合法的；不可能构造这个Void 类型的非底部值。这样做的好处是它有时可以让 GHC 将一小段代码识别为死代码。但这并不是一个很大的优势，而且会带来一些不幸的并发症。由于data 和newtype 之间的模式匹配语义不同，spin 的定义已经改变了含义。为了准确地保留含义，spin 可能应该写成

spin !x = case x of Void x' -> spin x'

（避免spin !(Void x) 绕过新类型构造函数和 bang 模式之间的交互中现已修复的错误；但对于 GHC 7.10（哈哈！），此表单实际上不会产生所需的错误消息，因为它已“优化”成一个无限循环）此时absurd = spin。

谢天谢地，这实际上并不重要，因为整个旧定义有点愚蠢。

【讨论】：