最強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は最強言語ということですね。