[−][src]Crate dialectic

Dialectic

dialectic (noun): The process of arriving at the truth by stating a thesis, developing a contradictory antithesis, and combining them into a coherent synthesis.

dialectic (crate): Zero-cost session types for asynchronous Rust.

When two concurrent processes communicate, it's good to give their messages types, which ensure every message is of an expected form.

Conventional types merely describe what is valid to communicate.
Session types describe when it is valid to communicate, and in what manner.

This crate provides a generic wrapper around almost any type of asynchronous channel that adds compile-time guarantees that a specified session protocol will not be violated by any code using the channel. Such a wrapped channel:

has zero runtime cost in time or memory;
is built on async/.await to allow integration with Rust's powerful async ecosystem;
gracefully handles runtime protocol violations, introducing no panics; and
allows for full duplex concurrent communication, if specified in its type, while preserving all the same session-type safety guarantees.

Together, these make Dialectic ideal for writing networked services that need to ensure high levels of availability and complex protocol correctness properties in the real world, where protocols might be violated and connections might be dropped.

What now?

If you are new to session types you might consider starting with the tutorial-style tour of the crate.
If you're familiar with session types, you might jump to the quick reference, then read more in the types module and the documentation for Chan.
If you want to integrate your own channel type with Dialectic, you need to implement the Transmit and Receive traits from the backend module.
Or, you can dive into the reference documentation...

Getting started

The first step to communicating is figuring out what you mean to say.

This crate provides a concise type-level language for expressing session types. The session type attached to a wrapped communications channel indicates precisely which actions are available for each end of the channel.

Let's write our first session type:

use dialectic::*;

type JustSendOneString = Send<String, End>;

This type specifies a very simple protocol: "send a string, then finish." The first argument to Send is the type sent, and the second is the rest of the protocol, which in this case is the empty protocol End.

Every session type has a Dual, which describes what the other end of the channel must do to follow the channel's protocol; if one end Sends, the other end must Recv:

assert_type_eq_all!(<Send<String, End> as Session>::Dual, Recv<String, End>);

Because many sessions end with either a Send or a Recv, their types can be abbreviated when the rest of the session is End:

assert_type_eq_all!(Send<String>, Send<String, End>);
assert_type_eq_all!(Recv<String>, Recv<String, End>);

Given a valid session type, we can wrap an underlying communications channel with it. Here, let's make two ends of a channel for playing out our JustSendOneString protocol.

In this case, we're using the mpsc backend Dialectic provides, which is built on tokio::sync::mpsc. However, the mechanism for wrapping underlying channels is extensible, meaning you can choose your own transport if you want.

use dialectic::backend::mpsc;

The static method channel is automatically defined for all valid session types (note: its corresponding trait NewSession needs to be in scope for it to be callable). It takes as input a closure that creates some underlying unidirectional transport channel, and creates a matched pair of bidirectional session-typed channels wrapping the underlying channel type.

let (c1, c2) = JustSendOneString::channel(|| mpsc::channel(1));

The types of c1 and c2 are inferred from the session type specified: c1's type corresponds to the given session type, and c2's type corresponds to its dual:

let _: Chan<mpsc::Sender, mpsc::Receiver, Send<String>> = c1;
let _: Chan<mpsc::Sender, mpsc::Receiver, Recv<String>> = c2;

Now that we have the two ends of a bidirectional session-typed channel, we can use them to concurrently enact the protocol specified by their type. In this case, we're going to run them in two parallel tokio tasks. However, Dialectic is generic over the underlying async runtime, provided the underlying transport channel is of a compatible type.

tokio::spawn(async move {
    c1.send("Hello, world!".to_string()).await?;
    Ok::<_, mpsc::Error>(())
});

let (greeting, c2) = c2.recv().await?;
assert_eq!(greeting, "Hello, world!");

🎉 Tada! We've just written an asynchronous session-typed program with Dialectic!

Moving forward

Almost every operation on a Chan:

is asynchronous due to the inherent asynchrony of the protocol,
is fallible to account for issues in the underlying transport channel,
and takes ownership of the Chan upon which it is invoked to enforce type correctness.

As a result, each invocation of an operation on a channel is usually followed by an .await?, and the result of each operation should usually be rebound via let to the same name as the original channel.

In this example, two interlocking threads collaborate to compute the parity of the length of the string "Hello, world!". Notice how each time a channel operation is invoked, its name is rebound to a new channel.

type ParityOfLength = Send<String, Recv<usize, Send<bool>>>;
let (c1, c2) = ParityOfLength::channel(|| mpsc::channel(1));

// The string whose length's parity we'll compute
let string = "Hello, world!".to_string();

// Send "Hello, world!", receive its length, then send its parity
let t1 = tokio::spawn(async move {
    // `send` returns the channel
    let c1 = c1.send(string).await?;

    // `recv` returns a pair of (received value, channel)
    let (len, c1) = c1.recv().await?;

    // `send` returns the channel
    let c1 = c1.send(len % 2 == 0).await?;

    Ok::<_, mpsc::Error>(())
});

// Receive a string, send its length, and receive its parity
let t2 = tokio::spawn(async move {
    // `recv` returns a pair of (received value, channel)
    let (string, c2) = c2.recv().await?;

    // `send` returns the channel
    let c2 = c2.send(string.chars().count()).await?;

    // `recv` returns a pair of (received value, channel)
    let (parity, c2) = c2.recv().await?;

    Ok::<_, mpsc::Error>(parity)
});

// Wait for the tasks to finish
t1.await??;
let parity = t2.await??;

// Check that the parity was correct
assert_eq!(parity, false);

Getting stopped

The most important benefit to session typing is not what it lets you do, but rather, what it prevents you from doing. Below are some things we can't do with our JustSendOneString channel from above:

type JustSendOneString = Send<String, End>;

Trying to do any of the below things results in a compile-time type error (edited for brevity).

If we try to send on the end of the channel that's meant to receive...

let (c1, c2) = JustSendOneString::channel(|| mpsc::channel(1));
c2.send("Hello, world!".to_string()).await?;

...we get an error telling us exactly that:

error[E0599]: no method named `send` found for struct `Chan<Sender, Receiver, Recv<String>>` in the current scope

If we try to receive the wrong type of thing...

let (c1, c2) = JustSendOneString::channel(|| mpsc::channel(1));
c1.send("Hello, world!".to_string()).await?;
let (n, c2): (i64, _) = c2.recv().await?;

...we get an error informing us so:

error[E0308]: try expression alternatives have incompatible types
   |
   | let (n, c2): (i64, _) = c2.recv().await?;
   |                         ^^^^^^^^^^^^^^^^ expected `i64`, found struct `String`

But the unique power session types bring to the table is enforcing the validity of sequences of messages. If we try to send twice in a row...

let (c1, c2) = JustSendOneString::channel(|| mpsc::channel(1));
let c1 = c1.send("Hello, world!".to_string()).await?;
c1.send("Hello again!".to_string()).await?;

...we get an error we saying the returned channel is now of type Chan<_, _, End>, and we can't send when it's the end:

error[E0599]: no method named `send` found for struct `Chan<Sender, Receiver, End>` in the current scope

Branching out

Most interesting protocols don't just consist of linear sequences of Sends and Recvs. Sometimes, one party offers the other a choice of different ways to proceed, and the other chooses which path to take.

In Dialectic, this possibility is represented by the Offer and Choose types. Each is parameterized by a tuple of session types representing, respectively, the choices offered by one end of the channel, or the choices available to choose from.

Offer is dual to Choose if the choices offered are dual to the choices available to choose from:

assert_type_eq_all!(
    <Offer<(Send<String>, Recv<i64>)> as Session>::Dual,
    Choose<(Recv<String>, Send<i64>)>,
);

Just as the send and recv methods enact the Send and Recv session types, the choose method and offer! macro enact the Choose and Offer session types.

Suppose we want to offer a choice between two protocols: either sending a single integer (Send<i64>) or receiving a string (Recv<String>). Correspondingly, the other end of the channel must indicate a choice of which protocol to follow -- and we need to handle the result of either selection by enacting the protocol chosen.

use dialectic::constants::*;

let (c1, c2) = <Offer<(Send<i64>, Recv<String>)>>::channel(|| mpsc::channel(1));

// Offer a choice
let t1 = tokio::spawn(async move {
    let c1 = offer!(c1 =>
        { c1.send(42).await? },  // handle `c2.choose(_0)`
        { c1.recv().await?.1 },  // handle `c2.choose(_1)`
    );
    Ok::<_, mpsc::Error>(())
});

// Make a choice
let t2 = tokio::spawn(async move {
    let c2 = c2.choose(_1).await?;            // select to `Send<String>`
    c2.send("Hi there!".to_string()).await?;  // enact the selected choice
    Ok::<_, mpsc::Error>(())
});

// Wait for the tasks to finish
t1.await??;
t2.await??;

In the above, we can see how the offer! macro takes the name of a channel (this must be an identifier, not an expression) and a list of expressions which may use that channel. In each expression, the channel's type corresponds to the session type for that choice. The type of each expression in the list must be the same, which means that if we want to bind a channel name to the result of the offer!, each expression must step the channel forward to an identical session type (in the case above, that's End).

Dually, to select an offered option, you can call the choose method on a channel, passing it as input a constant corresponding to the index of the choice. These constants are not Rust's built-in numeric types, but rather unary type-level numbers. Dialectic supports up to 128 possible choices in an Offer or Choose, and the corresponding constants _0, _1, _2, ... _127 are defined in the constants module.

Looping back

While some protocols can be described as a finite sequence of operations, many contain the possibility of loops. Consider things like retrying after an invalid response, sending an unbounded stream of messages, or providing a persistent connection for multiple queries. All these can be modeled with session types by introducing recursion.

Suppose we want to send a stream of as many integers as desired, then receive back their sum. We could describe this protocol using the Loop and Recur types:

type QuerySum = Loop<Choose<(Send<i64, Recur>, Recv<i64>)>>;

The dual to Loop<P> is Loop<P::Dual>, and the dual to Recur is Recur, so we know the other end of this channel will need to implement:

type ComputeSum = Loop<Offer<(Recv<i64, Recur>, Send<i64>)>>;
assert_type_eq_all!(<QuerySum as Session>::Dual, ComputeSum);

We can implement this protocol by following the session types. When the session type of a Chan hits a Recur point, it jumps back to the type of the Loop to which that Recur refers. In this case, for example, immediately after the querying task sends an integer, the resultant channel will have the session type Choose<(Send<i64, Recur>, Recv<i64>)> once more.

let (mut c1, mut c2) = QuerySum::channel(|| mpsc::channel(1));

// Sum all the numbers sent over the channel
tokio::spawn(async move {
    let mut sum = 0;
    let c2 = loop {
        c2 = offer!(c2 =>
            {
                let (n, c2) = c2.recv().await?;
                sum += n;
                c2
            },
            { break c2; },
        );
    };
    c2.send(sum).await?;
    Ok::<_, mpsc::Error>(())
});

// Send some numbers to be summed
for n in 0..=10 {
    c1 = c1.choose(_0).await?.send(n).await?;
}

// Get the sum
let (sum, c1) = c1.choose(_1).await?.recv().await?;
assert_eq!(sum, 55);

Notice: Whenever we loop over a channel, the channel itself needs to be declared mut. This is because each channel operation takes the channel as an owned value, returning a new channel. In order to repeat a loop, we need to re-assign to the channel at the end of the loop so that it is in scope for the next iteration.

Nested loops

If the protocol contains nested loops, you can specify which nested loop to continue with using the optional parameter of Recur. By default, Recur jumps to the innermost loop; however, Recur<_1> jumps to the second-innermost, Recur<_2> the third-innermost, etc. The types _0, _1, _2, etc. are defined in the unary::types module.

Automatic looping

You may have noticed how in the example above, choose can be called on c1 even though the outermost part of c1's session type QuerySum would seem not to begin with Choose. This is true in general: if the session type of a Chan either Loops or Recurs to a session type for which a given operation is valid, that operation is valid on the Chan. In the instance above, calling choose on a Chan with session type Loop<Choose<...>> works, no matter how many Loops enclose the Choose. Similarly, if a Chan's type is Recur, whatever operation would be valid for the session type at the start of the corresponding Loop is valid for that Chan.

This behavior is enabled by the Actionable trait, which defines what the next "real action" on a session type is. For End, Send, Recv, Offer, Choose, and Split (the final session type discussed below), the "real action" is that session type itself. However, for Loop and Recur, the next action is whatever follows entering the loop(s) or recurring, respectively.

In most uses of Dialectic, you won't need to directly care about the Actionable trait or most of the traits in types aside from Session. It's good to know what it's for, though, because that might help you understand an error message more thoroughly in the future!

Splitting off

Traditional presentations of session types do not allow the channel to be used concurrently to send and receive at the same time. Some protocols, however, can be made more efficient by executing certain portions of them in parallel.

Dialectic incorporates this option into its type system with the Split type. A channel with a session type of Split<P, Q> can be split into a send-only end with the session type P and a receive-only end with the session type Q, which can then be used concurrently. In the example below, the two ends of a channel concurrently swap a Vec<usize> and a String. If this example were run over a network and these values were large, this could represent a significant reduction in runtime.

type SwapVecString = Split<Send<Vec<usize>>, Recv<String>>;

The dual of Split<P, Q> is Split<Q::Dual, P::Dual>:

assert_type_eq_all!(
    <Split<Send<Vec<usize>>, Recv<String>> as Session>::Dual,
    Split<Send<String>, Recv<Vec<usize>>>,
);

Notice that P and Q switch places! This is because the left-hand P is always the send-only session, and the right-hand Q is always the receive-only session.

Now, let's use a channel of this session type to enact a concurrent swap:

let (c1, c2) = SwapVecString::channel(|| mpsc::channel(1));

// Spawn a thread to simultaneously send a `Vec<usize>` and receive a `String`:
let t1 = tokio::spawn(async move {
    // Split c1 into a send-only `tx` and receive-only `rx`
    let (tx, rx) = c1.split();

    // Concurrently send and receive
    let send_vec = tokio::spawn(async move {
        let tx = tx.send(vec![1, 2, 3, 4, 5]).await?;
        Ok::<_, mpsc::Error>(tx)
    });
    let recv_string = tokio::spawn(async move {
        let (string, rx) = rx.recv().await?;
        Ok::<_, mpsc::Error>((string, rx))
    });
    let tx = send_vec.await.unwrap()?;
    let (string, rx) = recv_string.await.unwrap()?;

    // Unsplit the ends of `c1`
    let c1 = Chan::unsplit(tx, rx).unwrap();

    Ok::<_, mpsc::Error>(string)
});

// Simultaneously *receive* a `Vec<usize>` *from*, and *send* a `String` *to*,
// the task above:
let (tx, rx) = c2.split();
let send_string = tokio::spawn(async move {
    let tx = tx.send("Hello!".to_string()).await?;
    Ok::<_, mpsc::Error>(tx)
});
let recv_vec = tokio::spawn(async move {
    let (vec, rx) = rx.recv().await?;
    Ok::<_, mpsc::Error>((vec, rx))
});

// Wait for the threads to finish
let tx = send_string.await??;
let (vec, rx) = recv_vec.await??;
let string = t1.await??;

// Unsplit the ends of `c2`
let c2 = Chan::unsplit(tx, rx).unwrap();

assert_eq!(vec, &[1, 2, 3, 4, 5]);
assert_eq!(string, "Hello!");

When using Split, keep in mind its limitations:

It's a type error to Send or Choose on the receive-only end.
It's a type error to Recv or Offer on the transmit-only end.
You can unsplit the two ends again only once their session types match each other.
It's a runtime UnsplitError to attempt to unsplit two Chans which did not originate from the same call to split, even if their types match.

Quick reference

The tutorial above covers all the constructs necessary to write session-typed programs with Dialectic. A quick summary:

To make a pair of dual Chans for a session type P: let (c1, c2) = P::channel(|| {...}) with some closure that builds a unidirectional underlying channel.
To wrap an existing sender tx and receiver rx in a single Chan for P: let c = P::wrap(tx, rx).

Once you've got a channel, here's what you can do:

Session Type	Channel Operation(s)	Dual Type
`Send<T, P = End>`	`let c = c.send(t: T).await?;`	`Recv<T, P::Dual>`
`Recv<T, P = End>`	`let (t, c) = c.recv().await?;`	`Send<T, P::Dual>`
`Choose<Choices>`	`let c = c.choose(_N).await?;`	`Offer<Choices::Dual>`
`Offer<Choices>`	`let c = offer!(c => {...}, ...);`	`Choose<Choices::Dual>`
`Split<P, Q>`	`let (tx, rx) = c.split();` `// concurrently use tx and rx` `let c = Chan::unsplit(tx, rx)?;`	`Split<Q::Dual, P::Dual>`
`Loop<P>`	(none)	`Loop<P::Dual>`
`Recur<N = Z>`	(none)	`Recur<N>`
`End`	`let (tx, rx) = c.close();`	`End`

Re-exports

pub use types::*;

Modules

backend	A `Chan<Tx, Rx, P, E>` is parameterized by its transmitting channel `Tx` and its receiving channel `Rx`. In order to use a `Chan` to run a session, these underlying channels must implement the traits `Transmit` and `Receive` for at least the types used in any given session (and in the case of `Transmit`, for the particular calling conventions used to pass those types to `Chan::send`).
types	The types in this module enumerate the shapes of all expressible sessions.

Macros

offer

Offer a set of different protocols, allowing the other side of the channel to choose with which one to proceed. This macro only works in a Try context, i.e. somewhere the ? operator would make sense to use.

Structs

Branches	The result of `offer`, `Branches<Tx, Rx, Ps>` represents an enumeration of the possible new channel states that could result from the offering of the type-level list of protocols `Ps`.
Chan	A bidirectional communications channel sending outgoing messages via the `Tx` connection and receiving incoming messages via the `Rx` connection, whose future session behavior is determined by the session type `P`. The `E` parameter is a type-level list describing the session environment of the channel: the stack of `Loop`s the channel has entered.
OutOfRangeChoice	An error representing a protocol violation where the other end of the channel has selected a choice whose index is too high to be handled by the current session type.
Unavailable	A placeholder for a missing transmit or receive end of a connection.
UnsplitError	The error returned when two channels cannot be `unsplit` together because they originate from different channels contains the two channels which couldn't be reunited.

Traits

NewSession

The NewSession extension trait gives methods to create session-typed channels from session types. These are implemented as static methods on the session type itself. For instance: