Categorical Message Passing Language (CaMPL) is a functional-style concurrent programming language whose semantics is in category theory, more specifically, linear actegories. Its core programming feature is message passing along typed communication channels between concurrent processes. CaMPL also supports controlled non-determinism via 'races' which allow processes to adapt dynamically while they are running, higher-order processes which pass other processes as messages, and custom channel datatypes called protocols and coprotocols which allow one to define infinite channel types or implement session types. The type system of CaMPL arises from a Curry-Howard-Lambek-like correspondence for concurrent programming, established by Cockett and Pastro in their paper titled "The logic of message passing". This type system ensures that a formal CaMPL program, i.e., one which does not allow general recursion, will never become deadlocked or livelocked. In this article, we explore the type system of CaMPL, custom channel types, and controlled non-determinism using code examples after briefly introducing its mathematical underpinnings.
翻译:范畴消息传递语言(CaMPL)是一种函数式风格的并发编程语言,其语义基于范畴论,更具体地说,基于线性作用范畴(linear actegories)。该语言的核心编程特性是并发进程之间通过类型化通信通道进行消息传递。CaMPL还通过“竞争”(races)支持受控的非确定性,允许进程在运行时动态调整;支持高阶进程,即能够将其他进程作为消息传递;并支持自定义通道数据类型(称为协议(protocols)与共协议(coprotocols)),从而可以定义无限通道类型或实现会话类型(session types)。CaMPL的类型系统源于Cockett与Pastro在论文《消息传递逻辑》中确立的类似于Curry-Howard-Lambek对应关系的并发编程逻辑框架。该类型系统确保形式化的CaMPL程序(即不允许一般递归的程序)永远不会陷入死锁或活锁。本文在简要介绍CaMPL的数学基础后,将通过代码示例探讨其类型系统、自定义通道类型以及受控非确定性。