A Category-Theoretic Framework for Dependent Effect Systems

TL;DR

This work presents a semantic framework that extends graded monads to support dependent effects by introducing indexed graded monads. By indexing both contexts and effect grades via Pred-based predicates, the authors provide a cohesive fibrational semantics for a refinement-type system with dependent effects. They prove soundness of the dependent effect system, demonstrate a systematic construction of indexed graded monads from ordinary graded monads, and instantiate the framework across multiple domains, including cost analysis, probabilistic reasoning, and temporal safety. The approach enables precise, value-dependent effect bounds and offers a unifying, category-theoretic foundation for refinement types with dependent effects, with potential for automated verification in practical languages.

Abstract

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.

Figures (10)

• Figure 1: Models of simple and dependent effect systems.
• Figure 2: Selected typing rules. Substitution of a value term $V$ for a variable $x$ is denoted by suffixing $[V/x]$.
• Figure 3: Selected rules for subtyping. Here, $\dot{\Gamma} \vDash \mathcal{E}_1 \le \mathcal{E}_2$ is semantic subeffecting in the refinement context $\dot{\Gamma}$.
• Figure 4: Dependency of the interpretation $\interpret{-}$. The interpretation is defined from top to bottom: (1) the interpretation of simply typed FGCBV is defined first; (2) using the interpretation of value terms in simply typed FGCBV, formulas are interpreted; (3) the interpretation of graded refinement types, graded refinement contexts, and dependent-effect terms are defined by simultaneous induction; and (4) the soundness of the dependent effect system is established by showing the existence of a lifting of the interpretation of terms in simply typed FGCBV.
• Figure 5: Instances of graded Hoare logics for simple effects.

Theorems & Definitions (119)

• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• proposition thmcounterproposition
• definition thmcounterdefinition
• lemma thmcounterlemma
• lemma thmcounterlemma