Monad variable puzzle

Stream: lean4

[Damiano Testa]

In what is below, noMonad does not use [Monad m].

import Lean.Environment

open Lean

variable {m : Type → Type} [Monad m]

def noMonad [MonadEnv m] : m Environment := do getEnv

/-- info: noMonad {m : Type → Type} [MonadEnv m] : m Environment -/
#guard_msgs in
#check noMonad

What happens if you remove [Monad m] from variable?

[Edward van de Meent]

ah. i guess that sortof makes sense?

[Edward van de Meent]

not really, but sortof?

[Damiano Testa]

I probably agree: I am still undecided on whether I think that it is cool or that it should not work.

[Edward van de Meent]

i guess MonadEnv basically is a misnomer compared to what it does?

[Edward van de Meent]

and we can either change the way it works, or its name?

[Damiano Testa]

I'm not sure that it is MonadEnv that is at fault there. You can get a similar outcome with other MonadXXX classes.

[Edward van de Meent]

it makes sense that you'd expect MonadXXX to be somehow related to Monads?

[Edward van de Meent]

so either we make them be related, or we change the name?

[Damiano Testa]

I am not sure that there is anything to be changed, I just find the rules for inclusion of variables in declaration surprising, that's all.

[Edward van de Meent]

i guess there's two surprises here. the first is that, despite the fact that Monad m doesn't get used here, its existance as an assumption is required in order to allow do notation. The second is that using a MonadEnv assumption doesn't somehow require you to have Monad already (resulting in the error with do notation when you remove the Monad assumption, rather than an error at MonadEnv).

[Damiano Testa]

Yes, but I am not too surprised to find out that MonadXXX does not actually require Monad.

[Edward van de Meent]

but it's in the name?

[Edward van de Meent]

it doesn't make sense as a class without?

[Damiano Testa]

To me, the name suggests that Monad will be relevant, which it is. As for making sense... Lean is happy with it, so I'm happy to accept that it does make sense! :upside_down:

[Kyle Miller]

I wonder if there are other typeclasses that you need to have present to elaborate but do not appear in the final type.

[Damiano Testa]

I do not know: I found out about this since the "unused variable command linter" that I am writing told me that Monad m was not needed and when I went to remove it, I got slapped!

[Damiano Testa]

(The specific MonadXXX that was being used was MonadMCtx, though this is probably irrelevant.)

[Damiano Testa]

See docs#Mathlib.Tactic.modifyMetavarDecl.

[Damiano Testa]

In that case, removing Monad m and do is an option! :smile:

[Damiano Testa]

I am not sure if there are some unexpected consequences in the removal, but #18420 is a PR making the linter happier.

[Kyle Miller]

Looks good, there are no consequences to that

[Kyle Miller]

Incidentally I was just noticing that MonadEnv didn't need Monad a few days ago

[Damiano Testa]

If I find more surprising removals, I will flag them, but so far all the removals have been pretty boring: a file has been split, variables have been copied, but are now unused. Mostly.

[Damiano Testa]

Kyle Miller said:

Incidentally I was just noticing that MonadEnv didn't need Monad a few days ago

I view this a little like when in mathlib you define "local rings" and there is nothing "local" about them: in my mind, the fact that MonadXXX may not require Monad seems just an implementation detail.