A Category-Theoretic Framework for Dependent Effect Systems

TL;DR

This paper introduces indexed graded monads, a categorical framework that models dependent effects in effect systems, enabling more expressive reasoning about program properties like cost, probability, and safety.

Contribution

It extends categorical semantics of graded monads to support dependent effects, allowing for refined effect systems with dependent types.

Findings

Provides a semantics for a refinement type system with dependent effects

Enables formal reasoning about cost, probability, and safety properties

Demonstrates instantiations for various program analysis systems

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.