统一分次和参数化单子
Unifying graded and parameterised monads
摘要：
Monad是构造有效计算特征的有用工具，如状态、非确定性和连续性。在过去的十年中，已经提出了几种monad的概括，通过用构造函数的索引家族替换monad的单个类型构造函数来提供更细粒度的效果模型。最值得注意的是，分级单子（由一个幺半群索引）模型的效果系统和参数化单子（由成对的前置和后置条件索引）模型的程序逻辑。本文通过第三种推广来研究单子的这两种推广之间的关系。这第三个推广，我们称之为类别分级单子，是通过将单子的观点推广为lax函子的一个特殊情况而产生的。一个范畴分次单子提供了一个由其他范畴的态射f索引的函子T f族。这允许排除某些效果的组合（以程序逻辑的风格）以及效果的抽象描述（以效果系统的风格）。以此为基础，我们展示了如何分级和参数化单子可以统一，研究他们的相似之处和差异。
英文摘要：
Monads are a useful tool for structuring effectful features of computation such as state, non-determinism, and continuations. In the last decade, several generalisations of monads have been suggested which provide a more fine-grained model of effects by replacing the single type constructor of a monad with an indexed family of constructors. Most notably, graded monads (indexed by a monoid) model effect systems and parameterised monads (indexed by pairs of pre- and post-conditions) model program logics. This paper studies the relationship between these two generalisations of monads via a third generalisation. This third generalisation, which we call category-graded monads, arises by generalising a view of monads as a particular special case of lax functors. A category-graded monad provides a family of functors T f indexed by morphisms f of some other category. This allows certain compositions of effects to be ruled out (in the style of a program logic) as well as an abstract description of effects (in the style of an effect system). Using this as a basis, we show how graded and parameterised monads can be unified, studying their similarities and differences along the way.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
