Data.Void.absurd与⊥有什么不同？

Question

今天早些时候我看到了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 NEWTYPE包装，并且永远不会返回，即使你能找到一个Void传递给它。这将是难以区分的实现将是这样的：

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

鉴于此，为什么我们说absurd是一个值得生活在Data.Void正常功能，但

drusba :: a -> Void 
drusba = undefined 

是函数不可能被定义？是否像下面这样？

absurd是一个总的功能，得到的非底结果为在其（空）域的任何输入，而drusba是局部的，从而底部结果对于一些（实际上所有）在其领域的输入。

Answer 1

Data.Void从void包改为base的基版4.8（GHC 7.10）。如果您查看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取代单严格的构造函数的数据类型：

newtype Void = Void Void 

这始终是合法的。然而，由于data和newtype之间的不同模式匹配语义，因此spin的定义已改变含义。为了保持精确，spin也许应该已被写入

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

（避免spin !(Void x)裙子在NEWTYPE构造函数和爆炸模式之间的相互作用现在已经修正了的意思;但对于GHC 7.10（公顷）此表没有按！实际上产生期望的错误消息，因为它被“优化”成一个无限循环）在这一点上absurd = spin。谢天谢地，它最终并不重要，因为整个旧的定义有点愚蠢。

Answer 2

由于历史原因，任何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这样的空类型时是惯用的。