Exceptions and Session Types

The paper "Exceptional Asynchronous Session Types: Session Types without Tiers" (http://simonjf.com/drafts/zap.pdf) explains an exception handling mechanism which is safe in the presence of linear session channels. As of version 0.7.2, this is included in Links.

The key idea is to add three new constructs:

• raise raises an exception
• try L as x in M otherwise N evaluates L, binding the result to x in M if successful, and evaluating N if not
• cancel M allows consumption of a linear session channel endpoint

The system works by a notion of "channel cancellation" -- that is, channels that are either discarded explicitly through a use of cancel or implicitly through being in the aborted continuation when an exception is raised, are marked as cancelled. When their peer endpoint attempts to perform an action that wouldn't succeed (for example, receiving from an empty buffer, where the peer endpoint is offline), then an exception is raised.

As an example, consider:

fun go() {
  try {
    var t = fork (fun (s) { cancel(s) });
    var (res, _) = receive(t);
    res
  } as (x) in {
    "result: " ^^ intToString(x)
  } otherwise {
    "exception"
  }
}

go()

The send endpoint s is cancelled. Thus, receiving from its peer would block forever. However, with this extension, an exception would be raised and "exception" would be printed.

The extension is implemented both on the client and on the server.

The extension is off by default, but can be enabled by using the --session-exceptions flag, or setting session_exceptions=true in the config file. Note that since session exceptions make use of the work on handlers for algebraic effects, enable_handlers must also be set to true.