On merging of two asynchronous queues

This is a personal note on what I implemented for this signature https://github.com/keigoi/ocaml-mpst/blob/master/lib/lwt/mstream.mli.

Comments are appreciated, but the followings are not meant to be read by others than myself.

----

Suppose you have two channels which are asynchronous — asynchronous queues. More precisely, an asynchronous queue q has the following properties:

1. A queue q consists of a triple (st,i,o): A stream st and two ends, output end o and input end i. Writing a message on o is immediately enqueued in st, which can be taken from i.
2. Writing on an output end is non-blocking.
3. Ordering in a stream is preserved. In other words, writings on an output end are ordered, i.e. messages m1 and m2 written in this order can only be read as first m1 then m2 on the input end, not conversely.

And I was thinking about merging of them. Here, merging is a concept derived from End Point Projection of Multiparty Sesison Types, but here is about queues and their ends, not types.

Let me informally establish what I meant by "merging".

• Rule i). Only two ends with the same modality (input/output) and the same payload type can be merged.
• Rule ii). Merging of two ends invokes merging of streams and the other ends; i.e. if two input ends are merged, then two streams and two output ends associated with them are merged into one respectively (here I assume the queues are empty); and vice versa. 

Merging means that the writing on a merged output end preserves ordering: writings "m1 to o1 then m2 to o2" can be observed in this order at the other end.

Rule ii) means that the merged ends are indistinguishable from each other. I.e., after merging two output ends o1 and o2, writing a message m on either o1 or o2 will have the same effect: it writes into the queue connected to them, without any flag or timestamp or any labellings.

Another implication is that two simultaneous inputs/outputs on the same ends will cause a race: If a stream contains only a message m0, simultaneous inputs on i1 and i2 will block one of them. Similarly, simultaneous outputs on o1 and o2 with messages m1 and m2 respectively will result in a stream non-deterministically enqueued with m1 then m2, or m2 then m1.

It bloated up to more than 20 lines, but actually easy: Merging unifies two queues into one, and after merging, they can be treated equally after that.

----

Then, let's add more complexity. Now, an asynchronous queue has its own wrapper function which transforms a message right before it is read by an input end.

A wrapped queue (st,i,o,f) consists of four elements: stream st, input end i, output end o and wrapper function f. Then, how the merging above should be defined properly?

Here is my solution using GADTs: 

https://github.com/keigoi/ocaml-mpst/blob/master/lib/lwt/mstream.ml  (However, this is tainted with a specific scatter/gather implementation of ocaml-mpst.)

Background thoughs might be explained in the following entry or revision of this entry.

制御の逆転 〜 OchaCaml と限定継続でイベンドハンドラをダイレクトスタイルで書く

昔、こういう記事を書いた：

OchaCamlで限定継続/answer type modificationを勉強する - keigoiの日記

もっと shift/reset で何か身の回りの例を書いてみたい。そこで限定継続を使って、イベントハンドラをコールバックではなくダイレクトスタイルで書けるようにする、ということをやってみる。

ユースケース

例がとても古くて恐縮だが、たとえば古きよきショッピングカートの web アプリを作るときは、普通はページのルーティングを書いて、クリックの度に発行される GET か POST リクエストに反応するイベントドリブンで構成することになる：

/* /item_list アイテム一覧ページ */
Page onItemList();

/* /confirm 注文の確認ページ */
Page onConfirm(Cart);

/* /thankyou 支払い完了ページ */
Page onThankyou()

これはよくあるパターンだけど、プログラムの制御の流れは「ぶつ切り」になり見辛いし、ページ遷移の流れもわからない…と言い張ることもできる。

しかし、もし限定継続があったならば、ページ遷移の流れをプログラムの制御フローにより直接的に書き下すことができる：

var cart = [];
while(true) {
  cart, checkout = show_item_list();
  if (checkout) {
    ok = show_confirm_page();
    if (ok) {
      break;
    }
  }
}
show_thankyou_page();

（実際、かつては継続を使った web アプリのフレームワークがいくつかあった。 Kahua とか。）

プログラム

int 型のイベント発生源があるとして、そのハンドラをコールバックではなくダイレクトスタイルで書いてみよう。
まずはライブラリコード：

(* int 型の穴をもつ継続 *)
type 'a t = Fini | Cont of (int / 'a -> 'a t / 'a)
let cont = ref Fini

(* 関数 body をイベントハンドラに登録する関数 *)
let register body = 
  cont := 
    reset (fun () -> 
      body (fun () -> shift (fun k -> Cont k))
    )

(* イベントハンドラ *)
let event x =
  match !cont with 
  | Fini -> failwith "finished" 
  | Cont k -> 
    cont := k x

実際にダイレクトスタイルでイベントハンドラを書いてみる：

(* int型のイベントを 2回待ってその和を表示する *)
register (fun f -> 
  let x = f () in 
  let y = f () in
  print_int (x+y); 
  Fini);;

イベント発生をシミュレートしてみましょう。 10, 20 が順番に起こったとする。

# event 10;;
- : unit = ()
# event 20;;
30- : unit = ()

見事、ダイレクトスタイルで書いたイベントハンドラが動き、和が表示されました。やったぜ。

これくらい Python の yield とかでも出来てしまうけれど、そのあたりはご愛嬌。
もっと専門的な例を見てみたい人は Continuation Workshop 2011 Tutorial を参照しましょう。
OchaCaml は研究用の言語ではあるものの、 Hindley-Milner 型推論と answer type modification があるので安全かつ自由度の高いプログラムが書けるのだ。

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

この記事は 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等を駆使して、木の型をもとにストリーム処理関数を生成するといった工夫があると思う。

最強OCamlでセッション型を実現

この記事は OCaml Advent Calendar 2012 の 18日目の記事です。

OCamlでセッション型を実装した、というお話です。ちょっと時間がないので簡潔に書いています。

• ソースはこちら

セッション型

セッション型とは:

• 通信チャネルの型です
• プライベートな二者間のメッセージ送受信が整合していることを保証してくれます。(定義によっては多者間)

例えば

let thread1 () = 
  send c "Hello"; 
  send c 123

という関数は文字列と整数をチャネルcに送るが (send c vはチャネルcに値vを送るプリミティブとする。以下同様)、

let thread2_bad () =
  let i = recv c in
  let j = recv c in
  print_int (i+j)

は整数を２つチャネルcで受けるため(recv cはcで受信した値を返す)、

let _ =
  Thread.create thread2_bad ();
  thread1 ()

のようにthread1, thread2_bad を並列に走らせると、セッション型の枠組みでは型エラーとして検出される。
次のように修正すれば、

let thread2 () =
  print_string (recv c);
  print_int (recv c)

let _ =
  Thread.create thread2 ();
  thread1 ()

thread1とthread2 のチャネルの使い方は整合しており、型チェックを通る。

• だが、HaskellやOCamlの型システムでは、そのままでは上のような型チェックはできない。例えば、

  send c "Hello"; 
  send c 123

は、cの型がstring channel か int channel のどちらか一方に型付けされてしまうため、OCamlでは型エラーになる。

どう実現したか

indexed monad (あるいはrestricted monad; 制限モナド)の方法を使った。通常の(プログラミングで使う)モナドは、

type 'a t
val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
val ret : 'a -> 'a t

なるシグネチャをもつモジュールで表されるが、indexed monadでは

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

というシグネチャになる(Haskellでも同様のことはできる)。
型パラメータ'p, 'q はそれぞれアクションの事前条件、事後条件を表している。
(>>=) の型を見ると、順接でつなぐ２つのアクションの事後条件と事前条件が整合していなければならない、という制限が読み取れると思う。

このindexed monadを使って通信を書くようにする。この事前条件、事後条件に、セッション型を埋め込んである。

仮に、チャネルの個数を１つに限定すれば

val send : 'a -> (('a, 's) send, 's, unit) monad

send 1という式は ((int, 's) send, 's, unit) monad という型をもつ。 (型(int,'s) send は、 整数を送り、その次に型'sの動作をする、と読む。)
セッション型は、アクションを起こす毎に型が変わってしまうが、それをindexed monadの事前条件・事後条件に埋め込んでやったというわけ。

複数のチャネルを扱うために、heterogeneous listの方法を使った。
OCamlでは、Haskellのような型クラスがないのでHaskellのようなheterogeneous listは作れないが、ガリグ先生の方法を使えば、似たようなことはできる。 参考

どんな風に使うか

let thread1 () =
  send c0 123 >>
  send c0 "Hello"

let thread2 () =
  recv c1 >>= fun v ->
  print_int v >>
  recv c1 >>= fun str ->
  print_string str

モナドっぽい書き方になっただけで、そんなに違和感なく使えると思う。
ただチャネルはpredefinedなc0,c1,...という名前しか使えない。チャネルというよりも、heterogeneous listのスロットの位置を表すインデックスと思ったほうがいいかもしれない。
各スレッドで使うチャネルの端点はc0,c1という名前で区別している。

動かすには

let _ =
  run (
    new_chan c0 c1 (a2b (a2b finish)) >>
    fork c0 thread1 () >>
    thread2 ()
  )

のようにする。 new_chanで新しいチャネルをスロットに割り当てる。この際、チャネルに割り当てるセッションの内容を書く必要がある。a2bは一方から他方に値を送るというセッションだ。
forkで新しいスレッドを作るのだけど、第一引数にはそのスレッドに所有権を渡すチャネルの名前を書く。

他にも実に多様な使い方ができるのだけど、それはまた。

なぜOCamlか

OCamlは、同値(equi-)再帰型をもつ。 これはループ(再帰)をもつセッションのセッション型をそのまま表現できるので、Haskellで必要だった変なエンコーディングが不要になっている。
コンパイルする時に、 -rectypes オプションを付ければ、これが使えるようになる。
(-rectypesを不要にする方法もあるのだけど割愛)

例えば、整数をずっと送りつづけるセッションは

(int, 'a) send as 'a

という型で自然に表すことができる。

Haskellだと、(以前私が作ったものだと)

Rec Z (Send Int (Var Z))

などというよくわからない型なっており、Rec型のfold/unfoldが必要で、スッキリしない。

同値再帰型をもつOCamlは最強言語ということですね。

OCamlで使える同値再帰型 (equi-recursive types) は恐ろしいけど、すごい

この記事は OCaml Advent Calendar 2012 の 17日目の記事です。

同値再帰型が何であるか知りたい方は、今後発売される TAPL日本語版を読むと良いと思います（私も翻訳しています。*1）。 Wikipedia英語版にもありますね。

同値再帰型は、再帰型の定式化の方法のひとつで、「型の再帰構造が外からまる見えな型」といった風情の型です。例えば無限リストは、普通の(同型)再帰型なら

type 'a inflist = InfList of 'a * 'a inflist
let rec ones = InfList(1, ones)

などと、ヴァリアント等を介さないと定義できませんが、 -rectypesオプションで同値再帰型が有効になっている場合、タプルを組み合わせるだけで無限リストを作れます。

let rec ones : int * 'a as 'a = 1, ones;;

この int * 'a as 'a が同値再帰型で、上の Wikipedia の記事の記法では μα. int * α などと表記されています。
この同値再帰型 FOOBAR as 'a は、 FOOBARに出現する 'a を自分自身に置き換えて展開した型もすべて同じ型とみなされます。つまり int * 'a as 'a と int * (int * 'a) as 'a と int * (int * (int * 'a)) as 'a 等は すべて同じ型とみなされます。型推論もちゃんと効くようです。すごいですね。

無限リストでなくても、任意の再帰型を同様の方法で作れます。例えばintのリストμα.(1+ int*α) と同様の構造をもつ型は、OCamlでは直和の部分を option で表現すれば (int * 'a) option as 'a という型で表現でき、次のように扱えます:

# let intlist = Some (0, (Some (1, (Some (2, None)))));;
val intlist : (int * (int * (int * 'a option) option) option) option =
  Some (0, Some (1, Some (2, None)))
# let rec map f = function Some (hd, tl) -> Some (f hd, map f tl) | None -> None;;
val map : ('a -> 'b) -> (('a * 'c) option as 'c) -> (('b * 'd) option as 'd) =
  <fun>
# map (fun x -> x+1) intlist;;
- : (int * 'a) option as 'a = Some (1, Some (2, Some (3, None)))
# 

もちろん木構造も表現できます（やってみましょう！）

フリーダムすぎる同値再帰型

恐らくメジャーな言語ではOCamlくらいにしか備わっていない同値再帰型(equi-recursive types)。
面白いですが、あまりにも自由すぎるせいで、恐らくプログラマが意図しない式にも型がついてしまいます。

$ ocaml
        OCaml version 4.00.1

# #rectypes;; (* 同値再帰型を有効にするコマンド *)
# let f x x = x x;;
val f : 'a -> ('b -> 'c as 'b) -> 'c = <fun>
# let f x = x::x;;
val f : ('a list as 'a) -> 'a list = <fun>
# let rec i = (i, i);;
val i : 'a * 'a as 'a =
  (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((...),
                                                                    (...)),
(何か良くわからない括弧の山)

このように弊害が大きいので、OCamlでも-rectypesはデフォルトではオフになっています。サブタイピングと組み合わせたとき、理論的な扱いがとても難しくなる（TAPLでも余帰納法を導入する等、そのあたりが一つの大きな山になっている。興味のある方はチャレンジしてみてください。）のも、あまり他の言語で実装されていない理由の一つのようです。

が、多相バリアントやオブジェクト型では -rectypes 無しでも同値再帰的な型付けになります。というか、同値再帰のおかげでこれらが有用になっている、言ってみればOCamlのひとつの神髄は同値再帰にあり、といっても過言ではない側面があります。それについてはまた。

*1:この翻訳チームによって"同値再帰型"という訳語が決まったようで(私の担当部分ではなかったけど)、今googleで調べてもこの私のブログしかヒットしない

第一級モジュールでジェネリックなSet操作

この記事は OCaml Advent Calendar 2012 の 8日目の記事です。

昨日のエントリでは無理矢理 'a t の形で扱える Setモジュールを作りましたが、これには欠点があり、 'a t型をもつ各集合で、'aの同値性の付け方が異なってしまいます。 昨日の記事に @garriguejej さんがコメントしたとおり、Setモジュールのバイナリメソッドunionやdiffなどは（各引数で'aの同値性が異なるかもしれず）使えないのです。
結局、集合の表現が 'a について同じ同値性をもつことを型で強制するには、Set.Makeをそのまま使うべき、ということですね。

では様々なSetについてジェネリックな関数はOCamlで書けないのでしょうか？ そんなことはないです。第一級モジュールがあればできます。

例

(* Setモジュールを第一級に *)
type ('t,'elt) set = (module Set.S with type t = 't and type elt = 'elt)

(* 
  多相なSet操作関数: 第一引数にどのSetに対する操作か指定する 
*)

(*
  val empty : ('a, 'b) set -> 'a
あるいは
  val empty : (module Set.S with type t = 'a and type elt = 'b) -> 'a
*)
let empty (type t) (type elt) ((module S) : (t,elt) set) = 
  S.empty

(*
  val add : ('a, 'b) set -> 'b -> 'a -> 'a
あるいは
  val add : (module Set.S with type t = 'a and type elt = 'b) -> 'b -> 'a -> 'a
*)
let add (type t) (type elt) ((module S) : (t,elt) set) =
  S.add

let singleton (type t) (type elt) ((module S) : (t,elt) set) =
  S.singleton

(* バイナリメソッドも定義できる *)
let union (type t) (type elt) ((module S) : (t,elt) set) =
  S.union

(* int,string の標準的な集合 *)
module IntSet = Set.Make (struct type t=int let compare = Pervasives.compare end)
module StrSet = Set.Make (struct type t=string let compare = Pervasives.compare end)

(* 比較関数が異なるIntSet *)
module IntSet2 = Set.Make (struct type t=int let compare x y = compare y x end)

let int : (IntSet.t,int) set = (module IntSet)
let int2 : (IntSet2.t,int) set = (module IntSet2)
let string : (StrSet.t,string) set = (module StrSet)

(* 
  使ってみよう
*)

let ia = singleton int 1
let ib = singleton int 2
let iab = union int ib ib

let sa = singleton string "a"
let sb = singleton string "b"
let sab = union string sa sb

(* 比較関数が異なると型エラー *)
let ic = singleton int2 3
(*
let iac = union int2 ia ic
Error: This expression has type IntSet.t
       but an expression was expected of type IntSet2.t
*)

これってどういうこと？

OCaml 3.11までは、Setについて多相な関数群を書く場合

module MySet(S:Set) = struct
  let empty = S.empty
end

と書いてSetモジュールを引数に取るfunctorを書いていたところを、

let empty (type t) (type elt) (module S : Set.S with type t = t and type elt = elt) = S.empty

などと、関数ごとにSetモジュールを受け取るように書き換えたのでした。 これが型の省略により

let empty (type t) (type elt) ((module S) : (t,elt) set) = S.empty

という記法になっているというお話です。
つまるところやってることはあまりfunctorと変わらないので、ここまでやるなら 素直にfunctor を使ったほうがいいかもしれませんね。

Haskell や Scala との比較

ところで

singleton int 1

のintは第一級モジュールの値を渡しているのですが、これは 型intの時に何をすべきかというディスパッチが書かれた辞書を渡しているようなものです。Haskellの型クラスで (Set s => Int -> s Int) 等と書くと、型推論により唯一のSetのインスタンスが決まるので暗黙にこのような辞書が渡されます。 Scalaなら implicit parameterで渡せますね。

この技が使えないとき

この方法は、 t や elt の型が 型引数を取る 'a t や 'a elt になった場合、破綻します。 たとえば モナドはこの方法では駄目で、詳しくは昨日のエントリからリンクした記事を読んでみてください。

第一級モジュールでSetの多相性を復活させてみよう

この記事は OCaml Advent Calendar 2012 の 7日目の記事です。

OCaml 3.12より導入され、4.00でさらに便利になった 第一級モジュール (First-class modules)を使った小技を紹介します。ある種の単相的に定義された抽象データ型(ADT)を多相的にするという技です。 (どこかで既出かも)

追記:

• OCamlのテストスイートに良く似たコードがありました。
• Higher Order Fun by MATÍAS GIOVANNINI では、似た技でモナドを表現しています。 @osiire と @camloeba 両氏のつぶやきも参考になります。 (thanks to @camloeba さん)
• 「Haskell では…なのに」 → 次の日のエントリを見て下さい

OCamlのStdlibのSetモジュールは、多相的ではありません。ここで多相的でないとは、集合の型が型パラメータを取らないことを言っています。例えば、Setを使う場合は Functorに比較関数を与え、集合の型に特化したモジュールを合成するのですが、

(* int用の順序 *)
module IntOrd = struct
  type t = int
  let compare = Pervasives.compare
end

(* intの集合のモジュール *)
module IntSet = Set.Make (IntOrd)

ここで合成された IntSet モジュールは、例えば add : int -> IntSet.t -> IntSet.t のように、集合の要素が IntSet.t という単相型になっています。つまり、様々な型の値の集合に対する操作を与えたい場合、お好みのSetモジュールを返すような別なFunctorを作ることになります。

本来、多相的に扱えそうなSetが、単相的になってしまう…モヤモヤしますね…

そこで、この単相的なSetを、OCaml3.12より導入されたFirst-class modules (第一級モジュール)を使い、多相的なSetにする方法を紹介します。

(Setモジュールが多相でない理由は、二項演算を効率よく実装するためだと考えられます。たとえば和集合を計算する場合、二つの木を連結する操作が必要になりますが、効率よく木を連結するにはそれぞれの木の順序付けが同一である必要があります。もし次の方法で集合を多相にした場合、引数に渡された二つの集合の順序付けが同じであることを保証できないため、和集合は一方に他方の要素を1つずつ追加して計算することになります。こればっかりはどうしようもありませんので、そのような効率は犠牲にすることにします。Batteriesには多相な集合を扱うPSetというモジュールもあります。追記: @garriguejej さんのコメントも参照)

モジュールのシグネチャ

type 'a t
(*空集合: 比較関数を与える*)
val empty : ('a -> 'a -> bool) -> 'a t
val is_empty : 'a t -> bool
val mem : 'a -> 'a t -> bool
val add : 'a -> 'a t -> 'a t
val singleton : ('a -> 'a -> bool) -> 'a -> 'a t
val remove : 'a -> 'a t -> 'a t
(* ... *)

普通の集合演算ですが、Functor版と異なり、集合を作る時に比較関数を決められるところが違います。

モジュールの実装

追記：@garriguejej さんによるコメントも参照

(* 1st class moduleに、モジュールとその値を包むための型 *)
module type MySet = sig
  module S : Set.S
  val set : S.t
end

(* 多相的な集合の型! First-class moduleを使い、要素の型はモジュール制約で多相に *)
type 'a t = (module MySet with type S.elt = 'a)

(*空集合をつくる. *)
(*(type s) は型束縛(locally abstract types)の構文であり、引数ではない.  empty:('a -> 'a -> bool) -> 'a t *)
let empty (type s) (cmp : s -> s -> int) : s t = 
  (* 比較関数から、ローカルモジュールとそのモジュールの空集合をつくる *)
  let module M = struct
    module S = Set.Make (struct type t = s let compare = cmp end)
    let set = S.empty
  end 
  in (module M : MySet with type S.elt = s) (* ローカルモジュールを1st-class module の値に *)

(*空集合か否か*)
(* is_empty (m:'a t) と書きたいところだが、1st-class moduleの型推論に関わるので、こう書く必要がある *)
(* これで is_empty の型はちゃんと 'a t -> bool になる *)
let is_empty (type s) (m:s t) = 
  let module M = (val m) in (* 1st-class module を開く*)
  M.S.is_empty M.set

let mem (type s) (v:s) (m:s t) = 
  let module M = (val m) in
  M.S.mem v M.set

let add (type s) (v:s) (m:s t) : s t = 
  let module M = (val m) in
  let module M' = struct (* 別のモジュールを作る *)
    module S = M.S
    let set = M.S.add v (M.set)
  end in (module M' : MySet with type S.elt = s)

(*...*)

まとめ

First-class moduleの使い道のひとつを紹介しました。ポイントは、単相なものから多相性を復活させる

type 'a t = (module MySet with type S.elt = 'a)

なる書き方ができることで、これはなかなか興味深いですね。

他にも色んなテクニックがありますので、皆さんもOCamlと第一級モジュールの世界をぜひ探検してみてください!