Effective ATS:
セッション型チャネル:
概要入門

この記事では、セッション型に対する簡単な入門を示します。

セッション型チャネルの基礎

広義の用語では、(動的な)セッションとは2つの並行実行されたプロセスの間における相互作用の列です。 またセッション型とはそのような相互作用を特定する(もしくは分類する)型です。 例えば、2つのプロセス P と Q が双方向チャネルによって接続されていると仮定してみましょう。 P の視点から見ると、そのチャネルは次のような項の列によって特定できます:

typedef P_ssn = chsnd(int)::chsnd(int)::chrcv(bool)::chnil

これは、1つの整数が送信しと、もう1つの整数が送信し、真理値が受信し、そして最後にそのチャネルが閉じることを意味しています。 Q の視点から見ると、次の項の列によってそのチャネルが特定されるべきであることは明確です:

typedef Q_ssn = chrcv(int)::chrcv(int)::chsnd(bool)::chnil

これは前の項の列が行なっていたことと正確に対 (dual) になっていることを意味しています。 P を、サーバ Q へ2つの整数を送信し、Q から最初に送られた整数が二番目の整数より小さいかどうかに依存して真もしくは偽を受信するような、クライアントであると考えることもできます。

チャネルには2つの終点 (endpoints) があり: それは正の終端 (positive end) と負の終端 (negative end) です; サーバによって保持される終端は正であり、クライアントによって保持される終端は負です。 正のチャネルと負のチャネルを表わすような、2つの抽象型 chanpos と channeg をそれぞれ導入しましょう。 このとき正の(負の)チャネルは、チャネルの正の(負の)終端を参照しています:

absvtype chanpos(ssn:type) // absvtype means linear abstype in ATS
absvtype channeg(ssn:type) // absvtype means linear abstype in ATS

例えば、P によって保持されたチャネルの終端には型 channeg(Q_ssn) (channeg(P_ssn) ではありません) が割り当てられ、Q によって保持されたチャネルの終端には型 chanpos(Q_ssn) が割り当てられます。 セッション型の相互作用は、正の終端 (すなわちサーバになります) の観 (view) に基づいて与えられます。

チャネル上にデータを送る関数は次のような型になります:

//
fun
chanpos_send
  {a:vt0p}{ss:type}
(
  chp: !chanpos(chsnd(a)::ss) >> chanpos(ss), x: a
) : void // end-of-function
//
fun
channeg_recv
  {a:vt0p}{ss:type}
(
  chn: !channeg(chrcv(a)::ss) >> channeg(ss), x: a
) : void // end-of-function
//
overload channel_send with chanpos_send
overload channel_send with channeg_recv
//

chanpos_send は正のチャネルに値を送るための関数であり、channeg_recv は負のチャネルに値を送るための関数であることに注意してください。 便宜上、channel_send シンボルがこれらの2つの関数でオーバロードされています。

チャネル上に送信されたデータを受信する関数は次の型になります:

//
fun
chanpos_recv
  {a:vt0p}{ss:type}
  (!chanpos(chrcv(a)::ss) >> chanpos(ss)): a
//
fun
channeg_send
  {a:vt0p}{ss:type}
  (!channeg(chsnd(a)::ss) >> channeg(ss)): a
//
overload channel_recv with chanpos_recv
overload channel_recv with channeg_send
//

chanpos_recv は正のチャネルからの値の受信を表わし、channeg_send は負のチャネルからの値の受信を表わすことに注意してください。 便宜上、channel_recv シンボルがこれらの2つの関数でオーバロードされています。

チャネルを閉じる関数は次の型になりります:

//
fun
chanpos_nil_wait (chp: chanpos(chnil)): void
fun
channeg_nil_close (chn: channeg(chnil)): void
//
overload channel_close with chanpos_nil_wait
overload channel_close with channeg_nil_close
//

chanpos_nil_wait は正のチャネルを閉じ、channeg_nil_close は負のチャネルを閉じることに注意してください。 さらに具体的に言うと、チャネルの正の終端に chanpos_nil_wait を呼び出すと、同じチャネルの負の終端に channeg_nil_close を呼び出しによるメッセージの到着を待ち合わせます。 便宜上、channel_close シンボルがこれらの2つの関数でオーバロードされています。

送受信のための関数は同期もしくは非同期どちらの通信にも基づくことができます。 これらの関数呼び出しは呼び出し元のブロックを引き起すかもしれません。 例えば、channpos_recv 呼び出しは、その呼び出しが返す値がなければ、ブロックするでしょう。 非同期通信では、channpos_send 呼び出しは、バッファに空きがなければ、呼び出し元をブロックするかもしれなせん。

プロセス P と Q を表わすプログラムは次のように実装できます:

(* ****** ****** *)

fun
P (
  i1: int, i2: int
, chn: channeg(Q_ssn)
) : bool = lt where
{
  val () = channel_send(chn, i1)
  val () = channel_send(chn, i2)
  val lt = channel_recv(chn)
  val () = channel_close(chn)
}

(* ****** ****** *)

fun
Q (
  chp: chanpos(Q_ssn)
) : void =
{
  val i1 = channel_recv(chp)
  val i2 = channel_recv(chp)
  val () = channel_send(chp, i1 < i2)
  val () = channel_close(chp)
}

(* ****** ****** *)

しかしそもそもチャネルはどうやって作れば良いのでしょうか？ その答は分散プログラミングをどのようにサポートするかに依存しています。 例えば、チャネルの生成に次のような関数 channel_create を導入できるでしょう:

fun
channeg_create{ss:type}
  (fserv: chanpos(ss) -<lincloptr1> void): channeg(ss)

web-workerに基づいたセッション型チャネル

この記事の残りでは、web-workerに基づいて実装されたセッション型チャネルの具体例を示します。 web-workerに馴染みのない読者にとって、読む前に何らかのプログラミングの例を学ぶのは良いアイデアかもしれません。 本質的に、web-workerはメッセージパッシングによってウェブブラウザと通信する、バックグランド実行されたスレッドです。 次に示す ATS コードは (Patsopt と Atscc2js で) JS コードにコンパイルされ、ウェブブラウザ (クライアント) と web-worker (サーバ) で実行するように意図されています。 JS (より正確にはそのランタイム) はシングルスレッドなので、無期限に呼び出し元をブロックさせるような関数 (例: chanpos_recv) をサポートできません。 この問題に対処するために、継続渡し (CPS: Continuation-passing) スタイルのセッション型チャネルをプログラミングするためのインターフェイスを構築します。

はじめにチャネルを閉じる関数に割り当てられた型を見てみましょう:

//
vtypedef
chanpos_nil = chanpos(chnil)
vtypedef
channeg_nil = channeg(chnil)
//
fun chanpos1_close(chanpos_nil): void
fun channeg1_close(channeg_nil): void
//

次にチャネルに対する送受信を行なう関数に割り当てられた型を見てみましょう:

//
typedef
chpcont0(ss:type) = (chanpos(ss)) -<cloref1> void
typedef
chncont0(ss:type) = (channeg(ss)) -<cloref1> void
//
typedef
chpcont1(ss:type, a:t0p) = (chanpos(ss), a) -<cloref1> void
typedef
chncont1(ss:type, a:t0p) = (channeg(ss), a) -<cloref1> void
//
typedef chpcont0_nil = chpcont0(chnil)
typedef chncont0_nil = chncont0(chnil)
//
fun
chanpos1_send
  {a:t0p}{ss:type}
(
  chanpos(chsnd(a)::ss), x0: a, k0: chpcont0(ss)
) : void // end-of-fun
//
fun
chanpos1_recv
  {a:t0p}{ss:type}
(
  chanpos(chrcv(a)::ss), k0: chpcont1(ss, chmsg(a))
) : void // end-of-fun
//
fun
channeg1_recv
  {a:t0p}{ss:type}
(
  channeg(chrcv(a)::ss), x0: a, k0: chncont0(ss)
) : void // end-of-fun
//
fun
channeg1_send
  {a:t0p}{ss:type}
(
  channeg(chsnd(a)::ss), k0: chncont1(ss, chmsg(a))
) : void // end-of-fun
//

上記の関数 P と Q は次のように実装できます:

(* ****** ****** *)

fun
P (
  i1: int, i2: int
, chn: channeg(Q_ssn)
) : void = (
//
channeg1_recv
( chn, i1
, lam(chn) =>
  channeg1_recv
  ( chn, i2
  , lam(chn) =>
    channeg1_send
    ( chn
    , lam(chn, lt) => let
      val lt = chmsg_parse<bool>(lt)
      (*
      // Some code for processing [lt]
      *)
      in
        channeg1_close(chn)
      end
    )
  ) 
)
//
) (* end of [P] *)

(* ****** ****** *)

fun
Q (
  chp: chanpos(Q_ssn)
) : void = (
//
chanpos1_recv
( chp
, lam(chp, i1) => let
  val i1 = chmsg_parse<int>(i1) in
  chanpos1_recv
  ( chp
  , lam(chp, i2) => let
    val i2 = chmsg_parse<int>(i2) in
    chanpos1_send
    ( chp, i1 < i2
    , lam(chp) => chanpos1_close(chp)
    )
    end // end-of-let // end-of-lam
  )
  end // end-of-let // end-of-lam
)
//
) (* end of [Q] *)

(* ****** ****** *)

P と Q のコードを使った単純なデモが オンライン から入手できます。 このデモコードの全体は次の名前の4つのファイルから成り立ちます:

introxmpl1_demo.html
introxmpl1_prctl.sats
introxmpl1_client.dats
introxmpl1_server.dats