Sessionモナドの読み方
初回に， Sessionモナドは indexed monad だと説明しましたが具体的にどういう制約が入っているのかをちゃんと説明しませんでした．
すべてを一度に説明するのは難しいのですが，とりあえずおおざっぱに説明を試みます
事前条件・事後条件 と プロトコルの差分
次の絵は， full-sessionsにおける Session t ss tt a という型*1をどう読むかを表している．
例えば Session t (Send Int (Recv String End):|:tt) (Recv String End:|:tt) a という型は，直前の計算が終了した時の(あるチャネルの)プロトコルが Send Int (Recv String End) であることを要求し，さらに，この計算の直後でプロトコルがRecv String Endであることを示している．このことから，この計算ではプロトコルの差分である Send Intを表す操作 ，即ち整数値の送信がおこることがわかる．
また，リストの残りの部分が変化していないことから，この計算では他のチャネルに対してはなにも操作しないことがわかる．
チャネルの生成
チャネルの生成により，事後条件のリストは事前条件のリストから1つ拡大される．例えば 次の図のように， Session t tt (Send Int End:|:tt) a という型は，まずチャネルを生成し，そして続きの計算に「Intを送信してチャネルを使うのをやめる」ことを要求している．これはすなわち，この計算の内部で 新しいスレッドが生成され，そこで Intを受信しようとしていることを示している．
例えば，次のプロセスpは，型 Session t (Send Int End:|:tt) tt () をもつ．
p = ixdo ch <- new forkIO (ixdo x <- recv; io (print (x+1::Int)))
