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.
翻译:本文证明了给定一个具有同态对象的右作用范畴等价于给定一个具有幂运算的右富集范畴。尽管该结果在闭对称情形下已知,我们的贡献在于将这一等价关系推广至非闭与非对称的幺半基范畴。这一推广的动机源于范畴消息传递语言(CaMPL)中高阶消息传递的语义,该并发语言的语义由线性作用范畴给出。该语言的一个理想特性是支持高阶进程:即作为一等公民在进程间传递的进程。虽然这种能力已存在于任何闭线性类型系统(例如CaMPL)中,但为了支持任意的递归进程定义,需要具备重用已传递进程的能力。然而,CaMPL中的并发资源不可复制,因此将进程作为线性闭包传递无法提供所需的灵活性。这意味着进程必须作为顺序数据传递,且并发端需在顺序端上富集,从而引出了本文的技术结果。