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.
翻译:我们提出了一种效应系统CatEff,该系统基于对应范畴分级单子的代数理论的范畴分级扩展。CatEff包含范畴分级的操作与处理器。其中,效应通过分级范畴的态射进行分级,这些分级态射可表征效应的精细结构,如依赖关系或状态类型。CatEff中的处理器被视作范畴分级效应的具体实现方案。我们定义了范畴分级代数理论的概念以建立CatEff的语义,并证明了其可靠性和完备性。同时,通过使用范畴分级效应表达收发类型化数据的协议,给出了具体示例。