中的absurd函数Data.Void具有以下签名，其中Void是该包导出的逻辑上无人居住的类型：
-- | Since 'Void' values logically don't exist, this witnesses the logical
-- reasoning tool of \"ex falso quodlibet\".
absurd :: Void -> a
我确实知道足够的逻辑来获得文档的注释，即通过 Proposal-as-types 对应，这对应于有效的公式⊥ → a。
我感到疑惑和好奇的是：这个函数在什么样的实际编程问题中有用？我在想，在某些情况下，作为一种彻底处理“不可能发生”情况的类型安全方式，它可能很有用，但我对 Curry-Howard 的实际用途知之甚少，无法判断这个想法是否在完全正确。
编辑：最好在 Haskell 中举例，但如果有人想使用依赖类型的语言，我不会抱怨......
生活有点艰难，因为 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)
Pipes这是 Gabriel Gonzales库中标准管道类型的严格简化版本。现在，我们可以将永远不会产生的管道（即消费者）编码为
type Consumer a r = Pipe a Void r
这真的永远不会产生。这意味着 a 的正确折叠规则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
或者，您可以在与消费者打交道时忽略收益情况。这是此设计模式的一般版本：使用多态数据类型并Void在需要时消除可能性。
可能最经典的用法Void是在 CPS 中。
type Continuation a = a -> Void
也就是说，aContinuation是一个永远不会返回的函数。 Continuation是“不”的类型版本。由此我们得到一个 CPS 的单子（对应于经典逻辑）
newtype CPS a = Continuation (Continuation a)
由于 Haskell 是纯的，我们无法从这种类型中得到任何东西。
考虑由自由变量参数化的 lambda 项的这种表示。（参见 Bellegarde 和 Hook 1994 年、Bird 和 Paterson 1999 年、Altenkirch 和 Reus 1999 年的论文。）
data Tm a = Var a
| Tm a :$ Tm a
| Lam (Tm (Maybe a))
您当然可以将其设为 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
我刚刚将 lambdas 表示为闭包。评估器由将自由变量映射a到值 over的环境参数化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)
实际上，也许它是相关的。如果您喜欢冒险，这篇未完成的文章将展示如何使用Void自由变量来压缩术语的表示
data Term f x = Var x | Con (f (Term f x)) -- the Free monad, yet again
Differentiable在从 a和Traversablefunctor自由生成的任何语法中f。我们Term f Void用来表示没有自由变量的区域，并[D f (Term f Void)]表示通过没有自由变量的区域的管子隧道到一个孤立的自由变量，或者到两个或多个自由变量的路径中的连接点。必须在某个时候完成那篇文章。
对于没有价值观的类型（或者至少在礼貌的公司中不值得一提），Void非常有用。并且absurd是你如何使用它。
我在想，在某些情况下，作为一种彻底处理“不可能发生”情况的类型安全方式，它可能很有用
这是完全正确的。
你可以说这absurd并不比const (error "Impossible"). 但是，它是类型受限的，因此它的唯一输入可以是 type Void，一种故意无人居住的数据类型。这意味着没有可以传递给的实际值absurd。如果你最终进入一个代码分支，类型检查器认为你可以访问 type 的东西Void，那么，那么，你处于一个荒谬的境地。所以你只是absurd用来基本上标记这个代码分支永远不应该到达。
“Ex falso quodlibet”的字面意思是“从 [a] 错误 [proposition]，任何事情都随之而来”。所以当你发现你手里拿着一个类型为 的数据时Void，你就知道你手里有假证据。因此，您可以（通过）填补您想要的任何absurd漏洞，因为从一个假命题开始，任何事情都会随之而来。
我写了一篇关于 Conduit 背后想法的博客文章，其中有一个使用absurd.
有不同的方式来表示空数据类型。一种是空代数数据类型。另一种方法是使其成为∀α.α的别名或
type Void' = forall a . a
在 Haskell 中 - 这就是我们如何在 System F 中对其进行编码（参见证明和类型的第 11 章）。这两种描述当然是同构的，同构由\x -> x :: (forall a.a) -> Void和见证absurd :: Void -> a。
在某些情况下，我们更喜欢显式变体，通常如果空数据类型出现在函数的参数中，或者出现在更复杂的数据类型中，例如在Data.Conduit中：
type Sink i m r = Pipe i i Void () m r
在某些情况下，我们更喜欢多态变体，通常空数据类型包含在函数的返回类型中。
absurd当我们在这两种表示之间转换时出现。
例如，callcc :: ((a -> m b) -> m a) -> m a使用 (隐式) forall b。它也可以是 type ((a -> m Void) -> m a) -> m a，因为对 contination 的调用实际上并没有返回，它会将控制权转移到另一个点。如果我们想使用延续，我们可以定义
type Continuation r a = a -> Cont r Void
（我们可以使用type Continuation' r a = forall b . a -> Cont r b，但这需要 2 级类型。）然后，vacuousM将其转换Cont r Void为Cont r b.
（另请注意，您可以使用haskellers.com搜索某个包的使用（反向依赖），例如查看谁以及如何使用void包。）
通常，您可以使用它来避免明显的部分模式匹配。例如，从这个答案中获取数据类型声明的近似值：
data RuleSet a = Known !a | Unknown String
data GoRuleChoices = Japanese | Chinese
type LinesOfActionChoices = Void
type GoRuleSet = RuleSet GoRuleChoices
type LinesOfActionRuleSet = RuleSet LinesOfActionChoices
然后你可以absurd像这样使用，例如：
handleLOARules :: (String -> a) -> LinesOfActionsRuleSet -> a
handleLOARules f r = case r of
Known a -> absurd a
Unknown s -> f s
在像 Idris 这样的依赖类型语言中，它可能比在 Haskell 中更有用。通常，在一个总函数中，当您模式匹配一个实际上无法推入函数的值时，您将构造一个无人居住类型的值并使用它absurd来完成案例定义。
例如，此函数从列表中删除一个元素，该元素具有该元素存在的类型级 costraint：
shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a
shrink (x :: ys) Here = ys
shrink (y :: []) (There p) = absurd p
shrink (y :: (x :: xs)) (There p) = y :: shrink (x :: xs) p
第二种情况是说空列表中有某个元素，这很荒谬。然而，一般来说，编译器不知道这一点，我们通常必须明确。然后编译器可以检查函数定义不是部分的，并且我们获得了更强的编译时保证。
通过 Curry-Howard 的观点，命题在哪里，那么absurd在矛盾的证明中是一种 QED。