LOPSTR と PPDP という共同開催の国際会議に行っていました。論理に基づく / 宣言型のプログラミングがテーマだそうです。 実況は例によって togetter.com/li/164644 にまとめてあります。 LOPSTR の方は、あまりよく知らなかったんですが、発表を聴いてみると、かなりガッツリと Prolog の言語仕様のディープなところに触れるような話があって、まるで、 C++ や Scala で盛り上がってる自分のTwitterのタイムラインの Prolog 版を見てるような雰囲気で楽しかったです。
聴いた中では Sloth という Haskell のライブラリの話が一番面白かったので、帰ってから関連論文を読んでいました。
何をするライブラリかというと、書いた関数が「できるかぎり遅延評価する」ものになってるかテストする、 というもの。Sloth というのは怠け者という意味らしく、「ちゃんと遅延評価を活かして限界までサボってる」か調べ、 サボりが足りなかったら怒ってくれます。
「サボりが足りない」とは何か？ 実例として、標準ライブラリの Data.List.intersperse という関数の実装が槍玉に上がっていました。これ。
intersperse :: a -> [a] -> [a]
intersperse _ [] = [] -- 空リストは空リストに
intersperse _ (x:[]) = [x] -- 1要素のリストもそのまま
intersperse sep (x:xs) = x : sep : intersperese sep xs -- 複数あるときはsepで先頭要素を区切って繰り返し
intersperse 1 [2,3,4,5] = [2,1,3,1,4,1,5] のような、リストの間に値を挟み込む関数です。
これがサボり足りないのは何故かというと…、こんな入力を考えてください。
intersperse 1 (2 : ???) = ??? の部分は、遅延評価なのでまだ評価していません。空リストが来るのか、さらに要素が来るのか、まだ分からない。 でも限界までサボりたいので、この入力は評価しないままで、できるだけ出力を出したい。実際、できます。 ??? に空リストが来ようが要素が来ようが、どっちの場合でも、少なくとも
intersperse 1 (2 : ???) = 2 : !!!intersperse した結果のリストの先頭は絶対に 2 なはずです。ここまでは、??? の評価をサボった状態でも答えが出せます。
でも、残念ながら、上に引用した実装は、そうなっていません。
1個のリストなのか複数個のリストなのかパターンマッチで判定してから結果を出そうとしているので、
??? を評価してからでないと、2 : を出せない。遅延さが足りない。
参考までに、サボり抜いた実装は、こうなります。
intersperse' :: a -> [a] -> [a]
intersperse' _ [] = []
intersperse' sep (x:xs) = x : go sep xs
where go sep [] = []
go sep (x:xs) = sep : x : go sep xs
先頭だけ特別扱いして、あとは、
go 1 [3,4,5] = [1,3,1,4,1,5] のような 1 を先頭から1個置きに埋める関数として書いています。
これを、上の実装をした関数を渡すと「もっとサボれるぜ！」と教えてくれて、 下のを渡すと「怠け者免許皆伝」と表彰してくれるのが、Sloth だそうです。 論文によると、実際、標準ライブラリの intersperse の怠け度が足りないせいでメモリの使用量が思いっきり増えてしまった事例があるそうで、 そういう意味で、面白いだけではなく、実用面でも意味があるのかもしれません。
実装は、基本的には全探索です。 例えばリストだったら先程の ??? に入るものは空リスト [] か cons : のどちらかに決まるので、 全部試してみて
intersperse 1 (2 : []) = 2 : []
intersperse 1 (2 : _ : []) = 2 : 1 : _ : []「どっちにしろ先頭の 2 : は確定じゃん！ なのに、評価するときエラーになる式 undefined を入れた時」
intersperse' 1 (2 : undefined) = 2 : undefined「こうならないで」
intersperse 1 (2 : undefined) = undefined「いきなりエラーになる標準ライブラリの実装は、サボりにかける情熱が足りない！」
と判定します。 試すまでは何要素のリストで試すと反例が見つかるかはわからないので、それも、小さい方から全探索。 ちなみに、たとえ多相型の関数であっても パラメトリシティ のような性質を使って、同じような探索ができる、というの証明の部分が今回の会議に投稿された論文の中心でした。
このやり方には、一つ、落とし穴があります。 「昔にも同じ方向の研究があったが、この落とし穴が残っていたのを埋めた」というのが Sloth 自体のセールスポイントらしいです。何かというと、
and True b = b
and False b = False
この論理アンドの実装は限界までサボれているでしょうか。 この実装は第一引数を必ず評価していますが…
and True False = False
and False False = Fasle -- どっちも同じなので第一引数の情報は不要
and undefined False = undefined -- でも見に行ってエラーになってしまう
「第一引数をまったく評価しなくても答えが決まるケースなのに、この実装は第一引数を評価している！ もっと怠惰を！！」
しかしこれは無茶な要求です。
and2 b True = b
and2 b False = False
第二引数でパターンマッチするようにすれば、 確かに第一引数の評価をサボれる場合もありますが、今度は、
and2 False True = False
and2 False False = False -- どっちも同じなので第二引数の情報は不要
and2 False undefined = undefined -- でも見に行ってエラーになってしまう
「第二引数見なくてもわかるのに見てる！この働き者めが！！」
実際、これは理論的に無理な要求で、 これを完全にサボりきって早めのエラーを回避する 並列論理和は通常の方法では作れない ことがわかっています。 通常でない方法で作るとそれはそれで面白いことが色々できて楽しいのですが、 それはまた別のお話で、 判定ツールとしては、 「普通の真っ当な Haskell コードで書ける範囲で十分頑張って怠けていれば、OK」 と結果を出してくれた方が、有用です。
実際 Sloth では、そういった寛容なチェックが導入されていて、上の and も and2 も、 どちらも十分怠けていると褒めてくれます。 この許容範囲の拡大の実装は、これまた色々引数を入れて全探索してみることで、 普通のコードで書ける範囲では仕方無く引数に順番がついてしまう、というパターンを見つけるそうな。 詳しくはぜひぜひ論文読んでみて下さい。
数日前に Twitter でフォローされた方のプロフィールページに "翻訳者" というバッヂがついていて、 何だろ？と思って調べ始めたのですが、
こういうボランティアベースのシステムで翻訳されてるんですね。全然知りませんでした。 で、Twitter には随分楽しませてもらっているので、 ちょっと協力するかーと思って始めてみたところ、 結構これは面白い。
というわけで暇つぶしにオススメです。 やってみるには http://translate.twttr.com/ から。