⅋ — session types for Rust

Cheatsheet

Showcase example: Chat server

Features

• Specify full concurrent protocols — Sequencing, branching, recursion, higher-order patterns.
• Type-checked protocol adherence — Expectations delivered, obligations fulfilled.
• Deadlock freedom — Cyclic communication is statically ruled out.
• Multiple concurrent participants.
• Fits well with Rust's type system:
  • Use enums for making choices.
  • Use recursion on types for cyclic protocols.
• Built on top of async/.await. Runtime agnostic.
• Ergonomic design — eg. atm.choose(Operation::CheckBalance)
• Standard patterns in modules:
  • Queue — Transmit an arbitrary number of items in order.
  • Server — Handle a dynamic number of clients concurrently.
• No unsafe!
• Accessible documentation as a learning tool.

Introduction

What's a session type, anyway? It's a description an entire external behavior of a concurrent, message-passing process. From the first message, through every possible path and interaction that can be made with it, to all the ways it can finish.

When implementing a concurrent program according to a session type, the type tells what can happen at any point in the program. When we have to send a message, when to select a path to continue, when to wait for someone else to make a choice and adapt.

Crucially, the types are designed to provide some useful guarantees:

• Protocol adherence — Expectations delivered, obligations fulfilled.
• Deadlock freedom — Cyclic communication is statically ruled out.

Protocol adherence means that when interacting with a process described by a session type, we can be sure (unless it crashes) that it will behave according to the protocol specified by its type. There will no unexpected messages, nor forgotten obligations. Just like we can rely on a function to return a string if it says so, we can rely on a process to send a string if its specified anywhere within its session type.

Deadlock freedom means that deadlocks can't happen, without dirty tricks anyway. It is achieved by imposing a certain structure on how processes are connected. It can take a bit of getting used to, but it becomes very important when implementing very complex concurrent systems.

❓ Reading this, one may easily think, "I don't see deadlocks happen in practice...", and that's a valid objection! But it arises from our concurrent systems not being very complex due to a lack of tools and types to design and implement them reliably. At high levels of complexity, deadlocks become an issue, and having them ruled out proves crucial.

Using session types, complex concurrent systems can be modelled and implemented with confidence, as any type-checked program is guaranteed to adhere to its protocol, and avoid any deadlocks. Message passing itself ensures natural synchronization.

Lastly, session types give names to concurrent concepts and patterns, which enables high levels of abstraction and composability. That makes it easier to reason and talk about large concurrent systems.

📚 The particular flavor of session types presented here is a full implementation of propositional linear logic. However, no knowledge of linear logic is required to use or understand this library.

Continue reading the tutorial...

❤️ If you like what you see, and want to see more, consider sponsoring! It really helps with being able to do what I love, alongside navigating life.