Lawful classes for `Monad{Lift/Control/etc}`?

Stream: general

[Quang Dao]

Hi all,

I'm looking to add Lawful instances to a bunch of monadic definitions in Init/Prelude such as Monad{Lift/Control/Functor/State/etc.}. The motivation being verification of programs written in a monadic stack. More generally, I hope to flesh out the monadic stack in Lean and align them to be more similar to what is in Haskell.

It seems that there's interest in such a development, from prior Zulip threads here and here. I'd imagine that this will prove helpful to Lean FRO's project to add support for verifying do block code (see this comment).

My question is thus: is this something in scope for the community, and where should this go (i.e. lean, batteries, mathlib, or perhaps a separate repo)?

[Kim Morrison]

To the extent that you are simply adding lawful instances of existing LawfulX type classes, I would suggest Batteries, or possibly Lean if you're happy to write an RFC first, and explain clearly what is being done and what would remain to be done.

If you're designing new classes, I'd recommend exploring in a separate repo for a while.

[François G. Dorais]

Do feel free to consult people in the batteries channel about this and related questions.

[Quang Dao]

PR opened: batteries#1125

[Kim Morrison]

Looks good, thanks. Left minor comments, but this is sufficiently straightforward that I'd be happy to take it.

[Kim Morrison]

Can you add instances corresponding to

instance (m n o) [MonadLift n o] [MonadLiftT m n] : MonadLiftT m o where
  monadLift x := MonadLift.monadLift (m := n) (monadLift x)

instance (m) : MonadLiftT m m where
  monadLift x := x

[Kim Morrison]

Can you say something about the EIO, BaseIO, IO, CoreM, MetaM, TermElabM, TacticM, CommandElabM stack. Are there any meaningful instances for the lifts existing there?

[Quang Dao]

A lot of these don't even appear to be accessible in batteries? They also rely on StateRefT which is somehow opaque.

I went through all instances of MonadLift (via typing #check instMonadLift and wait for all suggestions) and add the corresponding Lawful instances

[Kim Morrison]

To find all instances, grep instance.*: MonadLift in the lean4 repo.

[Kim Morrison]

If you want to add anything about the CoreM and upwards stack (if it even is true?) then they should go in Batteries/Lean/LawfulMonadLift.lean.