Define monad transformer for an inductively defined monad?

Stream: lean4

[Quang Dao]

I am trying to define (reactive) resumption monad transformers in Lean, with the goal toward formalizing cryptographic reasoning as in this Isabelle library. The reactive resumption monad can be defined inductively as:

inductive ReacM (Input : Type v) (Output : Type w) (α : Type u) : Type (max u v w) where
  | done : α → ReacM Input Output α
  | pause : Output → (Input → ReacM Input Output α) → ReacM Input Output α

This is all well and good, but I cannot use the same strategy to define its transformer version:

inductive ReacT (Input : Type u) (Output : Type u) (m : Type u → Type u)
    [Monad m] [LawfulMonad m] (α : Type u) : Type u where
  | done : m α → ReacT Input Output m α
  | pause : m (Output × (Input → ReacT Input Output m α)) → ReacT Input Output m α
/-
(kernel) arg #7 of 'ReacT.pause' contains a non valid occurrence of the datatypes being declared
-/

Is there a way to tell Lean that this inductive definition still works, despite the non-positivity?

[Chris Bailey]

You can use theunsafe modifier, as in unsafe inductive ReacT. It may or may not prevent you from doing other things you wanted to do in terms of proof.

[Chris Bailey]

I just glanced at the provided link so feel free to blow this off, but the ReacT.pause in the paper seems like Input -> Output -> m (ReacT Input Output m a)) which naively looks like StateCpsT, maybe you can use that?

[François G. Dorais]

Does this form work for your application?

inductive ReacT (Input : Type u) (Output : Type u) (m : Type u → Type u)
    [Monad m] [LawfulMonad m] (α : Type u) : Type u where
  | done : m α → ReacT Input Output m α
  | pause : m Output  → (Input → ReacT Input Output m α) → ReacT Input Output m α

I don't think you need to wrap Input → ReacT Input Output m α in the monad, but you might still need a squash : m (ReacT Input Output m α) → ReacT Input Output m α depending on what you are actually doing. That squash is illegal but there are some workarounds that might work if you really need them.

[François G. Dorais]

(Of course, you can always do unsafe inductive to bypass the issue entirely, if that's what you need.)

[Quang Dao]

Thanks for your answers. I don't want to use unsafe since I want to prove properties of ReacT.

I'll continue thinking about the proposed alternatives. One option I haven't tried is to define ReacT m directly for a specific monad m of interest (in my case it is a probability mass function).