Data.Void 中的荒谬函数有什么用? [英] What's the absurd function in Data.Void useful for?

问题描述

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

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

我确实知道足够的逻辑来获得文档的评论，即根据命题类型对应，这对应于有效公式 ⊥ → 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.

令我困惑和好奇的是:这个函数在什么样的实际编程问题中有用?我在想，在某些情况下，作为一种详尽处理不可能发生"的情况的类型安全方式，它可能很有用，但我对 Curry-Howard 的实际用途知之甚少，无法判断该想法是否可行完全正确.

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.

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

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

推荐答案

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

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

事实证明这有点有用.考虑 Pipes

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)

这是来自 Gabriel Gonzales 的 Pipes 库的标准管道类型的严格化和简化版本.现在，我们可以将永远不会产生的管道(即消费者)编码为

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

这真的永远不会产生.这意味着 Consumer 的正确折叠规则是

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

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

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.

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

Probably the most classic use of Void is in CPS.

type Continuation a = a -> Void

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

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)

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

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

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