Computer Science – Logic in Computer Science
Scientific paper
2011-01-14
Computer Science
Logic in Computer Science
extended version; first 10 pages are to appear on LICS'11
Scientific paper
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.
Goncharov Sergey
Schröder Linda L.
No associations
LandOfFree
Powermonads and Tensors of Unranked Effects does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Powermonads and Tensors of Unranked Effects, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Powermonads and Tensors of Unranked Effects will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-79103