Actegories, Copowers, and Higher-Order Message Passing Semantics

Abstract

In this paper we prove that giving a right actegory with hom-objects is equivalent to giving a right-enriched category with copowers. While this result is known in the closed symmetric setting, our contribution extends the equivalence to non-closed and non-symmetric monoidal bases. This generalization is motivated by the semantics of higher-order message passing in the Categorical Message Passing Language (CaMPL), a concurrent language whose semantics is given by a linear actegory. A desirable feature for this language is the support of higher-order processes: processes that are passed as first class citizens between processes. While this ability is already present in any closed linear type systems -- such as CaMPL's -- to support arbitrary recursive process definitions requires the ability to reuse passed processes. Concurrent resources in CaMPL, however, cannot be duplicated, thus, passing processes as linear closures does not provide the required flexibility. This means processes must be passed as sequential data and the concurrent side must be enriched in the sequential side, motivating the technical result of this paper.