Label-Dependent Session Types

TL;DR

This paper introduces a simplified, label-dependent session type calculus with a single communication reduction, enabling more flexible protocol descriptions and integrating dependent types with linear typing.

Contribution

It presents a foundational session type calculus with label-dependent types, decoupling communication from data manipulation, and introduces type-level recursion for protocol behaviors.

Findings

Decouples communication from data manipulation in session types

Supports type-level recursion for protocol-dependent behaviors

Proves equivalence of algorithmic and declarative type checking

Abstract

Session types have emerged as a typing discipline for communication protocols. Existing calculi with session types come equipped with many different primitives that combine communication with the introduction or elimination of the transmitted value. We present a foundational session type calculus with a lightweight operational semantics. It fully decouples communication from the introduction and elimination of data and thus features a single communication reduction, which acts as a rendezvous between senders and receivers. We achieve this decoupling by introducing label-dependent session types, a minimalist value-dependent session type system with subtyping. The system is sufficiently powerful to simulate existing functional session type systems. Compared to such systems, label-dependent session types place fewer restrictions on the code. We further introduce primitive recursion over natural numbers at the type level, thus allowing to describe protocols whose behaviour depends on numbers exchanged in messages. An algorithmic type checking system is introduced and proved equivalent to its declarative counterpart. The new calculus showcases a novel lightweight integration of dependent types and linear typing, with has uses beyond session type systems.