haskell - Data.Void 中的 absurd 函数有什么用？

Question

absurd Data.Void 中的函数具有以下签名，其中 Void 是该包导出的逻辑上无人居住的类型:

-- | Since 'Void' values logically don't exist, this witnesses the logical
-- reasoning tool of \"ex falso quodlibet\".
absurd :: Void -> a

我确实知道足够的逻辑来获取文档的注释，即通过命题类型对应关系，这对应于有效的公式 ⊥ → a。

我感到困惑和好奇的是:这个函数在什么样的实际编程问题中有用？我认为在某些情况下它可能是有用的，作为一种类型安全的方式来彻底处理“不可能发生”的情况，但我对 Curry-Howard 的实际用途了解不够，无法判断这个想法是否存在完全正确的轨道。

编辑:示例最好在 Haskell 中，但如果有人想使用依赖类型语言，我不会提示......

Answer 1

生活有点艰难，因为 Haskell 并不严格。一般用例是处理不可能的路径。例如

simple :: Either Void a -> a
simple (Left x) = absurd x
simple (Right y) = y

事实证明这有点用处。考虑 Pipes

的简单类型

data Pipe a b r
  = Pure r
  | Await (a -> Pipe a b r)
  | Yield !b (Pipe a b r)

这是 Gabriel Gonzales 的 Pipes 库中标准管道类型的严格简化版本。现在，我们可以将一个永不产生的管道(即消费者)编码为

type Consumer a r = Pipe a Void r

这真的永远不会让步。这意味着消费者的正确折叠规则是

foldConsumer :: (r -> s) -> ((a -> s) -> s) -> Consumer a r -> s
foldConsumer onPure onAwait p 
 = case p of
     Pure x -> onPure x
     Await f -> onAwait $ \x -> foldConsumer onPure onAwait (f x)
     Yield x _ -> absurd x

或者，您可以在与消费者打交道时忽略 yield 情况。这是此设计模式的通用版本:在需要时使用多态数据类型和 Void 来消除可能性。

Void 最经典的用法可能是在 CPS 中。

type Continuation a = a -> Void

也就是说，Continuation 是一个永远不会返回的函数。 Continuation 是“not”的类型版本。由此我们得到了CPS的一个monad(对应经典逻辑)

newtype CPS a = Continuation (Continuation a)

由于 Haskell 是纯粹的，我们无法从这种类型中得到任何东西。