Graded Monad

Graded Monad Skill

"A graded monad is a lax 2-functor from a monoidal category (viewed as a one-object 2-category) to Cat." — Soichiro Fujii (2019)

Trit: 0 (ERGODIC - coordinator) Color: #26D826 (Green) Status: Production Ready

Overview

A graded monad (also called an indexed monad or parametrized monad) is a monad whose operations carry an index from a monoidal category. The 2-categorical perspective reveals graded monads as:

• Lax 2-functors from a monoidal category to Cat
• Monads in a suitable 2-category (Fujii's insight)
• Effect systems with tracked computational effects

This unifies the programming notion of graded effects with the categorical notion of 2-monads.

Mathematical Definition

Given a monoidal category (M, ⊗, I):

A GRADED MONAD over M consists of:
  T : M → End(C)     (family of endofunctors indexed by M)
  η : Id → T_I       (unit, indexed by monoidal unit I)
  μ : T_m ∘ T_n → T_{m⊗n}  (multiplication, indexed by tensor)

subject to:
  μ_{m⊗n,p} ∘ (T_m μ_{n,p}) = μ_{m,n⊗p} ∘ (μ_{m,n} T_p)  (associativity)
  μ_{I,m} ∘ (η T_m) = id = μ_{m,I} ∘ (T_m η)                (unitality)

AS A 2-CATEGORICAL STRUCTURE:
  View M as a one-object 2-category ΣM:
    - One object: *
    - 1-cells: objects of M
    - 2-cells: morphisms of M
    - Composition: ⊗

  Then a graded monad = monad in the 2-category [ΣM, Cat]
  (lax 2-functors, lax natural transformations, modifications)

FUJII'S THEOREM:
  Graded monads over M ≅ Monads in Dist(M, -)
  where Dist is the 2-category of distributors/profunctors

The 2-Categorical Connection

┌─────────────────────────────────────────────────────────────┐
│                                                             │
│   ORDINARY MONAD          GRADED MONAD                      │
│                                                             │
│   T : C → C               T_m : C → C  (for each m ∈ M)    │
│   η : Id → T              η : Id → T_I                     │
│   μ : T² → T              μ_{m,n} : T_m T_n → T_{m⊗n}     │
│                                                             │
│   = monad in Cat           = monad in [ΣM, Cat]             │
│   = 2-monad on 1           = 2-monad on ΣM                  │
│                                                             │
│   T-Alg = Eilenberg-       T-Alg = graded algebras          │
│           Moore cats                (effect handlers)        │
│                                                             │
└─────────────────────────────────────────────────────────────┘

GF(3) Mapping

The graded monad coordinates between the constraining index category and the generative algebras — hence trit 0.

Programming Applications

Effect Systems (Haskell)

-- Graded monad for tracked effects
class GradedMonad (m :: k -> * -> *) where
  type Unit m :: k
  type Mult m (a :: k) (b :: k) :: k

  greturn :: a -> m (Unit m) a
  gbind   :: m i a -> (a -> m j b) -> m (Mult m i j) b

-- Example: State with tracked permissions
data Perm = Read | Write | ReadWrite

data StatePerm (p :: Perm) a where
  SRead  :: (s -> a) -> StatePerm 'Read a
  SWrite :: (s -> (a, s)) -> StatePerm 'Write a

instance GradedMonad StatePerm where
  type Unit StatePerm = 'Read
  type Mult StatePerm 'Read 'Read = 'Read
  type Mult StatePerm _ _ = 'Write  -- any write contaminates

Algebraic Effects (Eff)

-- Graded by effect set
graded_run : {E : EffectSet} → Eff E a → Handler E a → a

-- Index tracks which effects are used
-- M = PowerSet(Effects) with ∪ as tensor

IES Session Types (Lux Integration)

-- Session types are graded monads over protocol steps
Session : Protocol → Type → Type

-- Index category M = free category on protocol graph
-- T_step : action at that protocol step
-- μ : sequential composition of protocol steps

Why This Skill Was Missing

Graded monads were split across adjacent concepts:

1. free-monad-gen generates free monads in 1-categories, not graded/indexed variants
2. 2-monad defines 2-categorical monad theory but doesn't specialize to the ΣM case
3. linear-logic connects to resource tracking (grades ≈ resource annotations) but doesn't formalize the monad structure
4. kan-extensions handles Lan/Ran which can produce graded structure but doesn't own the definition

Gap: No skill connected the programming notion of graded effects (Haskell/Eff effect systems) to the 2-categorical definition (monads in [ΣM, Cat]). This unification is Fujii's key contribution and the bridge between 2-monad theory and practical programming.

Julia/Catlab Integration

using Catlab.CategoricalAlgebra

@present SchGradedMonad(FreeSchema) begin
    # Index category M
    Grade::Ob
    GradeMorph::Ob
    grade_src::Hom(GradeMorph, Grade)
    grade_tgt::Hom(GradeMorph, Grade)

    # Monoidal structure on M
    tensor::Hom(Grade, Grade)  # m ⊗ n (simplified)
    unit_grade::Hom(Grade, Grade)  # I

    # Graded endofunctor family
    GradedEndo::Ob
    endo_grade::Hom(GradedEndo, Grade)  # T_m indexed by m

    # Multiplication indexed by grade pairs
    GradedMult::Ob
    mult_left::Hom(GradedMult, Grade)   # m
    mult_right::Hom(GradedMult, Grade)  # n
    mult_result::Hom(GradedMult, Grade) # m ⊗ n

    EffectLabel::AttrType
    grade_label::Attr(Grade, EffectLabel)
end

Canonical Examples

GF(3) as Index Category

The GF(3) field itself is a monoidal category:
  Objects: {-1, 0, +1}
  Tensor: addition mod 3
  Unit: 0

A GF(3)-graded monad T tracks trit balance:
  T_{-1} : validator computations
  T_0    : coordinator computations
  T_{+1} : generator computations

  μ : T_m ∘ T_n → T_{m+n mod 3}

  Conservation: composing computations respects trit arithmetic

Bidirectional Neighbor Index

Edge-Scoped Propagator Table

Mutual Awareness Summary

       2-monad (0)
            ↑ compose
            │
free-monad (+1) ←── GRADED-MONAD (0) ──→ linear-logic (-1)
            │           │
            ↓ compose   ↓ verify
    codescent (-1)   gf3-tripartite (0)

+ 6 additional edges to existing skills

Total edges: 20 (10 bidirectional pairs) Propagator balance: 6 scope:change + 8 scope:compose + 6 scope:verify = balanced

GF(3) Triads

codescent (-1) ⊗ graded-monad (0) ⊗ flexible-algebra (+1) = 0 ✓  [Graded-BKP]
sheaf-cohomology (-1) ⊗ graded-monad (0) ⊗ free-monad-gen (+1) = 0 ✓  [Graded-Free]
linear-logic (-1) ⊗ graded-monad (0) ⊗ operad-compose (+1) = 0 ✓  [Resource-Operad]
segal-types (-1) ⊗ graded-monad (0) ⊗ synthetic-adjunctions (+1) = 0 ✓  [Index-Adjunction]
covariant-fibrations (-1) ⊗ graded-monad (0) ⊗ discopy-operads (+1) = 0 ✓  [Fibered-Graded]

Commands

just graded-monad-define M           # Define graded monad over index M
just graded-monad-compose m n        # Compute μ_{m,n} : T_m T_n → T_{m⊗n}
just graded-monad-embed T            # Embed as 2-monad on ΣM
just graded-monad-effects program    # Track effect grades through program
just graded-monad-gf3 computation    # Verify GF(3) grade conservation

References

• Fujii, S. (2019). "Towards a formal theory of graded monads." FSCD 4:1-17
• Katsumata, S. (2014). "Parametric effect monads and semantics of effect systems." POPL
• Orchard, D. & Yoshida, N. (2016). "Effects as sessions, sessions as effects." POPL
• Mellies, P.-A. (2017). "Categorical semantics of linear logic." In Panoramas et Synthèses 27
• Street, R. (1972). "The formal theory of monads." JPAA 2:149-168
• Smirnov, A. (2008). "Graded monads and rings of polynomials." Journal of Homotopy and Related Structures

SDF Interleaving

Primary Chapter: 6. Layering

Concepts: layered data, metadata, provenance, units

GF(3) Balanced Triad

graded-monad (0) + SDF.Ch6 (0) + [balancer] (0) = 0

Skill Trit: 0 (ERGODIC - coordination)

Connection Pattern

Layering adds metadata and provenance. Graded monads layer computational effects with grade annotations — each operation carries its "provenance" as an index from the grading category M.

CT lattice atlas

Part of: para-mensch-commons (CT lattice family).