OCamlと順序付き線形型で効率のよいXML処理 (to be continued)

OCaml 研究

この記事は OCaml Advent Calendar 2012 の 24日目の記事です。 が、実際にアップロードしたのは2013年1月18日です。 本当はもっと実用的なネタを書く予定だったのですが、飽きた ので、いっそ思い切り趣味に走った記事を書くことにしました。

追記： 動作するものを github にアップロードしました。 https://github.com/keigoi/olt_ocaml

追記：ちゃんと書きませんでしたが、OCamlによるXML処理ができる実装が既に著者らによって公開されています。 http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/x-p/

順序付き線形型とXML(木)

児玉・末永・小林による この論文 (日本語の文献) は、XMLなどの木構造を再帰的にトラバースするプログラムを、より効率のよいストリーム処理プログラムに変換する方法について書いている。
わかりやすくいえば、DOM APIを使って書いた（書きやすいが中間表現として木を操作するので効率の悪い）プログラムを、SAX APIによる（ストリーム処理であり効率のよい）プログラムにコンパイルする、みたいなことをやっている。
これは実用上有用な場面がかなりあると思う(大量のXMLを処理するとか)のだが、任意のプログラムを変換できるわけではなく、順序付き線形型という特別な型システムで型付けできるプログラムを対象にしており、OCamlやHaskellでそのまま使えるわけではない。 上にも少し書いたように、後の論文で任意の木処理の関数をストリーム処理に変換できるOCamlのトランスレータがある。

(論文のコピーは小林先生のpublicationsページで公開されている。 日本語では順序付き線形型に基づく木構造処理プログラムからストリーム処理プログラムへの変換 (PPL2004) がヒットする。)

順序付き線形型とは

要するに、線形型に変数の使用順序の制限を加えた型システム…だろうか。より詳しく知りたい人は、論文の型システムを眺めるのもいいし、概要は小林先生のFLOPS2008のスライドがわかりやすいかもしれない。

そうだ、OCamlでやろう

OCamlでもこの枠組みを使えるようにしたいというのが当面の目標だ。木構造を処理するプログラムをOCamlで書くと、実際には木を走査せずストリーム処理が走るようになれば、なんだか面白いしひょっとしたら便利かもしれない。

そしてOCamlの型システムに手を入れるのは大変なので、素のOCamlで動くようにしたい。一見不可能に思えるが、勝算はある。以前すでにセッション型をOCaml上で実現したが、そもそもセッション型は線形型の一種である。似たような方法を使えば順序付き線形型も（たぶん）OCamlにエンコードできるはずだ(エンコードされた物体が実用的かどうかはともかくとして)。

とりあえず、勘でつくってみた。
型を合わせただけなのでまだ動かないが。

木

まずは論文の最初の型システムと同じく、葉に整数があり、節にはなにもラベルがついていない木を扱う。 OCamlで書くと

type tree = Leaf of int | Node of tree * tree

といったところだが、この定義は重要ではない、というより使わない。木はモナドの中に封じ込め、順序型により触る順序を制限するため、プログラムには陽に現れないのだ。

モナド

例によって事前条件 'p, 事後条件 'q をもつ indexedモナド ('p,'q,'a) monad を使いたいところだが、元の型システムにはもう一つトリックがあり、戻り値で返す(つまりストリームで出力する)木は変数に束縛できないようになっている。
これを実現するため、今回はパラメータ4つのモナド、

('p,'q,'t,'a) monad

を使う。 't は計算結果として生成される木の型を表す。計算が木を返す場合は ('p,'q,tree,'a) monad, 返さない場合は ('p,'q,none,'a) monad というふうにする。

型環境

事前条件、事後条件は順序付き線形型の型環境(論文中のΔ)を表すことにする。 Γ|Δ ├ M:τ という型判定を、どう事前条件と事後条件に分けるのかは明白ではないけれど、ノリでなんとなく書いているので許してほしい。

とにかく、

x:Tree,Δ

という(順序付き線形型の)型環境を、OCamlでは

(tree, delta) cons

という型で表すことにする。

木を触る関数

f : Tree -> τ

は、OCamlでは

f : ((tree,'p) cons, 'p, ?, ?) monad

というモナドになる。 ここで事前条件では (tree,'p) cons と型環境に木がひとつあるのに対して、事後条件は 'p であり、その木はもう触れなくなっているという線形型の性質を表現している。

パターンマッチ

パターンマッチは、葉の場合と節の場合にそれぞれ動作する計算を渡す高階関数で表す。

  val tree_case : 
     (int -> ('p, 'q, 't, 'a) monad) (*葉の場合*)
  -> ((tree, (tree, 'p) cons) cons, 'q, 't, 'a) monad  (*節の場合*)
  -> ((tree, 'p) cons, 'q, 't, 'a) monad (*パターンマッチ全体として*)

葉の場合には順序付き型の型環境には何も加わらない。
節の場合には、2つの部分木を表すエントリが型環境に加わる。

木をつくる

上にも書いたように、木を作る計算は ('p,'q,tree,'a) monad という型をもつ。 節を作るには、部分木を作る計算を２つ与える。葉を作るには整数を与えればよい。

  val node_make : ('p, 'q, tree, unit) monad -> ('q, 'r, tree, unit) monad -> ('p, 'r, tree, unit) monad
  val leaf_make : int -> ('p, 'p, tree, unit) monad

型

そんなわけで、実装はともかく、以下のシグネチャーでこの論文の順序付き線形型をなんとなく表現できていると思うことにしよう

module type OLT_Tree = sig
  type (+'hd, +'tl) cons
  type nil

  type none
  type tree

  type ('p,'q,'t,'a) monad
  val ret : 'a -> ('p, 'p, none, 'a) monad
  val (>>=) : ('p,'q,_,'a) monad -> ('a -> ('q,'r,'t,'b) monad) -> ('p,'r,'t,'b) monad
  val (>>) : ('p,'q,_,unit) monad -> ('q,'r,'t,'b) monad -> ('p,'r,'t,'b) monad


  val run : ((tree,nil) cons, nil, none, 'a) monad -> 'a
  val run_tree : ((tree,nil) cons, nil, none, 'a) monad -> 'a

  val tree_case : (int -> ('p, 'q, 't, 'a) monad) -> ((tree, (tree, 'p) cons) cons, 'q, 't, 'a) monad -> ((tree, 'p) cons, 'q, 't, 'a) monad

  val node_make : ('p, 'q, tree, unit) monad -> ('q, 'r, tree, unit) monad -> ('p, 'r, tree, unit) monad
  val leaf_make : int -> ('p, 'p, tree, unit) monad

end

使えるのか

そもそもこのシグネチャに対する実装が存在するかどうかも明らかじゃないけれど、それは存在すると仮定しておく。

論文の最初のほうに出てくる例を3つだけ書いて見ました。

tree_map

葉に対して与えられた関数を適用する高階関数です。

  let rec tree_map : 'p. (int->int) -> ((tree,'p) cons, 'p, tree, unit) monad = fun f ->
    tree_case 
      (fun n -> leaf_make (f n)) 
      (node_make (tree_map f) (tree_map f))

この型注釈は必要で、ないと型エラーです。そう、この再帰は多相再帰なのです。 型環境を表す 'p が、再帰の回数ごとに異なるためです。先が思いやられますね!

tree_fold

いわゆる木のcatamorphismです。 葉に対して適用する関数と、節に対して適用する関数をこんな感じに与えます。

  (* tree algebra *)
  type ('t,'a) tree_alg = 
      {fg: 'p. 
          ((int -> ('p, 'p, 't, 'a) monad) *
              (((tree, (tree, 'p) cons) cons, (tree, 'p) cons, 't, 'a) monad ->
               ((tree, 'p) cons, 'p, 't, 'a) monad ->
               ((tree, (tree, 'p) cons) cons, 'p, 't, 'a) monad));
      }

  let rec tree_fold : 'p 't 'a. ('t,'a) tree_alg -> ((tree, 'p) cons, 'p, 't, 'a) monad = fun alg ->
    tree_case
      (fun n -> fst alg.fg n)
      (snd alg.fg (tree_fold alg) (tree_fold alg))

突如としてランク2多相なレコードが出現していておののきますが、これはやはり型環境を表す'pが多相的であることが必要なためです。
このレコードは 葉に対する関数と節に対する関数のペアです。

実際に tree_fold を使って tree_map を定義するとこうなります：

  let tree_map2 f = 
    tree_fold 
      {fg=(fun n -> leaf_make (f n)),
          (fun m1 m2 -> node_make m1 m2)}
inc_alt

やはり多相再帰ですが、 tree_foldほど難しくはないです。

  let rec inc_alt : 'p. unit -> ((tree, 'p) cons, 'p, tree, unit) monad = fun () ->
    let inc_alt_even () =
      tree_case
        (fun x -> leaf_make (x+1))
        (node_make (inc_alt ()) (inc_alt ()))
    in
    tree_case
      (fun x -> leaf_make x)
      (node_make (inc_alt_even ()) (inc_alt_even ()))

まとめと今後の課題

このエントリでは、順序付き線形型をうまいこと OCaml にエンコードするためのさわりについて書いてみた。
ところで元の論文では、木構造をパターンマッチで処理するプログラムを ストリーム処理プログラムに変換するという話だった。
このOCamlのコードについても、実際にストリーム処理プログラムの一部として動作するように、モジュールの実装を与えていく必要がある。

また、順序付き線形型は制限がきつすぎるので、元論文では木の一部をバッファにためて順序の制限のない操作をできるようにしている。この制限は最新の論文ではなくなっている。これは必要だろう。

その他に、実用性を考えた場合、 葉や木の型は柔軟に与えられる必要がある。たとえばCamlp4等を駆使して、木の型をもとにストリーム処理関数を生成するといった工夫があると思う。