Data.Void中的荒诞函数有什么用呢？

Question

Data.Void中的absurd函数具有以下签名，其中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

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

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

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

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

type Continuation a = a -> Void

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

newtype CPS a = Continuation (Continuation a)

因为Haskell是纯的，所以我们不能从这个类型中得到任何东西。

Answer 2

考虑由其自由变量参数化的lambda项的这种表示。(参见Bellegarde和Hook 1994，Bird和Paterson 1999，Altenkirch和Reus 1999的论文。)

data Tm a  = Var a
           | Tm a :$ Tm a
           | Lam (Tm (Maybe a))

当然，您可以使它成为一个捕获重命名概念的Functor和一个捕获替换概念的Monad。

instance Functor Tm where
  fmap rho (Var a)   = Var (rho a)
  fmap rho (f :$ s)  = fmap rho f :$ fmap rho s
  fmap rho (Lam t)   = Lam (fmap (fmap rho) t)

instance Monad Tm where
  return = Var
  Var a     >>= sig  = sig a
  (f :$ s)  >>= sig  = (f >>= sig) :$ (s >>= sig)
  Lam t     >>= sig  = Lam (t >>= maybe (Var Nothing) (fmap Just . sig))

现在考虑封闭的术语:这些是Tm Void的居民。您应该能够将封闭项嵌入到具有任意自由变量的项中。多么?

fmap absurd :: Tm Void -> Tm a

当然，问题是这个函数将遍历术语“什么都不做”。但它比unsafeCoerce更诚实一点。这就是为什么vacuous被添加到Data.Void中...

或者编写一个求值器。下面是b中带有自由变量的值。

data Val b
  =  b :$$ [Val b]                              -- a stuck application
  |  forall a. LV (a -> Val b) (Tm (Maybe a))   -- we have an incomplete environment

我刚刚将lambda表示为闭包。赋值器由将a中的自由变量映射到b上的值的环境参数化。

eval :: (a -> Val b) -> Tm a -> Val b
eval g (Var a)   = g a
eval g (f :$ s)  = eval g f $$ eval g s where
  (b :$$ vs)  $$ v  = b :$$ (vs ++ [v])         -- stuck application gets longer
  LV g t      $$ v  = eval (maybe v g) t        -- an applied lambda gets unstuck
eval g (Lam t)   = LV g t

你猜对了。计算任意目标上的闭合项

eval absurd :: Tm Void -> Val b

更广泛地说，Void很少单独使用，但当您想要以某种方式实例化类型参数时(例如，在这里，使用封闭项中的自由变量)，它是很方便的。通常，这些参数化类型带有高阶函数，将参数上的操作提升为整个类型上的操作(例如，这里为fmap、>>=、eval)。因此，您将absurd作为Void上的通用操作传递。

再举另一个例子，想象一下使用Either e v来捕获计算，它有望给出一个v，但可能会引发e类型的异常。您可以使用此方法来统一记录不良行为的风险。要在此设置中进行行为良好的计算，请将e设置为Void，然后使用

either absurd id :: Either Void v -> v

要安全运行，或者

either absurd Right :: Either Void v -> Either e v

在不安全的世界中嵌入安全组件。

哦，还有最后一次欢呼，处理“不可能发生的事”。它显示在一般的拉链结构中，光标不能在的任何地方。

class Differentiable f where
  type D f :: * -> *              -- an f with a hole
  plug :: (D f x, x) -> f x       -- plugging a child in the hole

newtype K a     x  = K a          -- no children, just a label
newtype I       x  = I x          -- one child
data (f :+: g)  x  = L (f x)      -- choice
                   | R (g x)
data (f :*: g)  x  = f x :&: g x  -- pairing

instance Differentiable (K a) where
  type D (K a) = K Void           -- no children, so no way to make a hole
  plug (K v, x) = absurd v        -- can't reinvent the label, so deny the hole!

instance Differentiable I where
  type D I = K ()
  plug (K (), x) = I x

instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g
  plug (L df, x) = L (plug (df, x))
  plug (R dg, x) = R (plug (dg, x))

instance (Differentiable f, Differentiable g) => Differentiable (f :*: g) where
  type D (f :*: g) = (D f :*: g) :+: (f :*: D g)
  plug (L (df :&: g), x) = plug (df, x) :&: g
  plug (R (f :&: dg), x) = f :&: plug (dg, x)

实际上，也许这是相关的。如果您喜欢冒险，这个unfinished article展示了如何使用Void来压缩带有自由变量的术语的表示

data Term f x = Var x | Con (f (Term f x))   -- the Free monad, yet again

在从Differentiable和Traversable函数器f自由生成的任何语法中。我们使用Term f Void来表示没有自由变量的区域，使用[D f (Term f Void)]来表示通过没有自由变量的区域的管道隧道，要么是到一个独立的自由变量，要么是到两个或更多个自由变量的路径中的交叉点。总有一天会把那篇文章写完。

对于没有值的类型(或者至少在上流社会中不值得一提)，Void非常有用。absurd就是你使用它的方式。

Answer 3

我在想，也许它在某些情况下是有用的，因为它是一种彻底处理“不可能发生”情况的类型安全方法

这是非常正确的。

你可以说absurd并不比const (error "Impossible")更有用。但是，它是受类型限制的，因此它唯一的输入可以是Void类型的内容，这是一种有意设置为无人居住的数据类型。这意味着没有可以传递给absurd的实际值。如果您曾经在代码分支中遇到类型检查器认为您可以访问Void类型的内容的情况，那么，好吧，您处于一种荒谬的境地。因此，您只需使用absurd来标记代码的这个分支永远不能到达。

"Ex from quodlibet“字面意思是”从一个错误的命题，任何事情都会发生“。因此，当您发现您持有的数据类型为Void时，您就知道手中掌握了错误的证据。因此，您可以填充任何您想要的漏洞(通过absurd)，因为从错误的命题开始，任何事情都会随之而来。

我写了一篇关于Conduit背后的想法的博客文章，其中有一个使用absurd的例子。

http://unknownparallel.wordpress.com/2012/07/30/pipes-to-conduits-part-6-leftovers/#running-a-pipeline