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中的处理器被视为范畴分级效应的实现。我们定义了范畴分级代数理论的概念，为CatEff提供语义，并证明其可靠性与完备性。我们还通过一个使用范畴分级效应来表达类型化数据发送接收协议的实例进行了说明。