Haskell Data.Void : undefined turns into infinite loop

Question

我注意到关于 Void 的一件事输入haskell Data.Void模块，这很奇怪，我非常想知道为什么会这样。
Undefined 应该是每个类型都存在的值(在我的理解中)，并且

undefined :: Type

应该产生

*** Exception: Prelude.undefined

它适用于我尝试过的每种数据类型， Void 除外. undefined :: Void根本不终止， absurd undefined 相同.
现在我认为这不是什么大问题，因为 Void表示无论如何都不会发生的值，但我仍然想知道是什么导致了这种行为。

Answer 1

经过更多调查，我想我理解这是如何发生的，以及它如何取决于 GHC 的优化选择。在 void-0.7 ，我们有以下相关定义:

newtype Void = Void Void

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

instance Show Void where
  showsPrec _ = absurd

请注意 Show实例委托(delegate)给 absurd ，这就解释了为什么 undefined :: Void在 GHCi 中给出与 absurd undefined 相同的结果.

现在查看 absurd a 的定义, 它使用 seq “确保” a实际被评估，所以你会认为应该触发 undefined异常(exception)。然而，巧妙地 seq实际上并不是这样工作的。 a `seq` b只保证 a和 b将在整个表达式返回之前进行评估，但不按顺序进行评估。首先评估哪个部分完全取决于实现的选择。

这意味着 GHC可以自由评估 a首先，触发异常；否则评估 spin a第一的。如果它评估 spin a首先，你会得到一个无限循环，因为 Void构造函数是 newtype构造函数，并且通过设计，打开它们实际上并不评估任何东西。

因此，根据 seq 的语义，这两个选项实际上都是同样合法的 Haskell 行为。

最后一点， exception semantics in GHC已被定义为明确的非确定性:如果一个表达式可以以几种不同的方式给出底部，GHC 可以选择其中任何一种。因为区分不同底部的唯一方法是在 IO ，这被认为是可以接受的。