我注意到有关Voidhaskell Data.Void模块中的类型的一件事,这很奇怪,我非常想知道为什么它是这样的.未定义应该是一个存在于每种类型的值(在我的理解中),和
undefined :: Type
Run Code Online (Sandbox Code Playgroud)
应该屈服
*** Exception: Prelude.undefined
Run Code Online (Sandbox Code Playgroud)
它适用于我尝试的每种数据类型,除了Void.
undefined :: Void根本没有终止,相同absurd undefined.现在我认为这不是一个问题,因为它Void代表了一种不会发生的价值,但我仍然想知道导致这种行为的原因.
经过一番调查后,我想我明白了这是怎么发生的,以及它如何取决于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
Run Code Online (Sandbox Code Playgroud)
请注意,Show实例委托给absurd,这解释了为什么undefined :: VoidGHCi给出的结果相同absurd undefined.
现在看一下它的定义absurd a,它用于seq"确保" a实际评估,所以你会认为应该触发undefined异常.然而,巧妙地seq实际上并没有这样做.a `seq` b只保证既 a和b整个表达式返回之前将被评估,但不以何种顺序.完全由实现的选择决定哪个部分首先被评估.
这意味着GHC可以自由地评估第a一个,触发异常; 或者spin a首先评估.如果它spin a首先计算,那么你得到一个无限循环,因为Void构造函数是一个newtype构造函数,并且通过设计,展开它们实际上并不评估任何东西.
因此,通过语义seq,两个选项实际上是同等合法的Haskell行为.
作为最后一点,GHC中的异常语义被定义为明确的非确定性:如果表达式可以以几种不同的方式给出底部,GHC可以选择其中任何一种.由于区分不同底部的唯一方法是IO,这被认为是可接受的.