Effective ATS:
Session-typed Channels:
A Brief Introduction

In this article, I present a brief introduction to session types.

Basics on session-typed channels

In broad terms, a (dyadic) session is a sequence of interactions between two concurrently running processes, and a session type is a form of type for specifying (or classifying) such interactions. As an example, let us assume that two processes P and Q are connected via a bidirectional channel. From the perspective of P, the channel may be specified by a term sequence of the following form:

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

which means that an integer is to be sent, another integer is to be sent, a boolean is to be received, and finally the channel is to be closed. Clearly, from the perspective of Q, the channel should be specified by the following term sequence:

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

which means precisely the dual of what the previous term sequence does. We may think of P as a client who sends two integers to the server Q and then receives from Q either true or false depending on whether or not the first sent integer is less than the second one.

There are two endpoints in a channel: a positive end and a negative end; the end held by the server is positive and the end held by the client is negative. We introduce two abstract types chanpos and channeg for positive channels and negative channels, respectively, where a positive (negative) channel refers to the positive (negative) end of a channel:

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

For instance, the end of the channel held by P is assigned the type channeg(Q_ssn) (not channeg(P_ssn)) and the end of the channel held by Q is assigned the type chanpos(Q_ssn). So the interpretation of a session type is given based on the view of the positive end (that is, the server).

The functions for sending data on channels are given the following types:

//
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
//

Note that chanpos_send is for sending a value on a positive channel while channeg_recv is for sending a value on a negative channel. For convenience, the symbol channel_send is overloaded with both of these functions.

The functions for receiving data sent on channels are given the following types:

//
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
//

Note that chanpos_recv is for receiving a value on a positive channel while channeg_send is for receiving a value on a negative channel. For convenience, the symbol channel_recv is overloaded with both of these functions.

The functions for closing channels are given the following types:

//
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
//

Note that chanpos_nil_wait is for closing a positive channel while channeg_nil_close is for closing a negative channel. More specifically, a call to chanpos_nil_wait on (the positive end of) a channel waits until a message sent by a call to channeg_nil_close on (the negative end of) the same channel arrives. For convenience, the symbol channel_close is overloaded with both of these functions.

The functions for sending and receiving can be based on either synchronous or asynchronous communication. Calling these functions may result in the caller to be blocked. For instance, calling channpos_recv blocks the caller if there is no value available for the call to return. For asynchronous communication, calling channpos_send may block the caller if there is no more room available for buffering.

The programs for the processes P and Q can be implemented as follows:

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

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)
}

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

But how a channel can be created in the first place? The answer to this question depends on the underlying support for distributed programming. For instance, we may be able to introduce the following function channel_create for creating a channel:

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

The basic idea here is to spawn a thread (by executing the linear closure-function fserv) that works on the postive end of the newly created channel and then returns the negative end of the channel to the caller.

Session-typed channels based on web-workers

In the rest of this article, I will give a concrete presentation of session-typed channels that are implemented based on web-workers. For those who are not yet familiar with web-workers, it can be a good idea to first study some programming examples involving them before reading on. Essentially, a web-worker is a thread running in the background that can communicate with the browser via message-passing. The ATS code presented as follows is intended to be compiled into JS code (via Patsopt and Atscc2js) for running in the browser (client) and a web-worker (server). As JS (or, more precisely, its run-time) is single-threaded, we cannot support a function (e.g., chanpos_recv) that may block its caller indefinitely. We address this issue by building an interface for programming session-typed channels that is of CPS-style (where CPS stands for continuation-passing style).

Let us first see the types assigned to the functions for closing channels:

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

Clearly, everything is standard here, and there is really no surprise at all.

Let us next see the types assigned to the functions for sending and receiving on channels:

//
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
//

Given a type T, the type chmsg(T) is for the marshalled representation of a value of the type T. The type assigned to the function chanpos1_send indicates that the function takes three arguments: a positive channel, a value (to be sent), and a continuation; the channel is passed to the continuation after the value is sent onto the channel. Also, the type assigned to the function chanpos1_recv indicates that the function takes two arguments: a positive channel and a continuation; the channel and the marshalled representation of a value are passed to the continutation after the representation is received. The types assigned to the functions channeg1_send and channeg1_recv can be explained similarly.

The above functions P and Q can now be implemented as follows:

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

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] *)

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

Note that chmsg_parse is a function template for unmarshalling: It is called to turn the marshalled representation of a value into the value itself.

A simple demo based on the code for P and Q is available on-line. The entirety of the code for this demo can be found in four files of the following names:

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

In the file introxmpl1_prctl.sats, the protocol for communincations between the client (browser) and the server (web-worker) is formally represented as a session type. As can be expected, this file is statically loaded in both introxmpl1_client.dats and introxmpl1_server.dats. The client code (in introxmpl1_client.dats) is based on the code for P but contains various significant modifications, and it makes use of Bacon.js in its handling GUI issues. On the other hand, the server code (in introxmpl1_client.dats) is directly based on the code for Q with virtually no modifications. I strongly encourage the reader to use the provided Makefile to build the demo on his/her own.

This article is written by Hongwei Xi.

Effective ATS: Session-typed Channels: A Brief Introduction

Basics on session-typed channels

Session-typed channels based on web-workers

Effective ATS:
Session-typed Channels:
A Brief Introduction