TY - GEN
T1 - Powermonads and tensors of unranked effects
AU - Goncharov, Sergey
AU - Schröder, Lutz
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=80052143269&partnerID=8YFLogxK
U2 - 10.1109/LICS.2011.34
DO - 10.1109/LICS.2011.34
M3 - Conference contribution
AN - SCOPUS:80052143269
SN - 9780769544120
T3 - Proceedings - Symposium on Logic in Computer Science
SP - 227
EP - 236
BT - Proceedings - 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011
T2 - 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011
Y2 - 21 June 2011 through 24 June 2011
ER -