#session #types #async #channel #protocol


Transport-polymorphic, asynchronous session types for Rust

5 releases (3 breaking)

0.4.1 Apr 1, 2021
0.4.0 Apr 1, 2021
0.3.0 Feb 11, 2021
0.2.0 Jan 13, 2021
0.1.1 Dec 18, 2020

#717 in Asynchronous

Download history 32/week @ 2023-01-08 13/week @ 2023-01-15 34/week @ 2023-01-22 58/week @ 2023-01-29 21/week @ 2023-02-05 24/week @ 2023-02-12 48/week @ 2023-02-19 30/week @ 2023-03-05 8/week @ 2023-03-12 9/week @ 2023-03-19 18/week @ 2023-03-26 15/week @ 2023-04-02 27/week @ 2023-04-09 1/week @ 2023-04-16 3/week @ 2023-04-23

53 downloads per month
Used in 7 crates (6 directly)

MIT license

1.5K SLoC


Rust license: MIT crates.io docs.rs documentation

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:

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

What now?


~157K SLoC