-
- いいね！0
lotz
@lotz84_
書きました〜！ #Haskell ／ Levelsモナドを使った幅優先探索の仕組み zenn.dev/lotz/articles/…
2021-09-03 13:59:13
lotz
@lotz84_
do x <- [1..] y <- [1..] z <- [1..] guard $ x^2 + y^2 == z^2 pure (x, y, z) だとzの列挙が終わらなくて何も出力されないけど、xyzを二重リストにして適切なモナドを定義すると、和が小さい組み合わせから順番に出力されて、期待通りにピタゴラス数の無限リストが手に入るという話
2021-09-03 16:14:33
専門性・売上・原稿
@golden_lucky
勝手に幅優先探索になるデータ構造という面白さだけでなく、データ型を定義してそれをモナドにするまでのすごくわかりやすいチュートリアルだった zenn.dev/lotz/articles/…
2021-09-03 16:32:29
lotz
@lotz84_
Levelsを使った幅優先探索をCatamorphismで二分木に実装してみた 幅優先探索の実装ってこんなに簡単だったっけｗ lotz84.github.io/recursion-algo… pic.twitter.com/sJKHoHAvQH
2021-09-03 18:01:19
拡大
Kenji Yoshida
@xuwei_k
zenn.dev/lotz/articles/… これsmallcheckみたいなproperty based testingの値の生成に使えないだろうか?元論文を見たけど直接そういう言及は無いな。 ただsmallcheckはLogicTを使っていて、LogicTに関する言及は論文内にある…🤔
2021-09-05 13:11:41
Kenji Yoshida
@xuwei_k
なるほど？ twitter.com/objectxplosive…
2021-09-05 13:16:33
眼力 玉壱號
@objectxplosive
ただ、あっちは rose tree と遅延評価で任意時点からの再開（及び世界線の分岐）をやってた（と昔ちょっと追いかけた時に見た）
2021-09-03 17:23:15
眼力 玉壱號
@objectxplosive
@xuwei_k well-typed.com/blog/2019/05/i… スね。参照されてる youtu.be/AIv_9T0xKEo とかも
2021-09-05 15:32:18
Kenji Yoshida
@xuwei_k
github.com/xuwei-k/Levels… github.com/xuwei-k/Levels… Scalaに翻訳してみたら、Monad則を満たさない？ものが出来上がってしまったんですが、自分が翻訳ミスしたのか、元のHaskellのやつが満たしていないのか、どっち・・・
2021-09-05 16:22:23
Nobuo Yamashita
@nobsun
すこし古いけれど、「関数プログラミングの楽しみ」第9章 論理プログラミングのためのコンビネータ あたりの話題かな。 twitter.com/xuwei_k/status…
2021-09-05 22:28:08
Kenji Yoshida
@xuwei_k
github.com/xuwei-k/Levels… 色々と勘違いをしていたので直したけれど、まだ満たさないな・・・
2021-09-05 22:50:02
Koji Miyazato
@viercc
@xuwei_k Monad則は厳密には満たしてない、というか内側のリストの順番を無視するという前提でのみMonad則を満たしていますね
2021-09-05 23:13:34
Kenji Yoshida
@xuwei_k
github.com/xuwei-k/Levels… Unit当てはめた場合に多項式の和と積になるぞ！ というのは、見事に論文通りに動いた気がする pic.twitter.com/DuAv6ddTd0
2021-09-05 23:37:13
拡大
さっきつくった
@make_now_just
@xuwei_k leancheck というproperty based testingライブラリがsmallcheckの問題点を指摘しながら、ほぼほぼ同様のことをやっていたはずです hackage.haskell.org/package/leanch…
2021-09-05 23:44:23
Kenji Yoshida
@xuwei_k
論文読んでHaskellへの翻訳みたいな作業、ひさしぶりにやった気がするけれど、思ったより衰えてもいないけど、全然実力向上してる感もないな (最近やってなかったのだからそれはそう)
2021-09-05 23:48:28
Koji Miyazato
@viercc
🧵 newtype Levels a = Levels [[a]] 話題のこの↑モナドだけど、（元ネタ論文にもあるように）正確には newtype Levels a = Levels [Bag a] です。ここでBag aは[a]から*順序の違いを無視した*型（Haskellでは書けない！）です。
2021-09-06 01:52:36
Koji Miyazato
@viercc
Bagのような型が仮にあれば、Levelsが正しくMonadであることをざっくり説明します。 まず、Bagそれ自体もMonadになります。モナド演算はリストのものと同じです。pure aは唯一aをもつBag、joinはBagのBagをとって、中身をすべて合わせてひとつのBagにします。
2021-09-06 01:52:37
Koji Miyazato
@viercc
リストモナド[]は[a]が自由モノイドであることに由来します。すなわち、随伴FreeMonoid |- ForgetMonoidに分解されます。このBagモナドも同様に、Bag aが自由可換モノイドであることに由来します。
2021-09-06 01:52:38
Koji Miyazato
@viercc
ListT m a = ListT (m [a])は、可換なモナドmに対してはモナド則を満たすモナドになっています。これは、「可換なモナドmはモノイドの圏上のモナドになっている」ことと、「あらゆる随伴F |- GとモナドTから、モナドG∘T∘Fが作れる」という事実によります。
2021-09-06 01:52:38
Koji Miyazato
@viercc
Levelsモナドの構成において、各レベルごとにBagを併合する<|>という演算がありました。 一般の可換モノイドaに対して、[a]の各"レベル"ごとに和をとるよう(<|>) :: (可換モノイド a) => [a] -> [a] -> [a]に一般化して、[a]を可換モノイドにできます。
2021-09-06 01:52:39
Koji Miyazato
@viercc
つまり、[]は可換モノイドaから可換モノイド[a]を作りだしています。これは可換モノイドの圏における関手になっています。 さらに言えば、[]は可換モノイドの圏のモナドでもあります！
2021-09-06 01:52:39
Koji Miyazato
@viercc
LevelsがモナドになるのはListTと同様の理由です。Bagは自由可換モノイド関手であり、[]は可換モノイドの圏におけるモナドであり、Levels = (忘却関手)∘[]∘Bagです！
2021-09-06 01:52:40
Koji Miyazato
@viercc
反例： xs = Levels [[""], [""]] ys = Levels [[""], [], ["A"]] (◆) = liftA2 (++) Applicative則から満たさなければならない次式 (xs ◆ ys) ◆ xs = xs ◆ (ys ◆ xs) は成り立たない。 twitter.com/viercc/status/…
2021-09-06 02:03:41