Deadlock-Free Session Types in Linear Haskell

TL;DR

Priority Sesh is a Linear Haskell library that provides deadlock-free session-typed communication APIs, leveraging linear types for simplicity and safety, with options for tree-based or priority-based deadlock prevention.

Contribution

Introduces Priority Sesh, a session types library in Linear Haskell offering two deadlock-free APIs, one restricting process structure and another using priorities for cyclic structures.

Findings

Ensures deadlock freedom with tree-structured processes.

Allows cyclic structures using priority-based deadlock prevention.

Leverages Linear Haskell for idiomatic and simple session type code.

Abstract

Priority Sesh is a library for session-typed communication in Linear Haskell which offers strong compile-time correctness guarantees. Priority Sesh offers two deadlock-free APIs for session-typed communication. The first guarantees deadlock freedom by restricting the process structure to trees and forests. It is simple and composeable, but rules out cyclic structures. The second guarantees deadlock freedom via priorities, which allows the programmer to safely use cyclic structures as well. Our library relies on Linear Haskell to guarantee linearity, which leads to easy-to-write session types and highly idiomatic code, and lets us avoid the complex encodings of linearity in the Haskell type system that made previous libraries difficult to use.