Soundness and completeness with respect to equational theories for programming languages are fundamental properties in the study of categorical semantics. However, completeness results have not been established for programming languages with algebraic effects and handlers, which raises a question of whether the commonly used models in the literature, i.e., free model monads generated from algebraic theories, are the only valid semantic models for effect handlers. In this paper, we show that this is not the case. We identify the precise characterizations of categorical models of effect handlers that allow us to establish soundness and completeness results with respect to a certain equational theory for effect handling constructs. Notably, this allows us to capture not only free monad models but also the CPS semantics for effect handlers as models of the calculus.

翻译：编程语言范畴语义研究中的基本性质是相对于方程理论的可靠性与完备性。然而，对于具备代数效应与处理器的编程语言，完备性结果尚未建立，这引发了一个疑问：文献中常用的模型（即由代数理论生成的自由模型单子）是否确实是效应处理器唯一有效的语义模型。本文证明事实并非如此。我们精确刻画了效应处理器范畴模型的特征，使得我们能够针对效应处理结构的特定方程理论建立可靠性与完备性结果。值得注意的是，这不仅使我们能够捕捉自由单子模型，还能将效应处理器的CPS语义纳入该演算的模型范畴。