如何做左空洞？

Question

我试图理解https://hackage.haskell.org/package/base-4.14.0.0/docs/Data-Void.html，并具有以下示例：

let x :: Either Void Int; x = Left Void

代码未编译。如何使其运行？

Answer 1

Void类型的要点是它没有居民（除了“底”值，例如异常和无限循环）。您可以写

x, y, z :: Either Void Int
x = undefined
y = Left $ error "Whoops"
z = Left $ let q = q in q

但是所有这些都违反了Void的基本概念。

Either Void Int类型的唯一“合法”值的格式为Right i，其中i :: Int。

实际上，您可以编写以下内容：

unEither :: Either Void a -> a
unEither (Left v) = absurd v
unEither (Right a) = a

Answer 2

由于不可能创建Void类型的值，因此Either Void Int类型的每个值都必须具有Right构造函数（或者在其Left构造函数的底部，这不是很有用）。例如Right 1将是此类型的有效值。