rntz
Is there a type system using graded monads that puts a grade on the _typing judgment_, not just on the monad type? I swear I saw something like this once, but can't find it. @dorchard ?
Jun 21 at 4:55pmWeb
Show threadrntzJun 21

I might expect rules like the following:

Γ ⊢_m e : T_n A
-------------------
Γ ⊢_{mn} run e : A

Γ ⊢_{mn} e : A
----------------------
Γ ⊢_m thunk e : T_n A

Γ ⊢_m e1 : A
Γ, x:A ⊢_n e2 : B
------------------------------
Γ ⊢_{mn} let x = e1 in e2 : B

Show threadjcreedJun 21
@rntz are you assuming a monoid operation on the turnstile index?
Show threadrntzJun 21
@jcreed yes. Graded monads are generally graded by something that has at least the structure of a partially ordered monoid (partial order is for "subtyping"/weakening - it can be discrete to trivialize this; monoid operator is for monadic join; monoid operator must be monotone wrt the partial order).
Show threadrntzJun 21

@jcreed T_{m} a graded monad on C means, iirc:

pure : Hom(A, T_1 A)
map : Hom(A,B) -> Hom(T_m A, T_m B)
join : Hom(T_m T_n A, T_{mn} A)
and probably
weaken : (m <= n) -> Hom(T_m A, T_n A) or maybe it flips direction whatever

plus appropriate naturalities/laws