Replicate, Reuse, Repeat: Capturing Non-Linear Communication via Session Types and Graded Modal Types

TL;DR

This paper introduces a type system combining session types with graded modal types to enable controlled non-linear communication patterns in concurrent programming, demonstrated in the Granule language.

Contribution

It extends session types with graded modal types to support non-linear behaviors while maintaining linear guarantees, a novel integration in type theory.

Findings

Enables controlled non-linear communication in session-typed systems

Demonstrates implementation in the Granule language

Provides formal guarantees for non-linear behaviors

Abstract

Session types provide guarantees about concurrent behaviour and can be understood through their correspondence with linear logic, with propositions as sessions and proofs as processes. However, a strictly linear setting is somewhat limiting, since there exist various useful patterns of communication that rely on non-linear behaviours. For example, shared channels provide a way to repeatedly spawn a process with binary communication along a fresh linear session-typed channel. Non-linearity can be introduced in a controlled way in programming through the general concept of graded modal types, which are a framework encompassing various kinds of coeffect typing (describing how computations make demands on their context). This paper shows how graded modal types can be leveraged alongside session types to enable various non-linear concurrency behaviours to be re-introduced in a precise manner in a type system with a linear basis. The ideas here are demonstrated using Granule, a functional programming language with linear, indexed, and graded modal types.