Opin vísindi

Flexibly graded monads and graded algebras

Flexibly graded monads and graded algebras

Title: Flexibly graded monads and graded algebras
Author: McDermott, Dylan
Uustalu, Tarmo
Date: 2022-09-22
Language: English
Scope: 102-128
University/Institute: Reykjavik University
Háskólinn í Reykjavík
School: School of Technology (RU)
Tæknisvið (HR)
Department: Department of Computer Science (RU)
Tölvunarfræðideild (HR)
ISBN: 9783031169113
Series: Lecture Notes in Computer Science;13544
ISSN: 0302-9743
DOI: 10.1007/978-3-031-16912-0_4
Subject: Graded monad; Graded algebra; Flexible grading; Relative monad; Computational effect; Locally graded category; Stærðfræði; Algebra; Tölvunarfræði
URI: https://hdl.handle.net/20.500.11815/4016

Show full item record


D. McDermott, T. Uustalu. Flexibly graded monads and graded algebras. In E. Komendantskaya, ed., Mathematics of Program Construction: 14th International Conference, MPC 2022, Tbilisi, Georgia, September 26-28, 2022, Proceedings, Lecture Notes in Computer Science, v. 13544, pp. 102-128. Springer, 2022. doi:10.1007/978-3-031-16912-0_4


When modelling side-effects using a monad, we need to equip the monad with effectful operations. This can be done by noting that each algebra of the monad carries interpretations of the desired operations. We consider the analogous situation for graded monads, which are a generalization of monads that enable us to track quantitative information about side-effects. Grading makes a significant difference: while many graded monads of interest can be equipped with similar operations, the algebras often cannot. We explain where these operations come from for graded monads. To do this, we introduce the notion of flexibly graded monad, for which the situation is similar to the situation for ordinary monads. We then show that each flexibly graded monad induces a canonical graded monad in such a way that operations for the flexibly graded monad carry over to the graded monad. In doing this, we reformulate grading in terms of locally graded categories, showing in particular that graded monads are a particular kind of relative monad. We propose that locally graded categories are a useful setting for work on grading in general.


Post-print (lokagerð höfundar)


From License to Publish, Article 3(c): The Licensee grants to the Author (i) the right to make the Accepted Manuscript available on their own personal, self-maintained website immediately on acceptance, (ii) the right to make the Accepted Manuscript available for public release on any of the following twelve (12) months after first publication (the “Embargo Period”): their employer’s internal website; their institutional and/or funder repositories. Accepted Manuscripts may be deposited in such repositories immediately upon acceptance, provided they are not made publicly available until after the Embargo Period. The rights granted to the Author with respect to the Accepted Manuscript are subject to the conditions that (i) the Accepted Manuscript is not enhanced or substantially reformatted by the Author or any third party, and (ii) the Author includes on the Accepted Manuscript an acknowledgement in the following form, together with a link to the published version on the publisher’s website: “This version of the contribution has been accepted for publication, after peer review (when applicable) but is not the Version of Record and does not reflect post-acceptance improvements, or any corrections. The Version of Record is available online at: http://dx.doi.org/[insert DOI]. Use of this Accepted Version is subject to the publisher’s Accepted Manuscript terms of use https://www.springernature.com/gp/open-research/policies/accepted-manuscript-terms”. Under no circumstances may an Accepted Manuscript be shared or distributed under a Creative Commons or other form of open access licence. Any use of the Accepted Manuscript not expressly permitted under this subclause (c) is subject to the Licensee’s prior consent.

Files in this item

This item appears in the following Collection(s)