Powermonads and Tensors of Unranked Effects

TL;DR

This paper investigates the combination of algebraic effects in programming semantics, introducing uniform effects and proving the existence of tensor combinations for effects like continuations and nondeterminism, enhancing modular language design.

Contribution

It introduces the class of uniform effects and proves tensor existence when combined with these effects, extending previous results to unbounded effects like continuations.

Findings

Tensor of effects exists if one component is uniform.

Characterization of effects where tensoring with nondeterminism is conservative.

Improved understanding of combining unbounded effects in semantics.

Abstract

In semantics and in programming practice, algebraic concepts such as monads or, essentially equivalently, (large) Lawvere theories are a well-established tool for modelling generic side-effects. An important issue in this context are combination mechanisms for such algebraic effects, which allow for the modular design of programming languages and verification logics. The most basic combination operators are sum and tensor: while the sum of effects is just their non-interacting union, the tensor imposes commutation of effects. However, for effects with unbounded arity, such as continuations or unbounded nondeterminism, it is not a priori clear whether these combinations actually exist in all cases. Here, we introduce the class of uniform effects, which includes unbounded nondeterminism and continuations, and prove that the tensor does always exist if one of the component effects is uniform, thus in particular improving on previous results on tensoring with continuations. We then treat the case of nondeterminism in more detail, and give an order-theoretic characterization of effects for which tensoring with nondeterminism is conservative, thus enabling nondeterministic arguments such as a generic version of the Fischer-Ladner encoding of control operators.