In this work, we present Global Protocol Combinators (GPC), a shallow embedding of multiparty session types (MPSTs) into a minimal functional programming language, OCaml^M, with support for channel-based concurrency, structural subtyping and equi-recursive types. GPC has the following ingredients: (1) global combinators -- a set of statically typed primitives for writing global protocol; (2) translation from global combinators to channel vectors -- a structured sequence of simply-typed i/o channels; and (3) a local calculus for programming message-passing computation. We prove that our language for global combinators is type-safe. We show a behaviour-preserving encoding of MPSTs to OCaml^M and establish an operational correspondence between well-formed multiparty global protocols and well-typed global combinators.
Our implementation in OCaml is the first fully-static MPST implementation with support for session delegation. It safely (without explicit casts) realises multiparty communication over simply-typed i/o channels, preserving the order of interactions. We demonstrate global combinators on a plethora of examples. Our evaluation shows that global combinators are more efficient (in terms of runtime performance), lightweight (no external verification tools are necessary) and more expressive (supports full-merging) than existing implementations.
Cornwallis South West,
University of Kent,