使用 Void 的实际例子

Question

编辑：Void，我的意思是 Haskell 的 Void 类型，即不能有值但 undefined.

的空类型

关于是否用实际的 Void 类型替换 noreturn 函数属性的 Swift Evolution 正在进行讨论。为此，我们必须确保这将为平台带来真正的好处。使用 Void 作为 return 类型是不够的。

所以我请您提供非常实用的示例，其中Void的使用增加了代码的清晰度、简洁性和通用性。也许它将使用类（在 Haskell 意义上），也许是泛型，也许它将在 ADT 中包含 Void。

但是请，不要深入研究 HKT、Monads 以及所有那些高级的东西。来自标准库的效用函数也是一个不好的例子。一个完美的例子是街机游戏或类似游戏的一部分。

Answer 1

(说到 Void 是没有值的类型，这与只有一个值的类型不同, 通常称为单位。)

在 Haskell 流式库中，如 streaming or pipes，有表示 "a source of values of type a that, once exhausted, returns a value of type r" 的数据类型。像 Producer a m r 之类的东西（m 是一个基础 monad，但这与这里无关。）

让生产者 return 具有一个值（其类型与它们在运行时发出的值的类型无关）实际上非常有用。例如，您可以将 "streaming splitter" 定义为类型为：

的函数

streamingSplit :: Producer a m r -> Producer a m (Producer a m r)

此函数对生产者进行分段，而无需在内存中累积拆分前的所有元素。

现在，如果我们想在类型级别表达生产者永不停止生产东西怎么办？我们可以使它 return 成为 Void 类型的值，例如 Producer a m Void.

另一个可能的用例。假设您有一个高阶函数，它接受一个可能会失败的回调。类似于：

-- does something with the wrapped callback, maybe emit a log message or whatever
takesACallback :: (a -> IO (Either e r)) -> a -> IO (Either e r)

如果我们想为函数 a -> IO r 定义 永不失败 的 takesACallback 版本怎么办？进出 Either 很麻烦，并且在获取值时会产生虚假的模式匹配。

使用Void我们可以从将a -> IO r变成a -> IO (Either Void r)开始，将它传递给takesACallback，然后移除"fake"错误分支在 Either 上使用 absurd :: Void -> a 函数。

takesACallback':: (a -> IO r) -> a -> IO r
takesACallback' callback = fmap (either absurd id) 
                         . takesACallback (fmap Right . callback)

Here 是 Hackage 上这个技巧的一个例子。

使用 Void 的实际例子

Practical examples of using Void

haskell

types

type-systems

curry-howard