A Category-Theoretic Framework for Dependent Effect Systems
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911389428219904 |
|---|---|
| author | Kura, Satoshi Gaboardi, Marco Sekiyama, Taro Unno, Hiroshi |
| author_facet | Kura, Satoshi Gaboardi, Marco Sekiyama, Taro Unno, Hiroshi |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_14846 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Category-Theoretic Framework for Dependent Effect Systems Kura, Satoshi Gaboardi, Marco Sekiyama, Taro Unno, Hiroshi Logic in Computer Science 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. |
| title | A Category-Theoretic Framework for Dependent Effect Systems |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2601.14846 |