Data.Void中有什么荒谬的function对你有用？
Data.Void的absurd函数具有以下签名，其中Void是由该包导出的逻辑上无人居住的types：
-- | Since 'Void' values logically don't exist, this witnesses the logical -- reasoning tool of \"ex falso quodlibet\". absurd :: Void -> a
我知道有足够的逻辑来得到文档的注释，这个注释对应于作为types的命题对应的有效公式⊥ → a 。
我感到困惑和好奇的是：这个函数有什么实用的编程问题是有用的？ 我认为在某些情况下，作为彻底处理“不可能发生”事件的types安全的方法，这可能是有用的，但是我不太了解Curry-Howard的实际用法，告诉我们这个想法是否在正确的轨道。
编辑：最好在Haskell的例子，但如果有人想使用依赖types的语言，我不会抱怨…
由于Haskell并不严格，所以生活有点困难。 一般用例是处理不可能的path。 例如
simple :: Either Void a -> a simple (Left x) = absurd x simple (Right y) = y
这原来是有用的。 考虑一个简单的Pipestypes
data Pipe abr = Pure r | Await (a -> Pipe abr) | Yield !b (Pipe abr)
这是来自Gabriel Gonzales'Pipes图书馆的标准pipe道types的严格和简化版本。 现在，我们可以编码一个从不屈服的pipe道（即消费者）
type Consumer ar = Pipe a Void r
这真的从来没有收益。 这意味着Consumer适当的折叠规则是
foldConsumer :: (r -> s) -> ((a -> s) -> s) -> Consumer ar -> s foldConsumer onPure onAwait p = case p of Pure x -> onPure x Await f -> onAwait $ \x -> foldConsumer onPure onAwait (fx) Yield x _ -> absurd x
或者，在处理消费者时可以忽略收益率情况。 这是这个devise模式的通用版本：使用多态数据types和Void在需要的时候去除可能性。
CPS中可能是Void最经典的用法。
type Continuation a = a -> Void
也就是说， Continuation是一个永不返回的函数。 Continuation是“不”的types版本。 由此我们得到了一个CPS（对应于经典逻辑）
newtype CPS a = Continuation (Continuation a)
由于Haskell是纯粹的，我们不能从这种types中获得任何东西。
考虑这个lambdaexpression式的表示法，用它们的自由variables进行参数化。 （参见Bellegarde and Hook 1994，Bird and Paterson 1999，Altenkirch and 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的居民。 你应该能够用任意的自由variablesembedded闭合项。 怎么样？
fmap absurd :: Tm Void -> Tm a
当然，这个function就是通过这个function来完成这个任务。 但这是一个比unsafeCoerce更诚实的unsafeCoerce 。 这就是为什么Data.Void添加到Data.Void …
或者写一个评估者。 这里是b有自由variables的值。
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自由variables映射到b的值来参数化。
eval :: (a -> Val b) -> Tm a -> Val b eval g (Var a) = ga eval g (f :$ s) = eval gf $$ eval gs where (b :$$ vs) $$ v = b :$$ (vs ++ [v]) -- stuck application gets longer LV gt $$ v = eval (maybe vg) t -- an applied lambda gets unstuck eval g (Lam t) = LV gt
你猜到了。 评估任何目标的封闭期限
eval absurd :: Tm Void -> Val b
更一般地说， Void本身很less使用，但是当你想以某种不可能的方式实例化一个types参数（例如，在这里使用一个闭合的自由variables）时，它是非常方便的。 通常，这些参数化types带有更高阶的函数，对整个types的操作参数（例如， fmap ， >>= ， eval ）进行提升操作。 所以你通过Void的通用操作就absurd了。
再举一个例子，想象一下使用e Either ev来捕捉计算，希望给你一个v但可能会引发etypes的exception。 您可以使用这种方法统一logging不良行为的风险。 对于这个设置中的完美performance计算，取e为Void ，然后使用
either absurd id :: Either Void v -> v
安全地运行
either absurd Right :: Either Void v -> Either ev
将安全组件embedded到不安全的世界中。
哦，还有最后一个欢呼，处理“不可能发生”。 它显示在通用的拉链结构中，光标不能到达的地方。
class Differentiable f where type D f :: * -> * -- an f with a hole plug :: (D fx, x) -> fx -- plugging a child in the hole newtype K ax = K a -- no children, just a label newtype I x = I x -- one child data (f :+: g) x = L (fx) -- choice | R (gx) data (f :*: g) x = fx :&: gx -- 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 DI = 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来压缩用自由variablesexpression的术语
data Term fx = Var x | Con (f (Term fx)) -- the Free monad, yet again
在任何从Differentiable和Traversable函数中自由生成的语法f 。 我们使用Term f Void来表示没有自由variables的区域， [D f (Term f Void)]表示通过没有自由variables的区域隧穿到孤立的自由variables，或者隧道到两个更多的自由variables。 必须完成那篇文章。
对于一个没有价值的types（或者至less，没有什么值得在有礼貌的公司说）， Void是非常有用的。 而absurd是你如何使用它。
我在想，在某些情况下，它可能是一种完全处理“不可能发生”事件的types安全的方法
这是正确的。
你可以说absurd不是比const (error "Impossible")更有用const (error "Impossible") 。 然而，它是types限制的，所以它唯一的input可以是Voidtypes的东西，这是一种有意无人居住的数据types。 这意味着没有实际的价值可以通过absurd 。 如果你最终在types检查者认为你有权访问types为Void的代码的分支，那么，你是在一个荒谬的情况。 所以你只是使用absurd的基本上标志着这个代码分支不应该达成。
“ex faso quodlibet”的字面意思是“从一个虚假的[主张]，任何事情都跟随”。 所以当你发现你所持有的是一个Voidtypes的数据时，你就知道你手上有假的证据。 因此，你可以填充任何你想要的洞（通过absurd ），因为从一个错误的命题，任何东西。
我写了一篇关于Conduit背后的想法的博客文章，其中有一个absurd的例子。
通常，您可以使用它来避免表面上部分模式匹配。 例如，从这个答案中获取数据types声明的近似值：
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 fr = case r of Known a -> absurd a Unknown s -> fs
如何表示空数据types有不同的方法。 一个是空的代数数据types。 另一种方法是使它成为∀α.α或别名
type Void' = forall a . a
在Haskell中 – 这是我们如何在系统F中进行编码（参见certificate和types的第11章）。 这两个描述当然是同构的，而同构是由\x -> x :: (forall aa) -> Void和absurd :: Void -> a见证absurd :: Void -> a 。
在某些情况下，我们更喜欢显式变体，通常如果空数据types出现在函数的参数中，或者更复杂的数据types（如Data.Conduit中） ：
type Sink imr = Pipe ii Void () mr
在某些情况下，我们更喜欢多态variables，通常空函数的types涉及到函数的返回types。
当我们在这两个表示之间转换时，就会出现absurd现象。
例如， callcc :: ((a -> mb) -> ma) -> ma使用（隐含） forall b 。 也可以是types((a -> m Void) -> ma) -> ma ，因为调用的继续并不实际返回，它将控制转移到另一个点。 如果我们想继续工作，我们可以定义
type Continuation ra = a -> Cont r Void
（我们可以使用type Continuation' ra = forall b . a -> Cont rb vacuousM type Continuation' ra = forall b . a -> Cont rb但是需要rank 2types。）然后， vacuousM将这个Cont r Void vacuousM Cont r Void转换成Cont rb 。
（另外请注意，您可以使用haskellers.com来search特定包的使用情况（反向依赖关系），比如查看使用虚拟包的人和方式。）
在像Idris这样的依赖types的语言中，它可能比Haskell更有用。 通常情况下，在模式匹配的总function中，一个实际上不能被推入到函数中的值时，您将构造一个无人居住types的值，并使用absurd来定义案例定义。
例如，这个函数从列表中删除一个元素，其types级别为costraint：
shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect na shrink (x :: ys) Here = ys shrink (y :: []) (There p) = absurd p shrink (y :: (x :: xs)) (There p) = y :: shrink (x :: xs) p
第二种情况是说在空的清单中有某种要素，这是荒谬的。 然而，总的来说，编译器并不知道这一点，我们通常必须明确。 然后编译器可以检查函数定义是不是部分的，我们获得更强大的编译时间保证。
通过库里 – 霍华德的观点，命题在哪里，那么absurd就是一种矛盾的certificate中的QED。
