ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Sun 11 Sep 2022 14:00 - 14:30 at M1 - HOPE Session 3

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.

Sun 11 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

14:00 - 15:30
HOPE Session 3HOPE at M1
Flexibly graded monads and graded algebras
Dylan McDermott Reykjavik University, Tarmo Uustalu Reykjavik University
File Attached
Monadic Semantics of Bidirectional Effects
Youyou Cong Tokyo Institute of Technology, Shin-ya Katsumata National Institute of Informatics, Kazuki Niimi Axell Corporation, Jonathan Immanuel Brachthäuser University of Tübingen