セッション型のduality
セッション型の読み方について説明します．
セッション型の種類
私のfull-sessionsにおけるセッション型を次のTable 2に示す：
セッション型は論文によって表記法が著しく異なるが，多かれ少なかれだいたいここで示した機能(と再帰)がすべてである．
- Send / Recvは送信 / 受信である．
- Selectで表される内部選択は，前回説明した sel1 と sel2 のように，プロセスが自発的に行う選択である．
- Offerで表される外部選択は，前回説明した offer のように，プロセスが通信相手の選択に従い分岐する種類の選択である．
- Throw/Catch は，チャネル渡しのプロトコルを表現する．型には渡されるチャネルのプロトコルを書く．
- End は通信の終了を表す．
例えば (Send Int End) は Int を送信し終了するプロトコルを表す．
