Publikation
Powermonads and Tensors of Unranked Effects
Sergey Goncharov; Lutz Schröder
In: Martin Grohe (Hrsg.). Proceedings of the 26th Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE. IEEE Symposium on Logic in Computer Science (LICS-2011), June 21-24, Toronto, Ontario, Canada, IEEE Computer Society, 2011.
Zusammenfassung
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 arities,
these combinations need not in general exist. 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.