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.

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

Quick reference

The tutorial 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).
• 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.

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

Session Type (S)	Channel Operation(s) (on a channel c: Chan<_, _, S, _>)	Dual Type (S::Dual)
Send<T, P = Done>	Given some t: T, returns a new c: let c = c.send(t).await?;	Recv<T, P::Dual>
Recv<T, P = Done>	Returns some t: T and a new c: let (t, c) = c.recv().await?;	Send<T, P::Dual>
Choose<Choices>	Given some _N < the length of Choices, returns a new c: let c = c.choose(_N).await?;	Offer<Choices::Dual>
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::Dual>
Split<P, Q>	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 Done: let (t, c) = c.split(|c| async move { ... }).await?;	Split<Q::Dual, P::Dual>
Loop<P>	Whatever operations are available for P	Loop<P::Dual>
Continue<N = Z>	Whatever operations are available for the start of the Nth-innermost Loop	Continue<N>
Break<N = Z>	• If exiting the outermost Loop: Returns the underlying Transmit/Receive ends: let (tx, rx) = c.close(); • If exiting an inner Loop: Whatever operations are available for the start of the (N + 1)th-innermost Loop	Break<N>
Seq<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.seq(|c| async move { ... }).await?;	Seq<P::Dual, Q::Dual>
Done	• If outside a Loop: Returns the underlying Transmit/Receive ends: let (tx, rx) = c.close(); • If inside a Loop, equivalent to Continue: whatever operations are available for the start of the innermost Loop	Done

Modules

backend	Transport backends for Chan, and the traits they implement in order to be used as such.
canonical	The CanonicalChan type is defined here. Typically, you don't need to import this module, and should use the Chan type synonym instead.
prelude	The prelude module for quickly getting started with Dialectic.
tutorial	The introductory tutorial for Dialectic (nothing is exported from this module).
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

Available	An available Transmit or Receive end of a connection.
Branches	The result of offer: an enumeration of the possible new channel states that could result from the offering of the tuple of protocols Choices.
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

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.

Type Definitions

Chan	A bidirectional communications channel using the session type P over the connections Tx and Rx.