Powermonads and tensors of unranked effects

Sergey Goncharov*, Lutz Schröder

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 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.

Original languageEnglish
Title of host publicationProceedings - 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011
Pages227-236
Number of pages10
DOIs
Publication statusPublished - 2011
Event26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011 - Toronto, ON, Canada
Duration: 21 Jun 201124 Jun 2011

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871

Conference

Conference26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011
Country/TerritoryCanada
CityToronto, ON
Period21/06/1124/06/11

ASJC Scopus subject areas

  • Software
  • General Mathematics

Fingerprint

Dive into the research topics of 'Powermonads and tensors of unranked effects'. Together they form a unique fingerprint.

Cite this