二重否定モナド

本記事では二重否定モナドを発見し、その正体を探ります。

なお、例外の発生や無限ループなどは無いものとします。

命題としての型

命題Pに対してその証拠eを考え、e :: Pと書くことにします。
「eは型Pの要素である」とも言います。

命題Pが少なくとも1つ以上の要素を持つとき、その命題は成り立つと言います。

正当化

命題Aが成立することの証拠aと、命題A → B(AならばB)が成立することの証拠fを持っているとします。

このとき命題Bが成立することの証拠も得られます。その証拠をf aと書くことにします。

ところで、命題AやBを型としてみなし、命題A → Bを関数の型A -> Bと見なしましょう。
すると、f :: A -> Bはただの関数で、f aは関数適用に見えてきます。

命題Aに対し、「Aが成り立つならばAが成り立つ」という恒真命題は恒等関数idに対応します。

同様に、命題A → Bの証拠fと命題B → Cの証拠gがあるとき、命題A → Cの証拠は関数合成g . fで表すことができます。

命題と型の対応関係は他にもありますが割愛します。

以降、型と命題を同一視します。

矛盾の型

Data.Voidで定義されているVoidは要素を持たない型です。

Voidを返すような関数f :: a -> Voidを書いてみます。

f :: a -> Void
f x = ???

???部分には何を書けば良いでしょう？
そもそも、Voidには要素が1つも無いのでこのような関数は書くことができないように思われます。
もし、Voidを返すような関数が書けたとすれば、Voidが値を持たないという事実に矛盾してしまうからです。

唯一例外があり、aがVoidのときは関数を書くことができます。

f :: Void -> Void
f x = x

「Voidの要素xを持っている」というあり得ない仮定から、Voidの要素を返すことに成功したわけです。

あり得ない仮定からはどんな結論をも導くことができ、Haskellではabsurdという関数が標準で用意されています。（空虚な真）

absurd :: Void -> a

否定

関数P -> Voidが得られたとします。
ここでPの要素を持っていると仮定すると、関数適用によりVoidの要素が得られることになります。これは矛盾です。

先ほどの観察と合わせて、Pは値を持たないはずです。
つまり、Pは成り立ちません。

したがって、命題Pの否定「Pでない」はP → Voidで表すことができます。

「Pでない」という命題を考える際は、Pの成立を仮定してVoidを導くような関数の型を考えれば良いわけです。

二重否定

命題Pの二重否定「(Pでない)でない」も同様に表すことができます。

(P → Void) → Void

二重否定の除去？

古典的な数学では、二重否定は即座に除去することができます。
つまり、「(Pでない)でない」ことを証明すれば、ただちに「Pが成り立つ」ことを証明したことになります。

しかし、今はHaskellで記述しているので事情が少し異なります。
この文脈では、「Pが成り立つ」という主張は単に"それが真であることを証明した"ということだけに留まらず、"それが真であることを示すアルゴリズムを記述した"ということになります。

実際、一般にPの二重否定の成立を示すアルゴリズムを持っているからと言って、Pの成立を示すアルゴリズムが得られるとは限らないようです。

二重否定モナド

二重否定を定義し、モナドインスタンスにしていきます。

newtype DoubleNegation a = DoubleNegation ((a -> Void) -> Void)

先へ進む前にnewtypeで作った型コンストラクタを剥がすヘルパー関数を用意しておきます。

unwrap :: DoubleNegation a -> (a -> Void) -> Void
unwrap (DoubleNegation notNotA) = notNotA

これはただのヘルパー関数ですが、読み方を変えると「aの二重否定」が成り立つ証拠と「aの否定」が成り立つ証拠の両方を持っているような状況は矛盾であるとも解釈できますね。

ファンクター

「aならばb」が成り立つ証拠と「aの二重否定」が成り立つ証拠を持っているとき、「bの二重否定」も成り立ちます。

やってみましょう。

instance Functor DoubleNegation where
    fmap aImpliesB (DoubleNegation notNotA) = DoubleNegation notNotB
        where notNotB notB = notNotA (notB . aImpliesB)

この主張の面白いところは、a自体の成立を示すアルゴリズムを持っていなくとも、aの二重否定の成立を示すアルゴリズムがあれば、aならばbを用いてbの二重否定の成立を示せるという点にあります。

関手則を満たすことも確認しておきましょう。

関手則

fmap id (DoubleNegation notNotA)
= DoubleNegation (\notB -> notNotA (notB . id))
= DoubleNegation (\notB -> notNotA notB)
= DoubleNegation notNotA
= id (DoubleNegation notNotA)

fmap (g . f) (DoubleNegation notNotA)
= DoubleNegation (\notB -> notNotA (notB . (g . f)))
= DoubleNegation (\notB -> notNotA ((notB . g) . f))

(fmap g . fmap f) (DoubleNegation notNotA)
= fmap g $ fmap f (DoubleNegation notNotA)
= fmap g $ DoubleNegation (\notB' -> notNotA (notB' . f))
= DoubleNegation (\notB' -> (\notB -> notNotA (notB' . f)) (notB . g))
= DoubleNegation (\notB -> notNotA ((notB . g) . f))

アプリカティブファンクター

まずはpureに関して考えましょう。

aが成り立つことの証拠を持っていれば、aの二重否定の成立も示せるということですね。

instance Applicative DoubleNegation where
    pure = DoubleNegation . aImpliesNotNotA
        where aImpliesNotNotA a notA = notA a

aImpliesNotNotA関数はData.Functionに定義されている(&)と同じです。

先ほど、二重否定の成立から元の命題を示せるとは限らないと言ったばかりですが、その逆は常に成り立つことが分かります。

続いてapについても考えましょう。

(aならばb)の二重否定が成立することの証拠と、aの二重否定が成立することの証拠を持っているならばbの二重否定が成立を示せるということですね。

instance Applicative DoubleNegation where
    (DoubleNegation notNotAImpliesB) <*> (DoubleNegation notNotA) =
        DoubleNegation notNotB
        where
        notNotB notB = notNotAImpliesB notAImpliesB
            where
            notAImpliesB aImpliesB = notNotA $ notB . aImpliesB

繰り返しになりますが、a自体やaならばb自体を成立させるアルゴリズムに言及していないところが面白い点です。

アプリカティブ関手則の成立の確認は割愛します。

補題の証明

モナドの実装の前に補題をいくつか示します。

いつでも二重否定を外せるとは限りませんが、特殊なケースでは二重否定を外すことができます。

偽である命題の二重否定は外すことができます。

doubleNegationOfFalseImpliesFalse :: DoubleNegation Void -> Void
doubleNegationOfFalseImpliesFalse (DoubleNegation notNotFalse) = notNotFalse id

否定の命題の二重否定から元となる否定の命題を導けます。

doubleNegationOfNegationImpliesNegation :: DoubleNegation (a -> Void) -> a -> Void
doubleNegationOfNegationImpliesNegation (DoubleNegation notNotNotA) a =
    notNotNotA (\notA -> notA a)

この時点でモナドの片鱗が見えるかと思います。

モナド

最後にbindについて考えます。

aの二重否定が成立することの証拠と、aが成り立つならばbの二重否定が成り立つことの証拠を持っているときに、bの二重否定の成立を示せるということですね。

instance Monad DoubleNegation where
    doubleNegationA >>= aImpliesDoubleNegationB =
        DoubleNegation
            $ doubleNegationOfNegationImpliesNegation
            $ fmap (unwrap . aImpliesDoubleNegationB) doubleNegationA

モナド則の確認は……割愛します。

継続モナド

冷静になって型を眺めてみると、二重否定モナドは単なる継続モナドの一具体例に過ぎません。
mtlパッケージのContモナドを拝借しましょう。

newtype Cont r a = Cont { runCont :: (a -> r) -> r }

ここでrをVoidとすれば先ほどまで扱っていたaの二重否定に早変わりです。

type DoubleNegation a = Cont Void a -- Cont { runCont :: (a -> Void) -> Void }

試しに「否定の命題の二重否定から元となる否定の命題を導ける」ことを示してみます。

module Data.DN where

import Control.Monad.Cont (Cont, runCont)
import Data.Void (Void)

type DoubleNegation a = Cont Void a

doubleNegationOfNegationImpliesNegation' :: DoubleNegation (a -> Void) -> a -> Void
doubleNegationOfNegationImpliesNegation' doubleNegationOfNegationA a =
    runCont ((\notA -> notA a) <$> doubleNegationOfNegationA) id

まとめ

二重否定がモナドになることが分かりました。

しかしその正体は単なる継続モナドでした。

以下、二重否定モナドの自力実装のまとめです。

Data/DoubleNegation.hs

module Data.DoubleNegation where

import Data.Void (Void)

newtype DoubleNegation a = DoubleNegation ((a -> Void) -> Void)

unwrap :: DoubleNegation a -> (a -> Void) -> Void
unwrap (DoubleNegation notNotA) = notNotA

instance Functor DoubleNegation where
    fmap aImpliesB (DoubleNegation notNotA) = DoubleNegation notNotB
        where
        notNotB notB = notNotA (notB . aImpliesB)

instance Applicative DoubleNegation where
    pure = DoubleNegation . aImpliesNotNotA
        where aImpliesNotNotA a notA = notA a

    (DoubleNegation notNotAImpliesB) <*> (DoubleNegation notNotA) =
        DoubleNegation notNotB
        where
        notNotB notB = notNotAImpliesB notAImpliesB
            where
            notAImpliesB aImpliesB = notNotA $ notB . aImpliesB

doubleNegationOfFalseImpliesFalse :: DoubleNegation Void -> Void
doubleNegationOfFalseImpliesFalse (DoubleNegation notNotFalse) = notNotFalse id

doubleNegationOfNegationImpliesNegation :: DoubleNegation (a -> Void) -> a -> Void
doubleNegationOfNegationImpliesNegation (DoubleNegation notNotNotA) a =
    notNotNotA (\notA -> notA a)

instance Monad DoubleNegation where
    doubleNegationA >>= aImpliesDoubleNegationB =
        DoubleNegation
            $ doubleNegationOfNegationImpliesNegation
            $ fmap (unwrap . aImpliesDoubleNegationB) doubleNegationA