的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 。
什么我困惑和好奇的是：在什么样的实际编程问题是这个功能有用吗？ 我想，也许它在某些情况下的详尽处理“不可能发生”的情况下，类型安全的方法是有用的，但我不知道有足够的了解咖喱霍华德的实际用途来告诉这个想法是否在步入正轨的。
编辑：最好的例子在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库。 现在，我们可以编码从不屈服的管道（即消费者）作为
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
或替代，您可以与消费者打交道时忽略的产量情况。 这是这种设计模式的一般版本：使用多态数据类型和Void摆脱的可能性，当您需要。
也许最经典的使用Void是CPS。
type Continuation a = a -> Void
也就是说，一个Continuation是永远不会返回的功能。 Continuation是的版型“不”。 由此我们得到（对应于经典逻辑），CPS的单子
newtype CPS a = Continuation (Continuation a)
因为Haskell是纯粹的，我们不能得到什么，这种类型的。
考虑此表示通过他们的自由变量参数化lambda项。 （见论文由里加答和胡克1994年，伯德和1999年帕特森，Altenkirch和雷乌斯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 ev捕捉计算其希望给你一个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和Traversable算符f 。 我们使用Term f Void来表示的区域与没有自由变量，并[D f (Term f Void)]通过与没有自由变量区域表示管隧道任一的分离的自由变量，或在路径的两个或一个结更自由变量。 有时必须完成这篇文章。
对于没有值的类型（或至少，在礼貌公司没有值得演讲）， Void是非常有用的。 而absurd是你如何使用它。
我想，也许它在某些情况下的详尽处理一个类型安全的方法“不可能发生”的情况下非常有用
这恰恰是正确的。
你可以说absurd不超过有用const (error "Impossible") 然而，它的类型的限制，使得其仅输入可以是类型的东西Void ，这是有意留无人居住的数据类型。 这意味着，还有就是你可以传递给没有实际价值absurd 。 如果你最终的代码分支，其中类型检查认为，您可以访问类型的东西Void ，然后，嗯，你是在一个荒谬的情况。 所以，你只需要使用absurd基本上标记出这个代码分支应该永远不会被达到。
“前FALSO quodlibet”字面意思是“从[α]假[命题]，任何如下”。 所以，当你发现你拿着一块的数据类型为Void ，你知道你在你的手中虚假证据。 因此，您可以填写你想要（通过任何孔absurd ），因为从一个伪命题，什么如下。
我写了一篇博客文章背后管道的想法具有使用的例子absurd 。
http://unknownparallel.wordpress.com/2012/07/30/pipes-to-conduits-part-6-leftovers/#running-a-pipeline
一般情况下，你可以用它来避免明显偏模式匹配。 例如，抓取从数据类型声明的近似值此答案 ：
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
有不同的方式如何表示空的数据类型 。 一个是空的代数数据类型。 另一种方法是让一个别名∀α.α或
type Void' = forall a . a
在Haskell -这是我们如何能够在系统F（参见第11章进行编码， 证明和类型 ）。 这两种描述是当然同构和同构由见证\x -> x :: (forall aa) -> Void和通过absurd :: Void -> a 。
在某些情况下，我们更喜欢明确的变型，平时如果空数据类型出现在一个函数的参数，或者在更复杂的数据类型，如Data.Conduit ：
type Sink i m r = Pipe i i Void () m r
在某些情况下，我们更喜欢多态性变异，通常是空的数据类型涉及函数的返回类型。
absurd ，当我们这两种表示之间的转换出现。
例如， callcc :: ((a -> mb) -> ma) -> ma用途（隐式） forall b 。 这可能是因为井型的((a -> m Void) -> ma) -> ma ，因为对contination呼叫实际上并不返回，其控制权转移到另一个点。 如果我们想与延续工作，我们可以定义
type Continuation r a = a -> Cont r Void
（我们可以使用type Continuation' ra = forall b . a -> Cont rb但会要求等级2点的类型。）然后， vacuousM将这个Cont r Void成Cont rb 。
（另请注意，您可以使用haskellers.com搜索使用率（反向依赖关系）的某个软件包，喜欢看到谁和如何使用的空白包）。
在像伊德里斯依赖性类型语言中，它可能比在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
其中第二种情况是说，有一个空的列表，其中，还有一个荒谬的某些元素。 但一般情况下，编译器不知道这一点，我们经常要明确。 那么编译器可以检查函数的定义是不偏，我们获得更强的编译时间保证。
通过视，到哪里都是命题咖喱霍华德点，那么absurd是用反证法证明排序QED的。
