TY - GEN
T1 - A counterexample to tensorability of effects
AU - Goncharov, Sergey
AU - Schröder, Lutz
PY - 2011
Y1 - 2011
N2 - Monads are widely used in programming semantics and in functional programming to encapsulate notions of side-effect, such as state, exceptions, input/output, or continuations. One of their advantages is that they allow for a modular treatment of effects, using composition operators such as sum and tensor. Here, the sum represents the non-interacting combination of effects, while the tensor imposes a high degree of interaction in the shape of a commutation law. Although many important effects are ranked, i.e. presented by algebraic operations of bounded arity, there is also a range of relevant unranked effects, with prominent examples including continuations and unbounded non-determinism. While the sum and tensor of ranked effects always exist, this is not so clear already when one of the components is unranked, in which case size problems come into play. In contrast to the case of sums where a counterexample can be constructed rather trivially, the general existence of tensors has, so far, been an open issue - as the tensor identifies more terms than the sum, it does exist in many cases where the sum fails to exist. As a possible counterexample, tensors of continuations with unranked effects have been discussed; however, we have disproved that possibility in recent work. In the present work, we nevertheless settle the question in the negative by presenting a well-order monad whose tensor with a simple ranked monad fails to exist; as a consequence, we show also that there is an unranked monad whose tensor with the finite list monad fails to exist.
AB - Monads are widely used in programming semantics and in functional programming to encapsulate notions of side-effect, such as state, exceptions, input/output, or continuations. One of their advantages is that they allow for a modular treatment of effects, using composition operators such as sum and tensor. Here, the sum represents the non-interacting combination of effects, while the tensor imposes a high degree of interaction in the shape of a commutation law. Although many important effects are ranked, i.e. presented by algebraic operations of bounded arity, there is also a range of relevant unranked effects, with prominent examples including continuations and unbounded non-determinism. While the sum and tensor of ranked effects always exist, this is not so clear already when one of the components is unranked, in which case size problems come into play. In contrast to the case of sums where a counterexample can be constructed rather trivially, the general existence of tensors has, so far, been an open issue - as the tensor identifies more terms than the sum, it does exist in many cases where the sum fails to exist. As a possible counterexample, tensors of continuations with unranked effects have been discussed; however, we have disproved that possibility in recent work. In the present work, we nevertheless settle the question in the negative by presenting a well-order monad whose tensor with a simple ranked monad fails to exist; as a consequence, we show also that there is an unranked monad whose tensor with the finite list monad fails to exist.
UR - http://www.scopus.com/inward/record.url?scp=80053010979&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-22944-2_15
DO - 10.1007/978-3-642-22944-2_15
M3 - Conference contribution
AN - SCOPUS:80053010979
SN - 9783642229435
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 208
EP - 221
BT - Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Proceedings
T2 - 4th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2011
Y2 - 30 August 2011 through 2 September 2011
ER -