Effective ATS:
セッション型チャネル:
セッションを合成しよう!

この記事では、既存のセッションを合成して新しいセッションを作るセッションコンビネータを示します。 この点では、セッションコンビネータは既存のパーサを合成して新しいパーサを作るパーサコンビネータと似ています。

CPS スタイルのセッション

次に示すのは、CPS スタイルのクロージャ関数として表わされたセッションです。 はじめに2つの抽象型を見てみましょう:

//
abstype chanpos_session(ss:type)
abstype channeg_session(ss:type)
//

実施には、抽象型 chanpos_session と channeg_session はそれぞれ chanpos_nullify と channeg_nullify として定義されます:

//
typedef
chanpos_nullify(ss:type) =
  (chanpos(ss), chpcont0_nil) -<cloref1> void
typedef
channeg_nullify(ss:type) =
  (channeg(ss), chncont0_nil) -<cloref1> void
//

型 chanpos_session(ss) のサーバセッションは、2つの引数として型 chanpos(ss) の正のチャネルと継続を取ります; そのセッションは正のチャネルを型 chanpos(chnil) に変化させて、それからそれを継続に渡します。 型 channeg_session(ss) のセーバセッションの意味は同様に解釈できるでしょう。

ここで、セッション型チャネルの 前の記事 におけるサーバプロセスの実装を思い出してみましょう:

//
typedef
Q_ssn =
chrcv(int)::chrcv(int)::chsnd(bool)::chnil
//
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] *)

Q に相当するサーバセッションは、サーバコンビネータを使うことで次のように実装できます:

//
overload :: with chanpos1_session_cons
//
fun
Q_session(): chanpos_session(Q_ssn) = let
//
val i1_ref = ref{int}(0)
val i2_ref = ref{int}(0)
//
val ss1 =
  chanpos1_session_recv<int>(lam(i) => i1_ref[] := i)
val ss2 =
  chanpos1_session_recv<int>(lam(i) => i2_ref[] := i)
val ss3 =
  chanpos1_session_send<bool>(lam() => i1_ref[] < i2_ref[])
//
in
  ss1 :: ss2 :: ss3 :: chanpos1_session_nil()
end // end of [Q_session]
//

セッションコンビネータ chanpos1_session_send は、継続にチャネルが渡される前に与えられた正のチャネルへメッセージを送信するだけの単一のアクションを持つセッションを作るために呼び出されます。 そのようなセッションをシングルトンセッションと呼ぶことにします。 同様に、セッションコンビネータ chanpos1_session_recv は、継続にチャネルが渡される前に正のチャネルからメッセージを受信するだけの単一のアクションを持つセッションを作るために呼び出されます。

//
fun{
a:t@ype
} chanpos1_session_send
  (cfun0(a)): chanpos_session(chsnd(a)::chnil)
fun{
a:t@ype
} chanpos1_session_recv
  (cfun1(a, void)): chanpos_session(chrcv(a)::chnil)
//

セッションコンビネータ chanpos1_session_nil と chanpos1_session_cons は次のような標準のコンストラクタになります:

//
fun
chanpos1_session_nil(): chanpos_session(chnil)
//
fun{}
chanpos1_session_cons
  {a:type}{ss:type}
(
  chanpos_session(chcons(a, chnil)), chanpos_session(ss)
) : chanpos_session(a::ss)
//

型の示すところでは、chanpos1_session_nil は空のセッションを作るために呼び出され、chanpos1_session_cons はシングルトンセッションと(一般の)セッションを合成するために呼び出されます。

Q_session を呼び出して構築されたセッションがどのように実行されるのか、introxmpl1_server.dats のコードを読んでください。 次のコードは、サーバセッション Q_session に対応するクライアントセッション P_session を実装しています:

//
fun
P_session
(
// argless
) : channeg_session(Q_ssn) = let
//
fun
theResult_process
  (lt: bool): void = let
  val () = Start_output("Session over!")
in
  theResult_set(if lt then "true" else "false")
end // end of [theResult_process]
//
val ss1 =
  channeg1_session_recv<int>(lam() => theArg1_get())
val ss2 =
  channeg1_session_recv<int>(lam() => theArg2_get())
val ss3 =
  channeg1_session_send<bool>(lam(lt) => theResult_process(lt))
//
in
  ss1 :: ss2 :: ss3 :: channeg1_session_nil((*void*))
end // end of [P_session]
//

けれども、P_session を呼び出して構築されたセッションは、GUI の課題を無視しているので、直接の使用には適しません。 GUI に関する課題の扱いの詳細については、introxmpl1_client.dats のコードを読んでください。

P_session と Q_session のコードに基づいた単純なデモが オンライン から入手できます。 このデモのコード全体は次の名前の4つのファイルから成っています:

introxmpl1.html
introxmpl1_prctl.sats
introxmpl1_client.dats
introxmpl1_server.dats

様々なセッションコンビネータ

セッションの合流: ssappend

2つのセッション型 ss1 と ss2 が与えられたとき、ssappend(ss1, ss2) は ss1 と ss2 の連結を表わすセッション型です。 サーバセッションとクライアントセッションを合成するためには、それぞれ次の関数 chanpos1_session_append と channeg1_session_append を呼び出します:

//
fun{}
chanpos1_session_append
  {ss1,ss2:type}
(
  ssp1: chanpos_session(ss1)
, ssp2: chanpos_session(ss2)
) : chanpos_session(ssappend(ss1, ss2))
//
fun{}
channeg1_session_append
  {ss1,ss2:type}
(
  ssn1: channeg_session(ss1)
, ssn2: channeg_session(ss2)
) : channeg_session(ssappend(ss1, ss2))
//

選択されたサーバセッション : sschoose_disj

2つのセッション型 ss0 と ss1 が与えられたとき、セッション型 sschoose_disj(ss0,ss1) は ss0 もしくは ss1 によって分類されるようなセッションを分類します; ss0 もしくは ss1 の選択はサーバによって決定されます。

選択されたクライアントセッション : sschoose_conj

2つのセッション型 ss0 と ss1 が与えられたとき、セッション型 sschoose_conj(ss0,ss1) は ss0 もしくは ss1 によって分類されるようなセッションを分類します; ss0 もしくは ss1 の選択はクライアントによって決定されます。

オプショナルなサーバセッション : ssoption_disj

セッション型 ss が与えられたとき、セッション型 ssoption_disj(ss) は sschoose_disj(ss, chnil) と本質的に同じです。

オプショナルなクライアントセッション : ssoption_conj

セッション型 ss が与えられたとき、セッション型 ssoption_conj(ss) は sschoose_conj(ss, chnil) と本質的に同じです。

繰り返されたサーバセッション : ssrepeat_disj

セッション型 ss が与えられたとき、セッション型 ssrepeat_disj(ss) はセッション ss を繰り返すようなセッションを分類します; 繰り返しが続くかどうかはサーバによって選択されます。

繰り返されたクライントセッション : ssrepeat_conj

セッション型 ss が与えられたとき、セッション型 ssrepeat_conj(ss) はセッション ss を繰り返すようなセッションを分類します; 繰り返しが続くかどうかはクライアントによって選択されます。

乗算テストのサービス

セッションコンビネータを使った典型的なデモとして、乗算を行なう能力をテストするサービスを次に示します。 このサービスを試すには ここ をクリックしてください。

ログインセッション

このサービスを使うためには、最初にログインする必要があります。 ログインセッションを分類するセンション型は次のようになります:

typedef
ss_login = chrcv(string)::ss_pass_try

typedef
ss_pass =
chrcv(string)::chsnd(bool)::chnil
typedef
ss_pass_try = ssrepeat_disj(ss_pass)

応答チェックセッション

受信した与えらえた質問への応答をチェックするのは、本質的にパスワードチェックと同じです。 セッション型 ss_answer_try は次のようなセッションです:

typedef
ss_answer =
chrcv(int)::chsnd(bool)::chnil
typedef
ss_answer_try = ssrepeat_disj(ss_answer)

1つのテストを表わすセッション

一度のテスト試行を表わすセッション型は次のようになります:

typedef
ss_test_one =
chsnd(int)::chsnd(int)::ss_answer_try

繰り返されたテストを表わすセッション

テスト試行の繰り返しを表わすセッション型は次のようになります:

typedef
ss_test_loop = ssrepeat_conj(ss_test_one)

乗算テストのセッション

最後に、全体のセッションを表わすセッション型 ss_multest は次のようになります:

typedef
ss_multest =
ssappend(ss_login, ss_test_loop_opt)

typedef
ss_test_loop_opt = ssoption_disj(ss_test_loop)

状態を取り回すセッションを実装する

状態を取り回すセッションは (ひょっとすると伸縮する) 可変のフィールドを持つレコードとして表わされる状態を取り回します。 そしてその取り回された状態はセッションの実行中に更新されることを意図しています。 次に具体例を見てみましょう:

extern
fun
f_ss_pass
  (state: state)
: chanpos_session(ss_pass)
//
implement
f_ss_pass
  (state) = let
//
val
pass = ref{string}("")
//
fun
pass_check
(
  x: string
) : bool = passed where
{
//
val
passed = 
(
  if x = "multest" then true else false
) : bool
//
val ((*void*)) =
  if passed then state.pass_result(true)
//
} (* pass-check *)
//
typedef str = string
//
val ss1 =
  chanpos1_session_recv<str>(lam(x) => pass[] := x)
val ss2 =
  chanpos1_session_send<bool>(lam() => pass_check(pass[]))
//
in
  ss1 :: ss2 :: chanpos1_session_nil()
end // end of [f_ss_pass]

次の関数 f_ss_pass_try は f_ss_pass の上に構築されています:

extern
fun
f_ss_pass_try
  (state: state)
: chanpos_session(ss_pass_try)
implement
f_ss_pass_try
  (state) = let
//
val mtry = 3
val ntry = ref{int}(0)
//
val ((*void*)) =
  state.pass_result(false)
//
implement
chanpos1_repeat_disj$choose<>() = let
  val n0 = ntry[]
  val () = ntry[] := n0 + 1
in
//
if state.pass_result()
  then 0 else (if (n0 >= mtry) then 0 else 1)
//
end // end of [chanpos1_repeat_disj$choose]
//
in
  chanpos1_session_repeat_disj(f_ss_pass(state))
end // end of [f_ss_pass_try]

この デモ のコード全体は次の名前の4つのファイルから成ります:

multest.html
multest_prctl.sats // protocol
multest_client.dats // client-session
multest_server.dats // server-session

• Interface
• Implementation