不必要的类型杂耍定义Data.Void(Hackage上的包"void")？

Question

的空隙包声称提供适合居住型称为Void,其定义如下: -

newtype Void = Void Void

这个定义比使用更简单的东西更好吗？说 -

data Void

如果我的理解是正确的,那么两种数据类型都只包含底值.然而,后者更容易理解.

编辑:好的,所以我理解丹尼尔的答案如下.但是我想到了另一种可能更简单的方法来保持Haskell98兼容.我们可以使用Abstract数据类型,并且不向用户公开构造函数.

module Data.Void (Void) where
  data Void = Void

现在只有Data.Void模块中的代码可以构造一个Void,但是因为我们知道它没有,所以Void数据类型实际上是无人居住的.

会有用吗还是我错过了什么？

Answer 1

来自Hackage上的void包的描述:"一个Haskell 98逻辑上无人居住的数据类型"(我的重点).声明Void为简单data Void需要Haskell 2010或"EmptyDataDecls"语言扩展,因此不会是"Haskell 98".

编辑

这是 Haskell Wiki上的一个页面,它描述了这种情况.

@AnupamJain这不简单甚至不正确.存在空包的唯一原因是具有底部作为唯一可能的居民的类型.无法导出构造函数并不意味着构造函数不存在.新型配方证明只有底部可以居住在这种类型.例如,这对于在模块类型检查中制作荒谬函数很重要. (2认同)

Answer 2

您的实现仍然不完整,因为您没有荒谬的功能:

absurd :: Void -> a

Void应该是Haskell中的初始对象,这就是你需要荒谬函数的原因.我发现void包中的absurd实现非常优雅和恰当:

absurd (Void a) = absurd a

这个定义让人联想到虚空与虚假前提的逻辑类比,从中可以推导出任何结论.它甚至使用引用自身的逻辑谬误来证明自己,这在逻辑上是荒谬的.