@wilbowma have you seen Michael Ballantyne's work on syntax-spec? eg https://dl.acm.org/doi/10.1145/3428297, https://github.com/michaelballantyne/syntax-spec, https://dl.acm.org/doi/10.1145/3674627

I remember being interested in micros/mcmicmac because they might solve a similar problem (defining macro-extensible macros). Is that why you're interested, or some other reason?

my unsophisticated intuition is that the type of (not-necessarily-finite) state machines over an alphabet a ought to be: (exists s. s * (s -> bool) * (s * a -> s)). so somehow equality on existentials should capture bisimulation of state machines. which parametricity models are you thinking of - do they agree with this?

I'm also interested in why this might not be the "right" notion of equality - but for what I'm doing right now it's the notion of equality I care about :P.

@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

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