の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)
これは、GabrielGonzalesのPipesライブラリにある標準パイプタイプの厳密に簡略化されたバージョンです。これで、決して降伏しないパイプ（つまり、コンシューマー）を次のようにエンコードできます。
type Consumer a r = Pipe a Void r
これは本当に決して譲歩しません。これが意味することは、aの適切なフォールドルール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し、必要に応じて可能性を排除します。
おそらく最も古典的な使用法はVoidCPSです。
type Continuation a = a -> Void
つまり、aContinuationは決して戻らない関数です。 Continuation「not」のタイプバージョンです。これから、CPSのモナドを取得します（古典論理に対応）
newtype CPS a = Continuation (Continuation a)
Haskellは純粋なので、このタイプからは何も得られません。
自由変数によってパラメーター化されたラムダ項のこの表現を検討してください。（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。閉じた項を任意の自由変数を持つ項に埋め込むことができるはずです。どのように？
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
ラムダをクロージャとして表現しました。評価者は、自由変数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 e v別の例として、を使用して計算をキャプチャすることを想像してみてください。これvにより、タイプの例外が発生する可能性がありますe。このアプローチを使用して、不正な動作のリスクを一律に文書化できます。この設定で完全に正常に動作する計算を行うには、次のようeになりVoid、を使用します。
either absurd id :: Either Void v -> v
安全に実行するか
either absurd Right :: Either Void v -> Either e v
安全でない世界に安全なコンポーネントを埋め込むため。
ああ、そして最後の1つは、「起こり得ない」ことを処理することです。それは一般的なジッパー構造に現れ、カーソルがありえないところならどこにでも現れます。
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して、自由変数のない領域を表し、自由変数のない領域をトンネルして、孤立した自由変数、または2つ以上の自由変数へのパスのジャンクションにトンネルするチューブ[D f (Term f Void)]を表します。いつかその記事を終えなければなりません。
値のないタイプ（または少なくとも、礼儀正しい会社で話す価値のないタイプ）の場合、Void非常に便利です。そして、それabsurdをどのように使用するかです。
「起こりえない」ケースを徹底的に処理するタイプセーフな方法として、場合によっては役立つと思います。
これは正確に正しいです。
absurdあなたはそれがより有用であると言うことができますconst (error "Impossible")。ただし、タイプが制限されているため、入力はタイプの何か、Voidつまり意図的に無人のままにしておくデータタイプにすることができます。これは、に渡すことができる実際の値がないことを意味しますabsurd。タイプチェッカーがタイプの何かにアクセスできると考えるコードのブランチにたどり着いた場合Void、まあ、あなたはばかげた状況にあります。したがってabsurd、基本的に、このコードのブランチに到達してはならないことをマークするために使用します。
「Exfalsoquodlibet」は、文字通り「[a] false [命題]から、何でも続く」という意味です。したがって、タイプがであるデータを保持していることに気付いた場合Void、手元に誤った証拠があることがわかります。したがって、（を介して）必要な穴を埋めることができますabsurd。これは、誤った命題から、何でも続くためです。
Conduitの背後にあるアイデアについてのブログ投稿を書きました。これには、の使用例がありabsurdます。
一般に、これを使用して、明らかに部分的なパターンの一致を回避できます。たとえば、この回答からデータ型宣言の近似値を取得します。
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
空のデータ型を表す方法はいくつかあります。1つは、空の代数的データ型です。もう1つの方法は、∀α.αまたはのエイリアスにすることです。
type Void' = forall a . a
Haskellで-これはシステムFでそれをエンコードする方法です（証明とタイプの第11章を参照）。これらの2つの記述はもちろん同型であり、同型はによって\x -> x :: (forall a.a) -> Void、およびによって目撃されabsurd :: Void -> aます。
場合によっては、明示的なバリアントを使用することをお勧めします。通常、空のデータ型が関数の引数に表示される場合、またはData.Conduitなどのより複雑なデータ型に表示される場合です。
type Sink i m r = Pipe i i Void () m r
場合によっては、ポリモーフィックバリアントを使用することをお勧めします。通常、関数の戻り型には空のデータ型が含まれます。
absurdこれら2つの表現の間で変換しているときに発生します。
たとえば、callcc :: ((a -> m b) -> m a) -> m a（暗黙的）を使用しforall bます。((a -> m Void) -> m a) -> m a継続への呼び出しは実際には戻らないため、タイプも同じである可能性があり、制御を別のポイントに移します。継続を処理したい場合は、次のように定義できます
type Continuation r a = a -> Cont r Void
（使用することもできますtype Continuation' r a = forall b . a -> Cont r bが、ランク2のタイプが必要です。）次に、これをにvacuousM変換します。Cont r VoidCont r b
（また、haskellers.comを使用して、 voidパッケージを誰がどのように使用しているかを確認するなど、特定のパッケージの使用法（逆依存関係）を検索できることにも注意してください。）
Idrisのような依存型の言語では、Haskellよりもおそらく便利です。通常、関数全体では、実際には関数に押し込めない値とパターンマッチする場合、無人タイプの値を作成し、それを使用absurdしてケース定義を完成させます。
たとえば、この関数は、リストに存在するタイプレベルのコストレインを持つ要素をリストから削除します。
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
2番目のケースが空のリストに特定の要素があると言っている場合、それは非常にばかげています。ただし、一般的に、コンパイラはこれを認識していないため、明示的にする必要があります。次に、コンパイラは関数定義が部分的でないことを確認でき、より強力なコンパイル時の保証が得られます。
カリー・ハワードの観点から、命題はどこにあるのか、それabsurdは矛盾による証明の一種のQEDです。