第12回プログラミングおよびプログラミング言語ワークショップ に行ってました。 お茶大のshift/reset推進委員会に対抗できる勢いでtree transducer勢が活躍していて素晴らしいことです。 それはともかく、面白かった発表をいくつかメモ。
『極性をもたないセッション型システム』。 セッション型（…とは何かはご本人のブログの解説をどうぞ）の既存の型システムは、チャンネルの自由な受け渡しを禁止した制約のあるものか、 極性という概念を入れてややこしくしたものか、どちらかだったそうなのだけど、そういう制限を無くせました！ という結果だそうな。個人的に面白いなーと思ったのは、型システムの健全性 （＝「型チェック通ったプログラムは実行時型エラーを起こさない」）の証明のために、 よくある type preservation (式eに型Tがつくなら、式eの実行を進めた結果の式e'にも同じ型Tが必ずつく) という補題は示せなくて、typability preservation とでもいうべきもの（e'に元と同じ型Tがつくとは限らないが、 なにかしら別の型T'は必ずつく）という補題を使う、という部分。 ここが一番のメインのアイデアではないらしいのですが、勝手に私がすごく面白そうと思っています。 なにか soft typing な方面に近いアイデアがあったりしそうな気がするし、ないなら何か応用できそうな…。
『Self Type Constructors』。
Scala 2.8 のコレクションライブラリの挙動
のようなものをハイパワーにマジカルに頑張るのではなくて、もう少し素直にできないものかいな、
というモチベーションで Java の型システムを拡張。
要は、Scala の this.type みたいなもの（継承先のメソッドとして使うときは自動的にその継承先の型）
を型コンストラクタとしても使える感じにに拡張。
class Bag<T> {ThisType<T> map(f) {...}}
から
class Set<T extends Comparable> extends Bag<T> {}
を派生すると Set<T> を返すmapメソッドができあがる。
class String extends List<Char> {} みたいに型引数が減るような継承をしたい場合も扱えますか、
という質問が出て、これはちょっと難しいらしい。懇親会の時に、C++ で比較関数を型パラメタにするように
class Set<T, Comparator> extends Bag<T> {} と型引数を増やすような継承はどうですか、
と聞いてみたところ、こっちは扱えそうらしい。
『Untyped Recursion Schemes and Infinite Intersection Types』 Recursion Scheme というのは、形式言語理論屋さん的に見ると無限の木構造を生成する高階文法なのですが、 これを型付きλ計算の可能な実行トレース集合の表現と見ることができて、それを使って高階関数型言語の性質検査をする、 という研究が最近ホットです。さて、型付きλ計算の実行トレースの表現として見られるなら、 その「型」の部分を外せば形無しλ計算を表現できるよね、というのは、 確かにこのλ計算の方向から見るととても当たり前に見えるのですが、文法規則として見ているとその発想はなかったです。 なるほどなあ、と感心していました。あと、この手法で性質検査が decidabable になるサブクラスの特徴付けの仕方がオートマトンオートマトンしてて自分の趣味的に楽しかった。
２日目の招待講演の 『Type-Based Reasoning for Real Languages』 (スライドPDF) は流石のわかりやすさ。 パラメトリシティ の説明と、 応用の軽い紹介、そして、単なる多相λ計算に限らず、 色々な言語機能の詰め込まれているリアルな関数型言語（要は Haskell）に対応した拡張パラメトリシティをどう確立していくか、という試みのまとめ。 パラメトリシティの証明には Logical Relation (論理関係) というテクニックを使うのですが、 「なんでこの技法を使うのか」という直感的な説明が （あんまりスライドには現れてなくて口頭でしたが） すごくわかりやすくてよかったです。
『条件式の解析によるSQLインジェクション脆弱性検査法の精度改善』 ユーザ入力が入る変数をSQLに埋め込むときにインジェクションが起きないことの検査、で、 従来研究は「正しくエスケープしている」のを認識して安全性の証拠として使う方向の検査法が主だったらしいのですが、 if文とかで変な入力を弾いているような部分を無視する感じになってて本当は安全な物にも警告を出してしまうことがあって、 その辺if文によるrejectも考慮できるように工夫したというお話。 中で使われている技術は、要は変数に入りうる文字列の正規表現パターンをどう伝搬していくか、 というもので、私のショートプレゼンの話と非常に近いところなので、色々お話させてもらいました。 楽しかったです。
『Tool Support for Crosscutting Concerns of API Documentation』 面白いという意味ではこれが一番面白かった。 アスペクト指向で言うところの「横断的関心事」はプログラムコードにだけ存在するのではない、 ドキュメントにも存在する、これはなんとかされるべきである、という主張。 正直なところ、これを「横断的関心事」と呼ぶのは少し違うのではないだろうかと思わないでもないのですが、 どういう名前で呼ぶかはさておくとして、確かにドキュメントのモジュラリティの問題は存在するし、 それをどうにかする、という方向は非常に正しいと思う。
自分の発表資料はこちら → （ショートプレゼン： [PPTX] [PDF]） （ポスター： [PDF]） です。ショートの方は、前々から気になっていた問題の解き方が思いつかないので、 公開しておけば誰か解いてくれるんじゃないかくらいの勢いで、簡単なケースの証明だけ用意して発表しにいきました。 まとめスライドの最後に挙げた「MTT*∩LSI = IRP∩LSI？」が、その、気になっている問題なんですけど、 "反例出せそうな気がする" "直感的には、成り立たないわけがないと思う" "バナッハ・タルスキの定理を応用して物凄く病的な反例をなんとか…" 等々まちまちな方向の反応をいただけて、 興味深いところです。