HaskellのData.Mapとそれを翻訳したScalazのMapのバグの話

.@kazzna 単純なミスではなく、「HaskellやScalaの言語の特徴による固有の問題(遅延評価？)」とか、全く違う原因の可能性がゼロなわけではないですけど。ローカル変数名まで含めてできるだけそのまま翻訳されてるので、わりと見比べやすいはずです(けど量が多い・・・)

2013-09-02 20:41:45

あーあと、もとのHaskellのやつがそもそもちょっと古いから、「もとのHaskellコード自体がバグってた」って可能性がゼロじゃないけど、まさかね・・・。というか、なぜちょっと古いやつ翻訳したんだろう・・・

2013-09-02 20:44:36

@xuwei_k もしかして：もとのHaskellコードで使われているアルゴリズムのバグ http://t.co/cN5Z2Isx3N http://t.co/J6ksrmFxWl （7.4.x - 7.6.xのものでは修正済み http://t.co/E258C6el39 ）

2013-09-02 21:37:58

@xuwei_k リンク先を見てみると分かると思いますが、Haskell コードだけがバグっていたのではなく、参照している論文のアルゴリズム自体に問題があったという話です。

2013-09-02 21:50:49

@shelarcy まじですか、ありがとうございます。ちょっと見てみます。そのバグってどういう現象が起きるんですか？今Scala版で発生してるのは、unionしてtoAscListしてみると、そもそもKeyが重複してたりと、Map内のデータ自体が壊れたりするっぽいのですが・・・

2013-09-02 21:52:17

Scala版が元にした containers-0.4.0.0 http://t.co/2YuvOVi3c9 をみると、リポジトリがdarcsだし、github上でcontainersみると、そのあたりの古いtagがあまり打たれてないし、ソースの履歴調べるのしんどい・・・

2013-09-02 21:58:06

おぉ・・・ http://t.co/YGs7iec78Q "Data.Mapのバグを取って定理照明系Coqで検証した"

2013-09-02 22:41:38

"proved in Coq that <3,2> is one and only one interger solution" http://t.co/pFqzk9LxpK https://t.co/rd3wAgqJ2L https://t.co/3ihOLhpnAn oh..

2013-09-02 22:50:52

@xuwei_k あっ、うろ覚えで少し勘違いしてましたが、元々のバグは delta が5に設定されているため、deleteMin で Map が壊れてしまうというものでした。（これ自体は Scala 版や参考にした Haskell コードでも修正済み）

2013-09-03 15:17:32

@xuwei_k で、kazu_yamamoto さんと pirapira さんのバージョンだと <3,2> だけが正しい、Milan のバージョンだと <4,2> も認められるけれど delete の性能を考えるとやはり <3,2> を採用した方が良いという話ですね。

2013-09-03 15:17:42

@xuwei_k Milan のバージョンが現 containers パッケージのベースで、パラメーターだけでなく比較演算子にも手が入っています。 https://t.co/zMiq3MfzFR https://t.co/FcnA7HXY9r

2013-09-03 15:18:01

@xuwei_k で、当時この修正を外から眺めていただけなので、元の Haskell コードに現在の Scala 版と同じバグがあったかどうか分かりませんが、

2013-09-03 15:18:36

@xuwei_k deleteMin も union も同じ木を平衡化するための関数やパラメーターに依存しているので、元の Haskell コードも同じバグを潜在的に抱えていた可能性が高いと考えている感じです。

2013-09-03 15:19:05

@xuwei_k c.f. http://t.co/axAcd2VU5x http://t.co/dNYnnrTTil

2013-09-03 15:19:24

.@xuwei_k @shelarcy 要素を削除すると、バランスが壊れるというバグでした。我々が証明したのはオリジナルの WBT で、Data.Map は WBT の亜種です。亜種の方も <4,2> (と <3,2> も？) はバランスが壊れないことが証明されています。

2013-09-03 15:29:43

Scalaz版のMapはどうせまだ入ったばかりでそれほど多く使われてるわけじゃないし、(どのくらいソースコード違うのかにもよるけど)、現在のコードをデバックするより最新のData.Mapをもとに書きなおすのが一番理想的な気がするが。まずなによりバグの原因の切り分け面倒

2013-09-03 15:32:01

Data.Map が亜種を使い続けているのは、オリジナルよりもサイズが小さいときに、深さが浅く収まるからです。

2013-09-03 15:34:55

.@xuwei_k @shelarcy Data.Map には、僕が書いたテストがたくさん付いているので、それを移植してテストするといいかもしれません。

2013-09-03 15:42:35

.@kazu_yamamoto このバグってratioやdeltaさえ変更すれば済む(ほかの関数の実装は変更しなくても)問題なんですかね？現在のScala版のものでratioやdeltaを変更してもどっちにしろテスト通らないし、Scala版は写し間違いの別のバグもある気がしてます

2013-09-03 15:44:27

haddock に "prop>" を入れたのは、Data.Map のテストを、ドキュメントに持ち上げるためなのさ。次の HP が出れば、準備は整う。

2013-09-03 15:45:09

.@xuwei_k キーがだぶるのは、明らかなバグです。探索木は、定義によりキーはだぶってはいけません。Haskell の Data.Map には、そのようなバグはないと思います。

2013-09-03 15:46:27

今日の豆知識：探索木は、キーが重複してはいけない。ヒープ(優先順位付きキュー)は、キーが重複してもよい。

2013-09-03 15:47:41