mplus は常に結合的である必要がありますか? Haskell wiki vs. Oleg Kiselyov 質問する

Question

以下はオレグ氏自身の意見と私のコメント、そして彼の説明です。

わかりましたまず、私はガブリエル・ゴンザレス氏に反対の意を表明したいと思います。がおよびMonadPlusに関してモノイドであるべきだということに誰もが同意しているわけではありません。レポートではそれについては何も述べられていません。そうではない説得力のあるケースが多数あります (以下を参照)。一般に、代数構造はタスクに適合するはずです。そのため、グループがあり、より弱い半グループまたは群 (マグマ) もあります。は、検索/非決定性モナドと見なされることが多いようです。そうであれば、の特性は、検索と検索に関する推論を容易にするものでなければなりません。誰かが何らかの理由で好む理想的なアドホックな特性ではありません。例を挙げましょう。法則を仮定するのは魅力的です。mplusmzeroMonadPlusMonadPlus

m >> mzero === mzero

しかし、探索をサポートし、他の効果も実行できるモナド（を考えてみてくださいNonDeT m）は、この法則を満たすことができません。例えば、

print "OK" >> mzero  =/==  mzero

左側には何かが印刷されますが、右側には印刷されないからです。同様に、mplusは対称にできません。一般に、は同じモデルのmplus m1 m2とは異なります。mplus m2 m1

について考えてみましょうmplus。連想的である必要がない主な理由は2つありますmplus。1つ目は検索の完全性です。

ones = return 1 `mplus` ones

foo = ones `mplus` return 2
  === {- inlining ones -}
  (return 1 `mplus` ones) `mplus` return 2
  === {- associativity -}
  return 1 `mplus` (ones `mplus` return 2)
  ===
  return 1 `mplus` foo

したがって、偶然帰納的に、ones と foo は同じであると思われます。つまり、foo から答え 2 を得ることは決してありません。

この結果は、が結合的かつ非可換であるMonadPlus限り、によって表される任意の検索に当てはまります。したがって、が検索のモナドである場合、の結合性は不合理な要件です。mplusMonadPlusmplus

2 つ目の理由は、確率的検索、または一般に、いくつかの選択肢に重みが付けられている場合には重み付き検索が望ましい場合があることです。確率的選択演算子が結合的でないことは明らかです。そのため、私たちの JFP 論文では、にモノイド ( mplus、mzero) 構造を課すことを特に避けていますMonadPlus。

http://okmij.org/ftp/Computation/monads.html#lazy-sharing-nondet（論文の図1に関する議論を参照）。

RCガブリエルさんとあなたは、検索モナドがモノイド構造を示さないという点では同意していると思います。議論は、検索MonadPlusモナドにを使用するべきか、それともとMonadPlus'似ていMonadPlusますが規則が緩いと呼ばれる別のクラスを使用するべきかという点に行き着きます。おっしゃるとおり、レポートではこのトピックについては何も述べられておらず、決定する権限もありません。

推論の目的上、私はそれに何の問題もないと思います。ただ、事例についての彼女の仮定を明確に述べればよいのですMonadPlus。

'esを再関連付けする書き換え規則に関してはmplus、関連付けられないインスタンスが「壊れている」かどうかに関係なく、単に存在し、広く使用されているMonadPlusことから、おそらくその定義は控えるべきでしょう。

わかりました私はガブリエルの発言には同意できないと思う

モノイド法則は最低限の要件です。なぜなら、モノイド法則がなければ、他の法則は意味をなさないからです。たとえば、と言う場合mzero >>= f = mzero、まずはの適切な定義が必要ですmzeroが、恒等法則がなければ、それは実現できません。モノイド法則は、提案されている他の法則を「正直」に保つものです。モノイド法則がなければ、適切な法則はなく、法則のない理論的な型クラスに何の意味があるのでしょうか。

たとえば、LogicT 論文、特に JFP 論文には、の結合性のない非決定性に関する等式推論の例がたくさんありますmplus。JFP 論文では、mplusとのすべてのモノイド法則が省略されていますmzero(ただしは使用しています)。とmzero >>= f === mzeroのモノイド法則がなくても、非決定性と検索に関する「正直な」かつ「賢明な法則」を持つことができるようです。mplusmzero

私もその主張に同意できるかどうかはわかりません

誰もが従うべきであると同意する 2 つの法則は、MonadPlus恒等法則と結合法則 (別名モノイド法則) です。

これについて世論調査が行われたかどうかはわかりません。報告書には法律は記載されていませんmplus(おそらく著者らはまだ議論中だったのでしょう)。したがって、この問題は未解決であり、これが伝えるべき主なメッセージであると言えます。

Answer 1