Affine Sessions

TL;DR

This paper introduces 'affine sessions', relaxing linearity to affinity in session types, enabling better error handling while maintaining progress properties in concurrent communication protocols.

Contribution

It proposes a novel affine session type system that allows channels to exhibit at most the prescribed behavior, simplifying exception handling without losing progress guarantees.

Findings

Enhanced error handling mechanism integrated into session types.

Channels exhibit at most the behavior prescribed, ensuring safety.

Progress properties are preserved despite relaxed linearity.

Abstract

Session types describe the structure of communications implemented by channels. In particular, they prescribe the sequence of communications, whether they are input or output actions, and the type of value exchanged. Crucial to any language with session types is the notion of linearity, which is essential to ensure that channels exhibit the behaviour prescribed by their type without interference in the presence of concurrency. In this work we relax the condition of linearity to that of affinity, by which channels exhibit at most the behaviour prescribed by their types. This more liberal setting allows us to incorporate an elegant error handling mechanism which simplifies and improves related works on exceptions. Moreover, our treatment does not affect the progress properties of the language: sessions never get stuck.