Algebraic operations and generic effects (Q1811033): Difference between revisions

\textit{E. Moggi} [in: Proc. LICS '89, IEEE Press, 14-23 and Inf. Comput. 93, 55-92 (1991; Zbl 0723.68073)] introduced the idea of giving a unified category-theoretic semantics for computational effects, modeling each of them in the Kleisli category of an appropriate strong monad on a base category with finite products. However, the calculus of Moggi's semantics models does not contain operations, the constructs that actually create the effects. In order to model constructive operations that arise in describing computational effects, the authors consider, given a complete and cocomplete symmetric monoidal closed category \({\mathcal V}\) and a symmetric monoidal \({\mathcal V}\)-category \({\mathcal C}\) with cotensors and a strong \({\mathcal V}\)-monad \(\mathbb{T}\) on \({\mathcal C}\), axioms under which an Ob \({\mathcal C}\)-indexed family of operations of the form \(\alpha_x: (\mathbb{T} x)^v\to(\mathbb{T} x)^w\) provides semantics for algebraic operations on the computational \(\lambda\)-calculus.