论文标题
类别分级的代数理论和效应处理者
Category-Graded Algebraic Theories and Effect Handlers
论文作者
论文摘要
我们基于代数理论的类别级扩展提供了效应系统Cateff，该分级扩展与类别级别的单调相对应。 Cateff具有类别级的操作和处理程序。 CATEFF的效果由分级类别的形态分级。评分形态代表依赖性或各种状态等效果的精细结构。 CATEFF中的处理人员被认为是类别毕业效应的实现。我们定义了类别级别的代数理论的概念，以提供Cateff的语义并证明合理性和充分性。我们还举例说明使用类别级别的效果来表示发送接收数据的协议。
We provide an effect system CatEff based on a category-graded extension of algebraic theories that correspond to category-graded monads. CatEff has category-graded operations and handlers. Effects in CatEff are graded by morphisms of the grading category. Grading morphisms represent fine structures of effects such as dependencies or sorts of states. Handlers in CatEff are regarded as an implementation of category-graded effects. We define the notion of category-graded algebraic theory to give semantics of CatEff and prove soundness and adequacy. We also give an example using category-graded effects to express protocols for sending receiving typed data.
