Multiparty Session Typing, Embedded (Technical Report)

TL;DR

The paper addresses the challenge of safely and live MPST-checked concurrent programs when embedded into mainstream languages, focusing on a Scala-based internal DSL. It introduces mpst.embedded, leveraging Scala's match types to encode global types $G$ and local types $L$ as Scala types and to automatically perform projection and merging, avoiding external DSLs. The work claims to be the first internal-DSL MPST tool that supports the full MPST feature set, including $n$-ary choices and full merge, with compile-time checks ensuring runtime safety and liveness. Empirical evaluation shows practical type-check times across a benchmark suite, with and without consistency checks, and the artifact is available on Zenodo.

Abstract

Multiparty session typing (MPST) is a method to make concurrent programming simpler. The idea is to use type checking to automatically detect safety and liveness violations of implementations relative to specifications. In practice, the premier approach to combine MPST with mainstream languages -- in the absence of native support -- is based on external DSLs and associated tooling. In contrast, we study the question of how to support MPST by using internal DSLs. Answering this question positively, this paper presents the mpst.embedded library: it leverages Scala's lightweight form of dependent typing, called match types, to embed MPST directly into Scala. Our internal-DSL-based approach avoids programming friction and leaky abstractions of the external-DSL-based approach for MPST.

Figures (5)

• Figure 1: MPST
• Figure 2: Run 1
• Figure 3: Run 2
• Figure 4: Run 3
• Figure 5: A few possible runs of the Negotation protocol