2012年に読んだ面白論文を紹介する会

例のアレです。今年は五月頃にソニーリーダーを失くしてしまう、しかも突っ込んでいた論文のバックアップを取っていなかったという悲劇のおかげで、ちょっとアレがアレしてるんですけど…バックアップは大事ですね!

Sound Predictive Race Detection in Polynomial Time

race なんて大嫌いだーってなってる頃に読んだ論文です。今も変わらず嫌いですけど…とりあえず id:shinichiro_h さんがもう書いているのでアウトソーシング

…だけだとあまりにも酷いので、えーっと何が面白いかというか嬉しいかというと。兎に角 race というのは、race のないコードを書くのも一定大変なんですが、あるコードに race がないことを保障することができない、というのが何より辛いわけです。いくら race detector を利用して race が見つけられたとしても、false-negative が含まれている可能性があると悲しくって、矢張り本当に欲しいのは sound な race detector なわけです。この論文における実験では、実行効率のために導入する制限で若干 soundness が損なわれているのですが、それでも sound な race detector の提案というのは、素晴らしいなあ…という。

この論文は、practical な感じのものではなくって、今後 sound な race detector の研究をする人たちの足がかりになりたい、というような感じになっていて、じゃあその後はどうなってるのかなあと思って調べてみたのですが、特にこの一年で発展は無いようです。残念。
しかし primary author の人が "Residual Investigation: Predictive and Precise Bug Detection" とかいう、これまた面白げな論文を出されてるようなので、そのうち読みたいですね…

最後に、これは私感ですが、本当に race がないことを保障したいのなら、race detector で頑張るとかよりは、session type とかになるのかなあと思います。ただ、この論文を読み始めた頃のボクのモチベーションは「いかにして race のないコードを書くか」だったので…ちなみに論文を読んでも「いかにして race のないコードを書くか」については大して学べなかったので悲しかったです。

Data types a la carte

お前去年これ参照してる論文読んでただろ、という突っ込みは勘弁して頂きたい…何はともあれ kinaba さんが書いているのでアウトソーシング。とはいえこっちは紹介と言う感じでもないので、一応真面目に紹介。

所謂 Expression Problem (以下 EP)を解決しましょうという良くある論文なのですが、これの面白いのは、実は新しい手法とかは全く提案していなくて、既に提案されている手法を組み合わせるだけで EP を解決してしまっている、というところです。面白いというか、すごくよくまとまっているというか。

ADT が F-algebra の initial algebra として捉えられることも、型クラスで型の直和を表現し、"subtype" の関係の成り立つ型に injection や projection を提供する型クラスを使う手法も、ずっと昔から知られています。Free モナドもあまり調べていませんが Category theory 界隈では良く知られていたものだったようなので、多分全部 20 世紀のうちには発見されてるんじゃないでしょうか…それが 2008 年に LtU なんかで紹介されて一定盛り上がったのだから、面白い話ですね。この論文はまさに伝記系ラノベと呼べるのではないでしょうか。

ちなみに去年読んでたというのは "The Monad Zipper" ですね。先にこっち読んでいれば、どれだけ理解が楽だっただろうか…

A pattern for almost compositional functions

世の中には「ほとんど合成可能な関数」というものが存在します。定義を説明するのは面倒なので具体例を挙げると、例えば AST に対するα変換的な namer とか、インクリメントを代入式に置き換かえるような desugar とか。そういうのです。
これらの処理は、普通に実装すると AST に対する再帰関数になります。しかし、こういう再帰関数があまりたくさんできてしまうのは嬉しくないです。というのも、値コンストラクタが増えた際に全て書き換えないといけなくなるし、そうでなくとも本質的な処理に集中したいのに AST を舐めるための再起処理ばかり書かされるはめになりがち、特に practical なコードの AST なんかは値コンストラクタたくさんもっていることが多いので、本質的な処理を見失いがち。そんなわけで、本質的な処理のみを切り離して記述できるように、AST を舐める処理はまとめてしまいましょう、という話。

というと、これって "The Essence of the Iterator Pattern" (以下 EIP) の Traversable なんじゃない?と思う人もいると思います。ボクも最初は思いました。ところが少し違っていて、

class Functor t => Traversable t where
  traverse :: Applicative m => (a -> m b) -> t a -> m (t b)

class Functor t => Compos t where
  compos :: Applicative m => (t a -> m (t b)) -> t a -> m (t b)

みたいになっています(実際に論文に出てくる型クラスによる定義は GADTs のために rank2-polymorphism を使った定義になっています)。

Traversable は勝手にデータ構造を走査してくれます。逆にいうと、データ構造の走査をコントロールすることはできません。一方 Compos ではそれが可能になっています。逆にいうと、コントロールしてやる必要があります。それだけといえばそれだけなんですが、それぞれを catamorphism 的に使う場合、これは結構面白い物と対応していて…というのはちょっと今回は秘密です。2012 年に読んだ論文の話じゃないから…(本当は次の comfrk のネタにするかもしれないからだからなんて、言えないね!)

論文には他にも、相互再帰的な複数の型から成るデータ構造を扱う話や、GoF の Visitor で Compos を実現する話や、SYB を利用する話等色々あるのですが…兎に角、EIP の Traversable と違い、データ構造に対する走査をコントロールすることができる、しなければならないというのが EIP の Traversable を知っている人には面白いポイントなのではないかなと思います。知らない人には、こういう風に書けば AST みたいなのうまく扱えるんだへー、ぐらいの話だと思います。

実はこの論文は "A Pattern for Almost Homomorphic Functions" という、よりとんがった論文を読むために読んでいたのですが、そっちは内容が Haskell 的な意味で重すぎ(closed type families とか出てきます)なので、あまりおすすめしません。とりあえず hackage へのリンクだけおいて置きます。0.9 から 2.0 にバージョンあがってるのが謎、Typeable 周りで 1.0 どっかいったのかな。これ、モチベーションは面白いんですけどねえ…

Extensibility for the Masses Practical Extensibility with Object Algebras

大変面白い論文なのですが、ちょっと面白い部分の説明が難しいです。実際のコード例が簡単な分、余計に…

これも "Data types a la carte" 同様、所謂 EP を解決しましょうというよくあるお話なのですが、それを JavaC# のような、それほど強力な型システムを持たない、シンプルな generics しか備えていない言語で解決してしまいましょう、というものです。そのために Object Algebras というものを提案しています。これは、極論すると GoF の Visitor パターンと Abstract Factory パターンと Builder パターンを組み合わせてより上手く構成したものです…といってもなんのことか分かりませんよね。

おさらい。オブジェクト指向プログラミングでは、オブジェクトの階層としてデータ構造を表現します。このデータ構造に対し、ADT でいうところの値コンストラクタ相当を新たに追加することは簡単です。単純に継承を利用するだけで、既存のコードの変更もなく追加することができます。一方で、データ構造に対する操作を追加する際には、愚直にやると既存のクラスに片っ端から新たにメソッドを実装していくことになってしまうため、かなり大変です。
Visitor パターンは、この問題を解決するために、オブジェクトの階層として表現されたデータ構造に対する decomposition を、元のデータ構造を表現するクラスとは分離した形で実現するものとして GoF で定められたデザインパターンです。このパターンの弱点は、decomposition の実現に必要なダブルディスパッチのために元のデータ構造を表現するクラスに "accept" メソッドを用意しておく必要がある点です。つまり、完全には元のデータ構造を表現するクラスと分離できてはいないわけです。

Object Algebras は、データ構造の表現自体を抽象化してしまおう、という手法です。

interface IntAlg<A> {
  A lit(int x);
  A add(A e1, A e2);
}

これは "Lightweight Modular Staging" の値表現の抽象化にかなり近い手法ですね(多分…)。"Lightweight Modular Staging" も紹介したかったのですが、一度名前だけ出してるしまあいいかみたいな…それはよくて。

値を生成するコードは、このインターフェースを利用するようにします。これにより、具象的な値表現に依存することはなくなります。

<A> A make3Plus5(IntAlg<A> f) {
  return f.add(f.lit(3) + f.lit(5));
}

あとは、IntAlg を実装するだけです。例えば式を表すクラス群 Exp, Lit, Add が既にあるとして、

class IntFactory implements IntAlg<Exp> {
  public Exp lit(int x) {
    return new Lit(x);
  }
  public Exp add(Exp e1, Exp e2) {
    return new Add(e1, e2);
  }
}

こんな具合に実装します。これを先ほど定義したメソッドに放り込んでやると、

Exp e = make3Plus5(new IntFactory());

ちゃんと式が得られる、と。それだけです。本当にそれだけです。おしまいです。

論文の内容紹介としては、後はこの IntAlg が既存のコードの変更無しに拡張可能になっていること、つまり値コンストラクタを後から追加できることや、IntFactory のようなその実装も同様に拡張可能になっている、つまり値コンストラクタが後から追加されても、その部分だけ実装しなおせばよい、よってコードの重複等は発生しないこと…つまり EP が解決できていることが具体的なコード例でもって延々と説明されます。応用例なんかも出ます。特に難しいものではないので、是非読んでみて下さい。

兎に角重要かつ面白い部分は、データ型のエンコーディングの抽象化と、その基礎の部分です。なのですが、この部分がいかに面白いかを説明できるほどの能力がボクに備わっていなかったのでここでおしまいです。残念。