Logic of computational semi-effects and categorical gluing for equivariant functors

TL;DR

This paper develops a new logical and categorical framework for semi-effects in programming languages, using actegories and equivariant functors, extending Moggi's effects calculus with novel semantics and gluing techniques.

Contribution

It introduces a proof-theoretic reconstruction of Moggi's metalanguage, semantics via equivariant functors, and categorical gluing for semi-effects, generalizing previous models.

Findings

Semantic models are given by equivariant functors, including Freyd categories.

Categorical gluing along equivariant functors is established.

Logical predicates for the $ hd$-modality are derived and related to $ op op$-lifting.

Abstract

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 \emph{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.