2020/07/09 by Yuichi Nishiwaki, Nishiwaki, Yuichi, Toshiya Asai +1
Computer Science · Mathematics · #FOS: Computer and information sciences #Homotopy and Cohomology in Algebraic Topology #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2007.04621
openalex publication_date 2020/07/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In this paper, we revisit Moggi's celebrated calculus of computational effects from the perspective of logic of monoidal action (actegory). Our development takes the following steps. Firstly, we perform proof-theoretic reconstruction of Moggi's computational metalanguage and obtain a type theory with a modal type \rhd as a refinement. Through the proposition-as-type paradigm, its logic can be seen as a decomposition of lax logic via Benton's adjoint calculus. This calculus models as a programming language a weaker version of effects, which we call semi-effects. Secondly, we give its semantics using actegories and equivariant functors. Compared to previous studies of effects and actegories, our approach is more general in that models are directly given by equivariant functors, which include Freyd categories (hence strong monads) as a special case. Thirdly, we show that categorical gluing along equivariant functors is possible and derive logical predicates for \rhd-modality. We also show that this gluing, under a natural assumption, gives rise to logical predicates that coincide with those derived by Katsumata's categorical \top\top-lifting for Moggi's metalanguage.