Graded monads refine traditional monads using effect annotations in order to describe quantitatively the computational effects that a program can generate. They have been successfully applied to a variety of formal systems for reasoning about effectful computations. However, existing categorical frameworks for graded monads do not support effects that may depend on program values, which we call dependent effects, thereby limiting their expressiveness. We address this limitation by introducing indexed graded monads, a categorical generalization of graded monads inspired by the fibrational "indexed" view and by classical categorical semantics of dependent type theories. We show how indexed graded monads provide semantics for a refinement type system with dependent effects. We also show how this type system can be instantiated with specific choices of parameters to obtain several formal systems for reasoning about specific program properties. These instances include, in particular, cost analysis, probability-bound reasoning, expectation-bound reasoning, and temporal safety verification.

翻译：分级单子通过效应标注对传统单子进行精化，以定量描述程序可能产生的计算效应。该方法已成功应用于多种形式系统，用于推理带效应的计算。然而，现有分级单子的范畴论框架不支持可能依赖于程序值的效应（我们称之为依赖效应），从而限制了其表达能力。我们通过引入索引分级单子来解决这一局限性，该结构是分级单子的范畴推广，其灵感来源于纤维化的“索引”视角以及依赖类型理论的经典范畴语义。我们展示了索引分级单子如何为具有依赖效应的精化类型系统提供语义。同时，我们演示了如何通过特定参数实例化该类型系统，从而获得多个用于推理特定程序属性的形式系统。这些实例特别包括代价分析、概率界限推理、期望界限推理以及时序安全性验证。