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 binary operation and a constant. 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.
Wed 14 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
13:40 - 15:20 | Programming and Reasoning About EffectsICFP Papers and Events at Linhart Chair(s): William J. Bowman University of British Columbia | ||
13:40 20mTalk | Monadic Compiler CalculationFunctional Pearl ICFP Papers and Events DOI | ||
14:00 20mTalk | Formal Reasoning About Layered Monadic Interpreters ICFP Papers and Events Irene Yoon University of Pennsylvania, Yannick Zakowski Inria, Steve Zdancewic University of Pennsylvania DOI | ||
14:20 20mTalk | Program Adverbs and Tlön EmbeddingsDistinguished PaperVirtual ICFP Papers and Events DOI Pre-print | ||
14:40 20mTalk | Flexible presentations of graded monads ICFP Papers and Events Shin-ya Katsumata National Institute of Informatics, Dylan McDermott Reykjavik University, Tarmo Uustalu Reykjavik University, Nicolas Wu Imperial College London DOI | ||
15:00 20mTalk | Fusing Industry and Academia at GitHubExperience Report ICFP Papers and Events Patrick Thomson GitHub, Rob Rix GitHub, Inc., Tom Schrijvers KU Leuven, Nicolas Wu Imperial College London DOI |