Crate 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): Transport-polymorphic 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 almost no 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;
• allows for full duplex concurrent communication, if specified in its type, while preserving all the same session-type safety guarantees; and
• can even implement context free sessions, a more general form of session type than supported by most other session typing libraries.

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.

Dialectic supports a number of async runtimes and backends out-of-the-box, if you don’t want to or don’t need to write your own:

• The dialectic-tokio-mpsc crate supports using Dialectic to communicate between tasks using Tokio’s mpsc queues.
• The dialectic-tokio-serde crate supports using Dialectic to communicate over any AsyncRead/AsyncWrite transport layer encoded using any Tokio codec. A couple of Serde formats are already implemented, but it is easy to implement your own:
  • dialectic-tokio-serde-bincode backend using bincode for serialization
  • dialectic-tokio-serde-json backend using serde_json for serialization

These crates also serve as good references for writing your own backends.

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 about the Session! macro for specifying session types, and continue on to look at the types module and the documentation for Chan.
• You may also find helpful the full self-contained examples, which show how all the features of the crate come together to build session-typed network programs.
• 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…

Quick reference

The prelude module exports most of the relevant constructs for writing programs with Dialectic. Most programs using Dialectic should use dialectic::prelude::*;.

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

• To specify a session type, use the Session! macro, which defines a domain-specific language for session types. It compiles to session types defined in the types module, which most users will never need to use directly.
• To construct a session-typed Chan, use the methods on the Session trait, such as Session::channel or Session::wrap, depending on whether you need to create both sides of a channel or just one side, respectively.
• Backend transports suitable for being wrapped in a Chan are provided in backend, along with the Transmit and Receive traits necessary to implement your own.
• When writing functions which are generic over their backend type, you will need to specify Transmit and Receive bounds on your backend. If you have a lot of these, the Transmitter and Receiver attribute macros can help eliminate them by letting you write them efficiently. All of the examples are written to be backend-agnostic, so taking a look at them may help if you get stuck.

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

Session! Macro Invocation	Session Type (S)	Channel Operation(s) (on a channel c: Chan<S, _, _>)	Dual Type (S::Dual)
send T; ...	Send<T, P>	Given some t: T, returns a new c: let c = c.send(t).await?;	Recv<T, P::Dual>
recv T; ...	Recv<T, P>	Returns some t: T and a new c: let (t, c) = c.recv().await?;	Send<T, P::Dual>
choose { 0 => ..., 1 => ..., ... }; ...	Choose<Choices>	Given some N < the length of Choices, returns a new c: let c = c.choose::<N>().await?;	Offer<Choices::Duals>
offer { 0 => ..., 1 => ..., ... }; ...	Offer<Choices>	Given a set of labeled branches N => ... in ascending order, exactly one for each option in the tuple Choices, returns a new c whose type each branch must match: let c = offer!(c => { 0 => ..., 1 => ..., ... });	Choose<Choices::Duals>
loop { ... }; ... or 'label: loop { ... }; ...	Loop<P>	Whatever operations are available for P	Loop<P::Dual>
continue; or continue 'label;	Continue<const N: usize>	Whatever operations are available for the start of the referred-to loop	Continue<N>
break; or break 'label;	Whatever follows the loop	Whatever operations are available after the end of the loop statement	The dual of whatever follows the loop
call { ... }; ... or call S; ...	Call<P, Q>	Given a closure evaluating the session type P to Done, returns a result and a channel for the type Q: let (t, c) = c.call(|c| async move { … }).await?;	Call<P::Dual, Q::Dual>
split { -> ..., <- ... }; ...	Split<P, Q, R>	Given a closure evaluating the session types P (send-only) and Q (receive-only) each to Done (potentially concurrently), returns a result and a channel for R: let (t, c) = c.split(|c| async move { … }).await?;	Split<Q::Dual, P::Dual, R::Dual>
(empty macro invocation)	Done	Closes the channel, dropping its receive/transmit ends: c.close();	Done

Modules

backend	The interface implemented by all transport backends for a Chan.
prelude	The prelude module for quickly getting started with Dialectic.
tuple	Conversions back and forth between flat tuples and their corresponding inductive list structures.
tutorial	The introductory tutorial for Dialectic (nothing is exported from this module).
types	The structs in this module enumerate the shapes of all expressible sessions.
unary	The unary numbers, represented by zero Z and successor S.

Macros

Session	The Session! macro compiles a small domain-specific language for describing session types into the types themselves. It should be invoked in type position.
offer	The offer! macro offers a set of different protocols, allowing the other side of the channel to choose with which one to proceed.

Structs

Branches	The result of offer: an N-ary enumeration of the possible Chans that could result from the what the other party chooses.
Chan	A bidirectional communications channel using the session type P over the connections Tx and Rx.
Over	The future returned by Session::over (see its documentation for details).
Unavailable	A placeholder for a missing Transmit or Receive end of a connection.

Enums

IncompleteHalf	A representation of what has gone wrong when a connection half Tx or Rx is incomplete.
SessionIncomplete	The error returned when a closure which is expected to complete a channel’s session fails to finish the session of the channel it is given.

Traits

Session

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

Attribute Macros

Receiver	In situations where the transmitting backend for a channel is generic, explicitly writing down all the trait bounds necessary to implement a protocol for that parameterized backend can be a lot of boilerplate. The Receiver attribute macro abbreviates these bounds by modifying the where clause of the item to which it is attached.
Transmitter	In situations where the transmitting backend for a channel is generic, explicitly writing down all the trait bounds necessary to implement a protocol for that parameterized backend can be a lot of boilerplate. The Transmitter attribute macro abbreviates these bounds by modifying the where clause of the item to which it is attached.