Monad assumptions in fields of other typeclasses

Stream: lean4

[Eric Wieser]

I found this definitions rather strange:

class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂)) where
  /--
  Runs the monadic action `f` on each element of the collection `coll`.
  -/
  forM [Monad m] (coll : γ) (f : α → m PUnit) : m PUnit

what is the [Monad m] argument doing there? Shouldn't it be up to individual instances to decide if they need m to be a Monad?

[Aaron Liu]

That not how it works that's so weird

[Eric Wieser]

In particular, this means instance : ForM Id _ _ requires you to implement ForM for any possible Monad Id, not just the canonical one.

[Eric Wieser]

lean4#10204 tries removing it

[François G. Dorais]

It is odd looking but it allows for the Monad m instance to be defined after the ForM instance.

[Aaron Liu]

François G. Dorais said:

It is odd looking but it allows for the Monad m instance to be defined after the ForM instance.

You can do that without hard-coding it into ForM

def myMonad := sorry

instance [Monad myMonad] : ForM myMonad foo bar := sorry

instance : Monad myMonad := sorry

[Eric Wieser]

Note that nowhere in core or batteries does this

[François G. Dorais]

You're totally right! I guess it just prevents hard-coding the monad. I don't know whether there is a good reason to do that.

[Eric Wieser]

I think this is pretty clearly the wrong way to use typeclasses generally, and if this was deliberate it was a hack to make elaboration behave better

[Eric Wieser]

(there is a small elaboration regression that impacts two lean4 tests where the type of the monad cannot be inferred from the outside in)