使用Void的实际例子

Ant*_*on3 9 haskell types type-systems curry-howard

编辑:Void我的意思是Haskell的Void类型,即不能有值的空类型undefined.

有关Swift Evolution的讨论是否noreturn要用实际Void类型替换函数属性.要做到这一点,我们必须确保这将为平台带来真正的好处.使用Void返回类型是不够的.

所以我请你提供非常实用的例子,其中使用Void增加了代码的清晰度,简洁性和通用性.也许它会使用类(在Haskell意义上),也许是泛型,也许它将包含Void在ADT中.

但是,不要太过深入HKT,Monads,所有那些高级别的东西.标准库中的实用程序功能也是一个不好的例子.一个完美的例子将是街机游戏的一部分或类似的东西.

dan*_*iaz 16

(说到Void与类型没有值,这是与刚才所述类型不同的一个值,通常被称为单元).

在Haskell流式传输库(如流式传输管道)中,有一些数据类型表示"类型值的来源a,一旦耗尽,就会返回类型值r".类似的东西Producer a m r(这m是一个基础monad,但这里不相关.)

让生成器返回一个值(与运行时它们发出的值类型无关的类型)实际上非常有用.例如,您可以将"流分割器"定义为具有以下类型的函数:

streamingSplit :: Producer a m r -> Producer a m (Producer a m r)
Run Code Online (Sandbox Code Playgroud)

该函数对生成器进行分段,而不必在内存中累积分割前的所有元素.

现在,如果我们想在类型级别表达生产者永远不会停止生产的东西呢?我们可以让它返回类型的值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)
Run Code Online (Sandbox Code Playgroud)

如果我们想要定义一个永不失败的takesACallback函数版本,a -> IO r该怎么办?进入和离开是一个麻烦,并在获得价值时引发虚假的模式匹配.Either

使用Void我们可以先将其a -> IO r转换为a a -> IO (Either Void r),将其传入takesACallback,然后使用该absurd :: Void -> a函数删除Either上的"假"错误分支.

takesACallback':: (a -> IO r) -> a -> IO r
takesACallback' callback = fmap (either absurd id) 
                         . takesACallback (fmap Right . callback) 
Run Code Online (Sandbox Code Playgroud)

以下是Hackage上这个技巧的一个例子.