[解決済み] Data.Voidの不条理な関数って何に使うの？

質問

その 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 .

私が戸惑い、興味を持ったのは、この関数がどのような実用的なプログラミングの問題で役に立つのか、ということです。 私は、おそらく、"can't happen" のケースを網羅的に処理する型安全な方法として、いくつかのケースで有用であると考えていますが、その考えが正しい方向であるかどうかを判断するには、カレー ハワードの実際の使用について十分に知りませんでした。

EDIT: 例はできれば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)

これは、Gabriel Gonzales の標準的なパイプ型を厳格化・単純化したものです。 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 は "not." の型バージョンです。ここから、CPS のモナド（古典論理に対応）が得られます。

newtype CPS a = Continuation (Continuation a)

Haskellは純粋なので、この型から何も得ることはできません。