Crate session_types

session_types

This is an implementation of session types in Rust.

The channels in Rusts standard library are useful for a great many things, but they're restricted to a single type. Session types allows one to use a single channel for transferring values of different types, depending on the context in which it is used. Specifically, a session typed channel always carry a protocol, which dictates how communication is to take place.

For example, imagine that two threads, A and B want to communicate with the following pattern:

1. A sends an integer to B.
2. B sends a boolean to A depending on the integer received.

With session types, this could be done by sharing a single channel. From A's point of view, it would have the type int ! (bool ? eps) where t ! r is the protocol "send something of type t then proceed with protocol r", the protocol t ? r is "receive something of type t then proceed with protocol r, and eps is a special marker indicating the end of a communication session.

Our session type library allows the user to create channels that adhere to a specified protocol. For example, a channel like the above would have the type Chan<(), Send<i64, Recv<bool, Eps>>>, and the full program could look like this:

extern crate session_types;
use session_types::*;

type Server = Recv<i64, Send<bool, Eps>>;
type Client = Send<i64, Recv<bool, Eps>>;

fn srv(c: Chan<(), Server>) {
    let (c, n) = c.recv();
    if n % 2 == 0 {
        c.send(true).close()
    } else {
        c.send(false).close()
    }
}

fn cli(c: Chan<(), Client>) {
    let n = 42;
    let c = c.send(n);
    let (c, b) = c.recv();

    if b {
        println!("{} is even", n);
    } else {
        println!("{} is odd", n);
    }

    c.close();
}

fn main() {
    connect(srv, cli);
}

Re-exports

pub use Branch::*;

Macros

chan_select	This macro plays the same role as the select! macro does for Receivers.
offer	This macro is convenient for server-like protocols of the form:
try_offer	Returns the channel unchanged on TryRecvError::Empty.

Structs

Chan	A session typed channel. P is the protocol and E is the environment, containing potential recursion targets
ChanSelect	Heterogeneous selection structure for channels
Choose	Active choice between P and Q
Eps	End of communication session (epsilon)
Offer	Passive choice (offer) between P and Q
Rec	Enter a recursive environment
Recv	Receive A, then P
S	Peano numbers: Increment
Send	Send A, then P
Var	Recurse. N indicates how many layers of the recursive environment we recurse out of.
Z	Peano numbers: Zero

Enums

Branch

Traits

HasDual

The HasDual trait defines the dual relationship between protocols.

Functions

connect	Connect two functions using a session typed channel.
hselect	Homogeneous select. We have a vector of channels, all obeying the same protocol (and in the exact same point of the protocol), wait for one of them to receive. Removes the receiving channel from the vector and returns both the channel and the new vector.
iselect	An alternative version of homogeneous select, returning the index of the Chan that is ready to receive.
session_channel	Returns two session channels