In this article, I present several session combinators for combining existing sessions together to form new sessions. In this regard, session combinators are similar to parsing combinators, which combine existing parsers to form new parsers.
In the following presentation, sessions are represented as closure-functions in CPS-style. Let us first see two abstract types:
// abstype chanpos_session(ss:type) abstype channeg_session(ss:type) //
The abstract types chanpos_session and channeg_session are actually defined as chanpos_nullify and channeg_nullify, respectively:
// typedef chanpos_nullify(ss:type) = (chanpos(ss), chpcont0_nil) -<cloref1> void typedef channeg_nullify(ss:type) = (channeg(ss), chncont0_nil) -<cloref1> void //
A server-session of the type chanpos_session(ss) takes as its two arguments a positive channel of the type chanpos(ss) and a continuation; it turns the positive channel into one of the type chanpos(chnil) and then passes it to the continuation. The meaning of a client-session of the type channeg_session(ss) can be similarly construed.
Let us now recall the implementation of the server process in a previous article on session-typed channels:
// 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] *)
A server-session corresponding to Q can be implemented as follows by making use of certain session combinators:
// 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] //
The session combinator chanpos1_session_send is called to form a single-action session which only sends a message on a given positive channel before passing the channel to a continuation. Note that I may also refer to such a session as a singleton session. Similarly, the session combinator chanpos1_session_recv is called to form a single-action session which only receives a message on a given positive channel before passing the channel to a continuation.
// 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) //
The session combinators chanpos1_session_nil and chanpos1_session_cons should remind one of the standard list constructors:
// 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) //
As indicated by the types, chanpos1_session_nil is called to form an empty session and chanpos1_session_cons to combine a singleton session with a (general) session.
Please study the code in introxmpl1_server.dats to see how the session constructed by calling Q_session can be executed. The following code implements a client-session P_session that corresponds to the server-session Q_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] //
However, the session constructed by calling P_session is not suitable for being used directly as it ignores GUI issues. Please study the code in introxmpl1_client.dats for details on handling GUI issues.
A simple demo based on the code for P_session and Q_session is available on-line. The entirety of the code for this demo can be found in four files of the following names:
introxmpl1.html introxmpl1_prctl.sats introxmpl1_client.dats introxmpl1_server.datsI strongly encourage the reader to use the provided Makefile to build the demo on his/her own.
Given two session types ss1 and ss2, ssappend(ss1, ss2) is a session type for specifying a session that is the concatenation of one specified by ss1 and another one by ss2. The following functions chanpos1_session_append and channeg1_session_append can be called to join server-sessions and client-sessions, respectively:
// 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)) //
Given two session types ss0 and ss1 the session type sschoose_disj(ss0,ss1) is for classifying a session that can behave like one classified by either ss0 or ss1; the choice as to whether it is classified by ss0 or ss1 is determined by the server.
Given two session types ss0 and ss1 the session type sschoose_conj(ss0,ss1) is for classifying a session that can behave like one classified by either ss0 or ss1; the choice as to whether it is classified by ss0 or ss1 is determined by the client.
Given a session type ss, the session type ssoption_disj(ss) is essentially the same as sschoose_disj(ss, chnil).
Given a session type ss, the session type ssoption_conj(ss) is essentially the same as sschoose_conj(ss, chnil).
Given a session type ss, the session type ssrepeat_disj(ss) is for classifying one that repeats a session classified by ss; the choice is made by the server as to whether repetition should continue.
Given a session type ss, the session type ssrepeat_conj(ss) is for classifying one that repeats a session classified by ss; the choice is made by the client as to whether repetition should continue.
As an example for demonstrating certain typical use of session combinators, I present as follows the construction of a service for testing one's ability to do multiplication mentally. Please click here to give the service a try.
To use the service, one needs to first perform login. The session type for classifying the login session is given as follows:
typedef ss_login = chrcv(string)::ss_pass_trywhere the session type ss_pass_try is defined below:
typedef ss_pass = chrcv(string)::chsnd(bool)::chnil typedef ss_pass_try = ssrepeat_disj(ss_pass)During the login session, the server receives a string (representing the ID of the user) and enters a session for password-checking; one round of password-checking involves receiving a string (password) from the user and sending the result of checking to the user; the service may initiate another round of password-checking if the current round fails (that is, the boolean value false is sent to the user).
Checking the received answer to a given question is essentially the same as password-checking, and the session type ss_answer_try is for classifying such a session is given as follows:
typedef ss_answer = chrcv(int)::chsnd(bool)::chnil typedef ss_answer_try = ssrepeat_disj(ss_answer)Like password-checking, the server may request the user to send another answer if the current given answer is incorrect.
The session type for a single round of test is given as follows:
typedef ss_test_one = chsnd(int)::chsnd(int)::ss_answer_tryEssentially, the server sends two integers (generated randomly) to the client and then enters the answer-checking session described above.
The session type for repeated rounds of tests is given as follows:
typedef ss_test_loop = ssrepeat_conj(ss_test_one)Notice that the client decides whether a fresh round of test should take place.
Finally, the session type ss_multest for the overall session is given as follows:
typedef ss_multest = ssappend(ss_login, ss_test_loop_opt)where the session type ss_test_loop_opt (for a server-optional session) is given below:
typedef ss_test_loop_opt = ssoption_disj(ss_test_loop)Essentially, the overall session starts with the login session described above; whether the session for repeated tests follows depends on whether the login session succeeds or fails.
A state-carrying session carries a state represented as a (possibly extensible) record with mutable fields, and the carried state is meant to be updated during the execution of the session. Let us see a concrete example given as follows:
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]Applying to a state (which is just a reference to a record), the function f_ss_pass returns a state-carrying server-session classified by the session type ss_pass. Note that pass_check sets the field pass_result of the carried state to true if the received password passes checking.
The following function f_ss_pass_try builds on the top of 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]The session returned by a call to f_ss_pass_try allows the client to try at most 3 times to supply a valid password. Note that the function template chanpos1_repeat_disj$choose is called inside the session combinator chanpos1_session_repeat_disj to determine whether the given session needs to be repeated.
The entire code for this demo can be found in four files of the following names:
multest.html multest_prctl.sats // protocol multest_client.dats // client-session multest_server.dats // server-sessionThe implementation of server-session in multest_server.dats is largely straightforward while the implementation of client-session in multest_client.dats is more involved due to the need for handling certain GUI issues. For those interested in studying session types and session combinators in more depth, the following links should be helpful: Naturally, one should expect that session combinators can be further lifted to higher forms of combinators (e.g., those for combining services together conveniently).
This article is written by Hongwei Xi.