Categorical Semantics of Higher-Order Message Passing
Robin Cockett, Melika Norouzbeygi
TL;DR
This work generalizes the categorical semantics of CaMPL by proving an equivalence between an $\mathbb{A}$-actegory with hom-objects and an $\mathbb{A}$-enriched category with copowers, extending Kelly–Janelidze’s closed, symmetric setting to the non-closed, non-symmetric case. The authors show how concurrent processes can be stored as sequential data via copowers, enabling higher-order message passing without duplicating resources, and provide detailed constructions of copowers, powers, and the required parametrized adjunctions. The results unify actegory-based and enrichment-based views, clarifying how to store and invoke concurrent processes within CaMPL’s sequential-concurrent duality. This foundational work supports the semantic foundation for higher-order message passing and informs potential implementations in CaMPL and related languages.
Abstract
The Categorical Message Passing Language (CaMPL) is a concurrent programming language with a categorical semantics based on a linear actegory. CaMPL has a sequential and a concurrent side. The sequential side is a functional-style programming language which has a linear actegorical action on the concurrent side to produce a semantics for message passing. Concurrent processes in CaMPL talk to each other along typed channels (or protocols). The typed channels of each CaMPL process are split into input and output polarity channels, allowing processes to be plugged together by connecting an output polarity channel of one process to an input polarity channel of another (provided the channels are of the same protocol). Channel polarities can be flipped input to output with a linear logic-style negation. A desirable feature of a concurrent message-passing language, such as CaMPL, is that it should support higher-order processes. This allows processes to be passed as first-class citizens between processes. While the ability to pass concurrent processes is already present in any closed linear type system-such as CaMPL's-supporting arbitrary recursive process definitions requires reusing passed processes. Concurrent resources in CaMPL cannot be duplicated, thus, passing processes as linear closures does not provide the required flexibility. Instead, processes must be passed as sequential data, and the concurrent side must be enriched in the sequential side. This paper concerns the categorical semantics that lets us store concurrent processes as sequential data and yet use them. Abstractly, this is given by the equivalence between an actegory with hom-objects and an enriched category with copowers. In the closed symmetric case, this was studied by Kelly and Janelidze. Here, we present the proof of this equivalence for the non-symmetric, non-closed case in detail.