一句话：提出灵活分级表示，克服既有分级表示的缺陷，并建立其与一类分级单子的代数保持对应。
许多用于建模计算效应的单子可由操作与方程表示，而分级单子能追踪效应的定量信息，但既有的分级表示概念存在缺陷，导致不少效应没有自然的分级表示。本文引入“灵活分级表示”（flexibly graded presentation）并发展相应理论：证明每个灵活分级表示都诱导一个分级单子，且该单子带有表示中操作的解释；证明满足特定余极限条件的分级单子都具有灵活分级表示。作为核心结果，作者将通常的“表示与单子类之间的保持代数的对应”推广为灵活分级表示与一类灵活分级单子之间的保持代数的对应。
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.
@article{paperbot1488,
title = {Flexible presentations of graded monads},
author = {Shin-ya Katsumata and Dylan McDermott and Tarmo Uustalu and Nicolas Wu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547654}
}