Flexible presentations of graded monads
Open Access
- 29 August 2022
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Programming Languages
- Vol. 6 (ICFP) , 902-930
Abstract
A large class of monads used to model computational effects have natural presentations by operations and equations, for example, the list monad can be presented by a constant and a binary operation subject to unitality and associativity. Graded monads are a generalization of monads that enable us to track quantitative information about the effects being modelled. Correspondingly, a large class of graded monads can be presented using an existing notion of graded presentation. However, the existing notion has some deficiencies, in particular many effects do not have natural graded presentations. We introduce a notion of flexibly graded presentation that does not suffer from these issues, and develop the associated theory. We show that every flexibly graded presentation induces a graded monad equipped with interpretations of the operations of the presentation, and that all graded monads satisfying a particular condition on colimits have a flexibly graded presentation. As part of this, we show that the usual algebra-preserving correspondence between presentations and a class of monads transfers to an algebra-preserving correspondence between flexibly graded presentations and a class of flexibly graded monads.Keywords
Funding Information
- Icelandic Centre for Research (196323-053 and 228684-051)
- Engineering and Physical Sciences Research Council (EP/S028129/1)
- Japan Science and Technology Agency (JPMJER1603)
This publication has 22 references indexed in Scilit:
- Monads need not be endofunctorsLogical Methods in Computer Science, 2015
- Trace Semantics via Generic ObservationsLecture Notes in Computer Science, 2013
- Algebraic foundations for effect-dependent optimisations2012
- Notions of Lawvere TheoryApplied Categorical Structures, 2009
- Graded monads and rings of polynomialsJournal of Mathematical Sciences, 2008
- Combining effects: Sum and tensorTheoretical Computer Science, 2006
- Notions of Computation Determine Monads2002
- Gabriel-Ulmer duality for categories enriched in bicategoriesJournal of Pure and Applied Algebra, 1999
- Adjunctions whose counits are coequalizers, and presentations of finitary enriched monadsJournal of Pure and Applied Algebra, 1993
- Polymorphic effect systems1988