Combining effects: Sum and tensor

• Published in: Theoretical computer science 2006-07, Vol.357 (1), p.70-99
• Main Authors: Hyland, Martin, Plotkin, Gordon, Power, John
• Format: Article
• Language: English
• Subjects: Algebra; Algorithmics. Computability. Computer arithmetics; Applied sciences; Category theory, homological algebra; Computational effect; Computer science; control theory; systems; Exact sciences and technology; General logic; Lawvere theory; Logic and foundations; Mathematical logic, foundations, set theory; Mathematics; Modularity; Monad; Sciences and techniques of general use; Theoretical computing
• ISSN: 0304-3975; 1879-2294
• DOI: 10.1016/j.tcs.2006.03.013

We seek a unified account of modularity for computational effects. We begin by reformulating Moggi's monadic paradigm for modelling computational effects using the notion of enriched Lawvere theory, together with its relationship with strong monads; this emphasises the importance of the operations that produce the effects. Effects qua theories are then combined by appropriate bifunctors on the category of theories. We give a theory for the sum of computational effects, which in particular yields Moggi's exceptions monad transformer and an interactive input/output monad transformer. We further give a theory of the commutative combination of effects, their tensor, which yields Moggi's side-effects monad transformer. Finally, we give a theory of operation transformers, for redefining operations when adding new effects; we derive explicit forms for the operation transformers associated to the above monad transformers.