Indexed Graded Monads and Their Logics

Kura, Gaboardi, Sekiyama, Unno · ESOP 2026 · arxiv arXiv:2601.14846

Prereqs: 🍞 Staton 2025 (Hoare triples), 🍞 Gaboardi 2021 (graded effects).

An indexed graded monad combines two ideas: the index says which type of state you start and end in (like a state machine), and the grade tracks cumulative effects. Definition 7 gives the composition rule: the output index of stage 1 must equal the input index of stage 2.

Simplifications on this page: grades are natural numbers with + as the semiring operation, indices are symbols, and logical quantification ("for all x") is demonstrated by finite test sets.

Indexing — which state you're in

An indexed monad T(i, j, A) means: "a computation that starts in state i, ends in state j, and produces a value of type A." You can only compose T(i, j, _) with T(j, k, _) — the output state of the first must match the input state of the second. This is the handshake.

Scheme

; Indexed computation: (start-state end-state value)
; Compose only when indices match: T(i,j) ; T(j,k) = T(i,k)

(define (make-indexed start end val) (list start end val))
(define idx-start car)
(define idx-end cadr)
(define idx-val caddr)

(define (idx-bind m f)
  (let* ((j (idx-end m))
         (result (f (idx-val m))))
    (if (eq? j (idx-start result))
        (make-indexed (idx-start m) (idx-end result) (idx-val result))
        (begin (display "ERROR: Index mismatch — handshake failed") (newline)))))

; raw -> filtered -> ranked
(define step1 (make-indexed 'raw 'filtered '(a b c)))
(define step2-fn (lambda (v) (make-indexed 'filtered 'ranked (length v))))

(define pipeline (idx-bind step1 step2-fn))
(display "pipeline: ") (display pipeline) (newline)
; (raw ranked 3) — indices chain, handshake holds

Adding grades on top

Now add a grade: T(i, j, e, A) means "start in i, end in j, with effect e, producing A." Composition requires index match (handshake) AND grade composition (budget accounting). This is Definition 3 in the paper. The paper uses a preordered semiring for grades; on this page, we use (ℕ, +, 0) — natural numbers with addition.

Scheme

; Indexed graded computation: (start end grade value)
(define (make-ig s e g v) (list s e g v))
(define ig-start car)
(define ig-end cadr)
(define ig-grade caddr)
(define ig-val cadddr)

(define (ig-bind m f grade-op)
  (let* ((j (ig-end m))
         (result (f (ig-val m))))
    (if (eq? j (ig-start result))
        (make-ig (ig-start m)
                 (ig-end result)
                 (grade-op (ig-grade m) (ig-grade result))
                 (ig-val result))
        (begin (display "ERROR: Index mismatch") (newline)))))

; stage 1: raw->cached, cost 2
(define step1 (make-ig 'raw 'cached 2 '(x y z)))

; stage 2: cached->filtered, cost 1
(define step2-fn
  (lambda (v) (make-ig 'cached 'filtered 1 (length v))))

(define result (ig-bind step1 step2-fn +))
(display "result: ") (display result) (newline)
; (raw filtered 3 3) — indices chain, grades add

The restricted pointwise order

Kura's innovation: the restricted pointwise order on graded predicates. A graded predicate Q at grade e refines Q' at grade e' if e ≤ e' and Q(x) implies Q'(x) for all x. This lets you weaken postconditions by increasing the allowed effect budget — you can always over-approximate.

Scheme

; Restricted pointwise order (toy checker — finite sample, not proof):
; (Q, e) ≤ (Q', e') iff e ≤ e' AND Q(x) => Q'(x) for all x

(define (every pred lst) (if (null? lst) #t (if (pred (car lst)) (every pred (cdr lst)) #f)))

(define (refines? Q e Q-prime e-prime test-vals)
  (and (<= e e-prime)
       (every (lambda (x)
         (if (Q x) (Q-prime x) #t))
       test-vals)))

(define Q  (lambda (x) (> x 10)))     ; strong: x > 10
(define Q* (lambda (x) (> x 0)))      ; weak: x > 0

; The real definition quantifies over all x.
; We test a finite sample to build intuition.
(define test-vals '(-5 0 5 10 15 20))

(display "(x>10, cost=1) refines (x>0, cost=3)? ")
(display (refines? Q 1 Q* 3 test-vals)) (newline)
; #t — tighter postcondition, lower budget

(display "(x>0, cost=3) refines (x>10, cost=1)? ")
(display (refines? Q* 3 Q 1 test-vals)) (newline)
; #f — looser postcondition can't refine tighter

The handshake — Definition 7

Definition 7 gives the composition rule for indexed graded Hoare triples. If {P} c₁ : (i→j, e₁) {R} and {R} c₂ : (j→k, e₂) {Q}, then {P} c₁;c₂ : (i→k, e₁·e₂) {Q}. The intermediate R is the handshake — it must satisfy both the postcondition of c₁ and the precondition of c₂, at matching index j.

Scheme

; Definition 7: The indexed graded handshake
; {P} c1 : (i->j, e1) {R}  and  {R} c2 : (j->k, e2) {Q}
;   => {P} c1;c2 : (i->k, e1+e2) {Q}

(define (make-triple pre post start end grade fn)
  (list pre post start end grade fn))
(define t-pre car) (define t-post cadr) (define t-start caddr)
(define t-end cadddr)
(define (t-grade t) (list-ref t 4))
(define (t-fn t) (list-ref t 5))

(define (compose-triples t1 t2 grade-op)
  (if (not (eq? (t-end t1) (t-start t2)))
      (begin (display "ERROR: Index mismatch") (newline)))
  ; The logical handshake: t1's postcondition must imply t2's precondition
  (list (t-pre t1) (t-post t2)
        (t-start t1) (t-end t2)
        (grade-op (t-grade t1) (t-grade t2))
        (lambda (x) ((t-fn t2) ((t-fn t1) x)))))

(define (run-triple t x)
  (if (not ((t-pre t) x)) (begin (display "ERROR: Precondition failed") (newline)))
  (let ((y ((t-fn t) x)))
    (if (not ((t-post t) y)) (begin (display "ERROR: Postcondition failed") (newline)))
    y))

; c1: takes any number, guarantees result >= 0
(define c1 (make-triple number? (lambda (y) (>= y 0))
            'raw 'cached 2 abs))

; c2: requires input >= 0, guarantees result <= 10
(define c2 (make-triple (lambda (y) (>= y 0)) (lambda (y) (<= y 10))
            'cached 'filtered 1 (lambda (x) (min x 10))))

; Composes: c1 guarantees >= 0, c2 requires >= 0 — handshake holds
(define pipeline (compose-triples c1 c2 +))
(display "Composed: ") (display (t-start pipeline))
(display " -> ") (display (t-end pipeline))
(display ", grade=") (display (t-grade pipeline)) (newline)
(display "run(-7): ") (display (run-triple pipeline -7)) (newline)
; raw -> filtered, grade=3, run(-7)=7

; Now break it: c3 requires input > 100 — c1 can't guarantee that
(define c3 (make-triple (lambda (y) (> y 100)) (lambda (y) #t)
            'cached 'filtered 1 (lambda (x) x)))
(define bad (compose-triples c1 c3 +))
(display "run(-7) with bad pipeline: ")
(display (run-triple bad -7))
; Error: precondition of c3 fails — 7 is not > 100

; Definition 7: The indexed graded handshake
; {P} c1 : (i->j, e1) {R}  and  {R} c2 : (j->k, e2) {Q}
;   => {P} c1;c2 : (i->k, e1+e2) {Q}

(define (make-triple pre post start end grade fn)
  (list pre post start end grade fn))
(define t-pre car) (define t-post cadr) (define t-start caddr)
(define t-end cadddr)
(define (t-grade t) (list-ref t 4))
(define (t-fn t) (list-ref t 5))

(define (compose-triples t1 t2 grade-op)
  (if (not (eq? (t-end t1) (t-start t2)))
      (begin (display "ERROR: Index mismatch") (newline)))
  ; The logical handshake: t1's postcondition must imply t2's precondition
  (list (t-pre t1) (t-post t2)
        (t-start t1) (t-end t2)
        (grade-op (t-grade t1) (t-grade t2))
        (lambda (x) ((t-fn t2) ((t-fn t1) x)))))

(define (run-triple t x)
  (if (not ((t-pre t) x)) (begin (display "ERROR: Precondition failed") (newline)))
  (let ((y ((t-fn t) x)))
    (if (not ((t-post t) y)) (begin (display "ERROR: Postcondition failed") (newline)))
    y))

; c1: takes any number, guarantees result >= 0
(define c1 (make-triple number? (lambda (y) (>= y 0))
            'raw 'cached 2 abs))

; c2: requires input >= 0, guarantees result <= 10
(define c2 (make-triple (lambda (y) (>= y 0)) (lambda (y) (<= y 10))
            'cached 'filtered 1 (lambda (x) (min x 10))))

; Composes: c1 guarantees >= 0, c2 requires >= 0 — handshake holds
(define pipeline (compose-triples c1 c2 +))
(display "Composed: ") (display (t-start pipeline))
(display " -> ") (display (t-end pipeline))
(display ", grade=") (display (t-grade pipeline)) (newline)
(display "run(-7): ") (display (run-triple pipeline -7)) (newline)
; raw -> filtered, grade=3, run(-7)=7

; Now break it: c3 requires input > 100 — c1 can't guarantee that
(define c3 (make-triple (lambda (y) (> y 100)) (lambda (y) #t)
            'cached 'filtered 1 (lambda (x) x)))
(define bad (compose-triples c1 c3 +))
(display "run(-7) with bad pipeline: ")
(display (run-triple bad -7))
; Error: precondition of c3 fails — 7 is not > 100

Python

# Definition 7: Indexed graded Hoare triple composition
class Triple:
    def __init__(self, pre, post, start, end, grade, fn):
        self.pre, self.post = pre, post
        self.start, self.end, self.grade, self.fn = start, end, grade, fn

    def compose(self, other, grade_op=lambda a, b: a + b):
        assert self.end == other.start, f"Index mismatch: {self.end} != {other.start}"
        return Triple(self.pre, other.post,
                      self.start, other.end,
                      grade_op(self.grade, other.grade),
                      lambda x: other.fn(self.fn(x)))

    def run(self, x):
        assert self.pre(x), f"Precondition failed on {x}"
        y = self.fn(x)
        assert self.post(y), f"Postcondition failed on {y}"
        return y

# c1: any number -> guarantees >= 0
c1 = Triple(lambda x: isinstance(x, (int, float)), lambda y: y >= 0,
            "raw", "cached", 2, abs)
# c2: requires >= 0 -> guarantees <= 10
c2 = Triple(lambda y: y >= 0, lambda y: y <= 10,
            "cached", "filtered", 1, lambda x: min(x, 10))

pipeline = c1.compose(c2)
print(f"{pipeline.start} -> {pipeline.end}, grade={pipeline.grade}")
print(f"run(-7): {pipeline.run(-7)}")

# Break it: c3 requires > 100 — c1 can't guarantee that
c3 = Triple(lambda y: y > 100, lambda y: True,
            "cached", "filtered", 1, lambda x: x)
bad = c1.compose(c3)
print(f"run(-7) with bad pipeline: {bad.run(-7)}")
# AssertionError: Precondition failed on 7

# Definition 7: Indexed graded Hoare triple composition
class Triple:
    def __init__(self, pre, post, start, end, grade, fn):
        self.pre, self.post = pre, post
        self.start, self.end, self.grade, self.fn = start, end, grade, fn

def compose(self, other, grade_op=lambda a, b: a + b):
        assert self.end == other.start, f"Index mismatch: {self.end} != {other.start}"
        return Triple(self.pre, other.post,
                      self.start, other.end,
                      grade_op(self.grade, other.grade),
                      lambda x: other.fn(self.fn(x)))

def run(self, x):
        assert self.pre(x), f"Precondition failed on {x}"
        y = self.fn(x)
        assert self.post(y), f"Postcondition failed on {y}"
        return y

# c1: any number -> guarantees >= 0
c1 = Triple(lambda x: isinstance(x, (int, float)), lambda y: y >= 0,
            "raw", "cached", 2, abs)
# c2: requires >= 0 -> guarantees <= 10
c2 = Triple(lambda y: y >= 0, lambda y: y <= 10,
            "cached", "filtered", 1, lambda x: min(x, 10))

pipeline = c1.compose(c2)
print(f"{pipeline.start} -> {pipeline.end}, grade={pipeline.grade}")
print(f"run(-7): {pipeline.run(-7)}")

# Break it: c3 requires > 100 — c1 can't guarantee that
c3 = Triple(lambda y: y > 100, lambda y: True,
            "cached", "filtered", 1, lambda x: x)
bad = c1.compose(c3)
print(f"run(-7) with bad pipeline: {bad.run(-7)}")
# AssertionError: Precondition failed on 7

Confidence: Simplified. Captures the composition law. The paper's version works over graded Freyd categories with a preordered semiring.

Graded monad lifting

The restricted pointwise order weakens postconditions: more budget, less guaranteed about the output. Lifting works the other direction. It pulls a postcondition backward through a computation to derive the weakest precondition on the input. The grade controls how much that precondition relaxes. Same monotonicity, opposite ends of the pipe.

Scheme

; Graded lifting: wp_e(c, Q) — weakest pre adjusted by grade
; Grade = tolerance. Higher grade = weaker precondition needed.

(define (graded-wp c grade Q)
  ; Returns a predicate: "does x satisfy the weakest
  ; precondition of c for postcondition Q at this grade?"
  (lambda (x)
    (let ((result (c x)))
      (Q result grade))))

; Postcondition: result within tolerance of target
(define target 100)
(define (within-tolerance y grade) (<= (abs (- y target)) (* grade 5)))

(define (noisy-measure x) (+ x 3))  ; systematic bias of 3

; wp at grade 1: only inputs where |c(x) - 100| <= 5
(define wp-tight (graded-wp noisy-measure 1 within-tolerance))
; wp at grade 4: inputs where |c(x) - 100| <= 20
(define wp-loose (graded-wp noisy-measure 4 within-tolerance))

(define vals '(80 90 95 97 100 103 110 120))
(for-each (lambda (x)
  (display x)
  (display " grade=1:") (display (if (wp-tight x) "pass" "fail"))
  (display " grade=4:") (display (if (wp-loose x) "pass" "fail"))
  (newline))
vals)
; Higher grade => more inputs pass the weakest precondition

; Graded lifting: wp_e(c, Q) — weakest pre adjusted by grade
; Grade = tolerance. Higher grade = weaker precondition needed.

(define (graded-wp c grade Q)
  ; Returns a predicate: "does x satisfy the weakest
  ; precondition of c for postcondition Q at this grade?"
  (lambda (x)
    (let ((result (c x)))
      (Q result grade))))

; Postcondition: result within tolerance of target
(define target 100)
(define (within-tolerance y grade) (<= (abs (- y target)) (* grade 5)))

(define (noisy-measure x) (+ x 3))  ; systematic bias of 3

; wp at grade 1: only inputs where |c(x) - 100| <= 5
(define wp-tight (graded-wp noisy-measure 1 within-tolerance))
; wp at grade 4: inputs where |c(x) - 100| <= 20
(define wp-loose (graded-wp noisy-measure 4 within-tolerance))

(define vals '(80 90 95 97 100 103 110 120))
(for-each (lambda (x)
  (display x)
  (display " grade=1:") (display (if (wp-tight x) "pass" "fail"))
  (display " grade=4:") (display (if (wp-loose x) "pass" "fail"))
  (newline))
vals)
; Higher grade => more inputs pass the weakest precondition

Notation reference

Paper	Scheme	Meaning
T(i, j, e, A)	(make-ig i j e val)	Indexed graded computation
e₁ · e₂	(grade-op e1 e2)	Grade composition
i = j (Def 7)	(eq? (idx-end t1) (idx-start t2))	Index handshake
≤_rpo	refines?	Restricted pointwise order
wp_e(c, Q)	(graded-wp c grade Q)	Graded weakest precondition

Neighbors

Other paper pages

🍞 Gaboardi 2021 — graded Hoare logic (grading without indexing)
🍞 Staton 2025 — ungraded Hoare logic (the handshake without budgets)
🍞 Liell-Cock 2025 — graded monads in the Para construction

Foundations (Wikipedia)

Translation notes

All examples use simple integers for grades and symbols for indices. The paper works over preordered semirings for grades and arbitrary index categories, with the restricted pointwise order defined on fibered predicates. For example: the handshake demonstration on this page checks symbol equality between two stages. In the paper, the same definition works over a category of indexed types where the index match is a morphism equation in the index category — allowing non-trivial coercions between compatible state types. The composition pattern is identical. The categorical generality is not.

Ready for the real thing? arxiv

Read the paper. Start at §3 for indexed graded monads (Def 3), §4 for the Hoare logic (Def 7).

Framework connection: The Natural Framework pipeline's handshake composition maps directly to Definition 7 — the output index of each stage must match the input index of the next. (The Handshake)

← Gaboardi 2021 · 4 of 21 by june.kim Hedges 2018 · 6 of 21 →