セッション型 on Haskell
セッション型は プロトコルを表現する型で， 15年くらい前から π計算の型理論の1つとして研究されてきました(文献リスト(一部))．並行・分散ソフトウェアの普及を鑑みるに，セッション型のような仕組みは次世代の型安全かつ表現力の高いプログラミングのための強力なツールとして役に立つと考えます．
しかしその直観的なわかりやすさにも関わらず，セッション型を提供しているプログラミング言語は皆無(おそらく…)です．
そこで，今 流行(?)の型レベル計算を駆使して Haskell にセッション型を導入してみました．
ダウンロード
晒してみる．
まだ α版 full-sessions ダウンロードページへ
セッション型の例
例として次のHaskellプログラムを与える． これは私の実装でちゃんと型がつく：
proc1 = ixdo k <- new forkIO (ixdo send k (12345::Int); str <- recv k; io (putStrLn str)) i <- recv k send k (show (i*10))
newは新しいチャネルを生成する．このチャネルでの通信は同期的であり，送信は相手が受信するまでブロックする．send k v はチャネルkを介した値vの送信， recv k はチャネルkを介した受信である． forkIO は新しいスレッドを開始する． ixdo は do記法の一種である．
このプログラムを実行すると，
123450
という結果が得られる．
上の例では，forkIO で分岐したスレッドが， Int型の値 12345 を送り，次に String型の値を受信する．一方，メインスレッドは 逆に Int型の値を受け取り，showで文字列表現に変換した String型の値を送信する．このような，状況に応じて異なる型を扱えるのがセッション型である．
このセッション型は，ある時点におけるプロトコルを表現する． 具体的には， send k (12345::Int) の直前では，チャネル k は セッション型 (Send Int (Recv String End)) をもつ． このsendの直後，recv k の直前 では，チャネル k は セッション型 (Recv String End) を持つ．ここで Send は送信を， Recv は受信を表す．
セッション型の性質
- チャネルは，正確に 2つのスレッドに所有されてから使われなければならない (チャネルは渡すこともできる)
- チャネルは，互いに セッション型がdualとなるように使わなければならない
1. により，たとえば
ixdo
k <- new
send k True
という式は拒否される (生成したチャネルが単一のスレッドにしか所有されないため)．
ixdo
k <- new
forkIO (send k True)
のようにして，2つのスレッドにチャネルが所有されるようにする．
2. により，たとえば
ixdo k <- new forkIO $ send k True send k True
という式は拒否される (sendとsendはdualでないため)．
このように，セッション型は2者間のチャネル通信に格段の柔軟さと安全性を両立する．
私の "セッション型 on Haskell" 基礎編
セッション型を Haskellの型レベル計算 で無理やり実現するにあたって， いくつかの型と型クラスを導入する．
(基礎1) indexed monad
私の実装は，indexed monad を使い，セッション型の制約がついた計算を表現する．
(indexed monad は， Hackage では category-extras の Control.Monad.Indexed で提供されている． が，べつに自分で実装してもよい)． indexed-monad は，例えばOlegさんの限定継続の実装でも使われている．
indexed monad は，(私の理解では) 事前条件と事後条件を持つモナドだ．モナドにおなじみのみなさんはindexed monadを表現した次の型クラスで何かわかるかもしれない：
class IxMonad m where (>>>=) :: m i j a -> (a -> m j k b) -> m i k b ireturn :: a -> m i i a
普通のMonadクラスの型構築子と比べて型パラメータが2つ増えていることに注目されたい． 型 m i j a において， iが事前条件，jが事後条件を表すパラメータで， (>>>=) の型は， m >>>= f のような計算において m の事後条件と f の事前条件が一致しなければならず，さらに合成された計算における 事前条件が >>>= の左手の事前条件と， 事後条件が 右手の事後条件と一致しなければならないことを表している．
私のセッション型の実装では，この indexed monad によって， 「ある時点」におけるチャネル群のセッション型を管理している．
また，上の例で使っている ixdo 記法は，プリプロセッサ ixdopp (Tovらの実装) により，次の通り indexed monad の計算に展開される．
proc1 = new >>>= \k -> forkIO (send k (12345::Int) >>= \_ -> recv k >>>= \str -> io (putStrLn str)) >>>= \_ -> recv k >>>= \i -> send k (show i)
(基礎2) Sessionモナド, 型環境と型レベルリスト
セッション型を扱う計算を表すモナドを Session モナドと名付けている． Session モナドは IOモナドのラッパーで，次の通り定義されている．
newtype Session ss tt a = Session (IO a)
セッションモナド Session ss tt a のパラメータ ss と tt は型レベルリストで，セッション型に関する整合条件を表す．
この型レベルリストは，次の型構築子で表現される：
-- |type-level list cons data (:|:) hd tl infixr 3 :|: -- |type-level list nil data Nil
この型レベルリストは，「どのチャネルがどのセッション型をもつか」を表している．たとえば， あるチャネルに対してInt型の値を送信する計算 m は次の型をもつ：
m :: Session (Send Int c:|:tt) (c:|:tt) ()
事前条件に セッション型 Send Int c が, 事後条件に セッション型(変数) c が現れ， この計算では あるチャネルに Int型の値が送信されることを示している．
(基礎3) チャネル型, 型レベル自然数
チャネルの型レベル表現として，型レベル自然数を用いる．
newtype Channel n = ...(MVarを使って適当に実装) -- |type-level peano number n+1 data S n -- |type-level peano number 0 data Z
チャネル型 Channel n における型パラメータn に型レベル自然数を埋め込む． 例えば型レベル表現0 を持つチャネルの型は Channel Z, 型レベル表現 n+2 を持つチャネルは 型 Channel (S (S n)) をもつ．
(基礎4) チャネルと型環境
チャネルとセッション型の対応付けは，
型レベル表現nのチャネルのセッション型 = 型レベルリストの後ろからn-1番目
という関係をもつ．後ろからn番目，を表現するために，次の型クラス Length を用いる．
class Length tt l | tt -> l (インスタンス略)
Length tt l は，型レベルリスト tt が長さ l を持つことを表現する．
例えば，チャネル k :: Length tt (S n) => Channel n があるとき， send k True :: Session (Send Bool c:|:tt) (c:|:tt) () のように型がつき，チャネル k は send k True で Bool型の値の送信に使われることを示している．
実践・セッション型推論
ためしてみよう
私のセッション型は， Haskellの型検査器, 例えば GHCi などで型推論させることができる(一部)．たとえば，上の例 proc1 は，次の(ような)型をもつ：
proc1 :: Length ss l => Session t ss (End :|: ss) ()
あまり型がおもしろくないのは，チャネルが既に2つのスレッドで占有されているため，それ以上使えないからである．
次の式の型を見てみよう：
proc2 = ixdo k <- new forkIO (send k 123) ireturn k
Main> :t proc2 proc2 :: (Length tt l, Num t) => Session tt (Cap Nil (Recv t End) :|: tt) (Channel l)
少し面白い型が出てきた．
この proc2 は， あるチャネルを生成して， そのチャネルに 整数値を送る．ここでのセッション型は Num t => Send t End である．
一方，計算の戻り値の型Length tt l => Channel l と，事後条件 (Cap Nil (Recv t' End) :|: tt) によって，この計算が返してくる チャネル k は Num t => Recv t End を満たすように使えばよいことがわかる．
この計算を実行してみよう．
Main> :t proc2 >>>= \k -> recv k >>>= \i -> io (print i) proc2 >>>= \k -> recv k >>>= \i -> io (print i) :: (Length ss1 l) => Session ss (Cap Nil End :|: ss) () Main> runS $ proc2 >>>= \k -> recv k >>>= \i -> io (print i) 123
よし！
他こんなこともできる
proc2 = ixdo k <- new forkIO (send k (123::Int)) ireturn k proc2' k = forkIO $ recv k >>>= \i -> io (print (i::Int)) proc3 = ixdo k <- proc2 k' <- proc2 k'' <- proc2 proc2' k proc2' k' proc2' k'' ireturn ()
Main> runS proc3 121132233
