Graded Algebraic Theories

TL;DR

This paper develops graded algebraic theories and demonstrates their categorical equivalence with graded Lawvere theories and finitary graded monads, extending classical results to graded settings and enabling effect combination.

Contribution

It introduces graded algebraic theories and proves their categorical equivalence with graded Lawvere theories and graded monads, extending existing theory.

Findings

Establishes categorical equivalence among graded algebraic theories, Lawvere theories, and graded monads.

Provides methods to combine computational effects using sums and tensor products of graded theories.

Extends classical algebraic theories to graded contexts, broadening their applicability.

Abstract

We provide graded extensions of algebraic theories and Lawvere theories that correspond to graded monads. We prove that graded algebraic theories, graded Lawvere theories, and finitary graded monads are equivalent via equivalence of categories, which extends the equivalence for monads. We also give sums and tensor products of graded algebraic theories to combine computational effects as an example of importing techniques based on algebraic theories to graded monads.