Data.Void中有什么荒谬的功能对你有用？ [英] What's the absurd function in Data.Void useful for?

问题描述

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

   -  |由于'虚空'值在逻辑上不存在，因此它证明了\ex falso quodlibet \的逻辑
  - 推理工具。 
 absurd :: Void  - > a 
  

我知道有足够的逻辑来获得文档中的相应的注释，类型对应关系，有效公式⊥→a 。

我很困惑和好奇的是：in这个函数有用的是什么样的实际编程问题？我在想，在某些情况下，它可能是一种全面处理不可能发生事件的类型安全方式，但我对咖喱霍华德的实际用途知之甚少，无法确定这个想法是否存在正确的轨道。

编辑：最好在Haskell中的例子，但如果有人想使用依赖类型的语言，我不会抱怨...

解决方案

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

  simple：或者Void a  - > a 
 simple（Left x）= absurd x 
 simple（Right y）= y 
  

这显然是有用的。考虑一个简单的类型 Pipes

 数据管道abr 
 =纯r 
 |等待（a  - >管道b）
 | Yield！b（Pipe abr）
  

这是标准管道类型的严格和简化版本来自Gabriel Gonzales的 Pipes 图书馆。现在，我们可以将一个从不产生的管道（即消费者）编码为

 类型Consumer ar = Pipe a Void r 
  

这真的不会收益。这意味着对于 Consumer 的适当折叠规则是

  foldConsumer ::（r  - > s） - > （（a→s）→s）→>消费者r  - > s 
 foldConsumer onPure onAwait p 
 =案例p 
 Pure x  - > onPure x 
等待f  - > onAwait $ \x  - >纯消费onAwait（f x）
收益x _  - >荒谬的x 
  

或者您可以忽略与消费者。这是这种设计模式的通用版本：使用多态数据类型和 Void 以在需要时摆脱可能性。

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

  type继续a = a  - >无效
  

也就是继续是一个永不返回的函数。 继续是not的类型版本。从这里我们得到一个CPS单元（对应于经典逻辑）

pre $ c $ new $ CPS a =继续（继续a）

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

The absurd function in Data.Void has the following signature, where Void is the logically uninhabited type exported by that package:

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

I do know enough logic to get the documentation's remark that this corresponds, by the propositions-as-types correspondence, to the valid formula ⊥ → a.

What I'm puzzled and curious about is: in what sort of practical programming problems is this function useful? I'm thinking that perhaps it's useful in some cases as a type-safe way of exhaustively handling "can't happen" cases, but I don't know enough about practical uses of Curry-Howard to tell whether that idea is on the right track at all.

EDIT: Examples preferably in Haskell, but if anybody wants to use a dependently typed language I'm not going to complain...

解决方案

Life is a little bit hard, since Haskell is non strict. The general use case is to handle impossible paths. For example

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

This turns out to be somewhat useful. Consider a simple type for Pipes

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

this is a strict-ified and simplified version of the standard pipes type from Gabriel Gonzales' Pipes library. Now, we can encode a pipe that never yields (ie, a consumer) as

type Consumer a r = Pipe a Void r

this really never yields. The implication of this is that the proper fold rule for a Consumer is

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

or alternatively, that you can ignore the yield case when dealing with consumers. This is the general version of this design pattern: use polymorphic data types and Void to get rid of possibilities when you need to.

Probably the most classic use of Void is in CPS.

type Continuation a = a -> Void

that is, a Continuation is a function which never returns. Continuation is the type version of "not." From this we get a monad of CPS (corresponding to classical logic)

newtype CPS a = Continuation (Continuation a)

since Haskell is pure, we can't get anything out of this type.

这篇关于Data.Void中有什么荒谬的功能对你有用？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！