Monad `Of` classes

Stream: lean4

[Mac]

Many of the monad extensions classes (ex. MonadReader, MonadState, MonadExcept) have Of variants (ex. MonadReaderOf, MonadStateOf, MonadExceptOf). The non-Of variants are outParam in their respective value type (ex. ρ, σ, ε) whereas the Of variants are not. For example:

class MonadReaderOf (ρ : Type u) (m : Type u → Type v) where
  read : m ρ

class MonadReader (ρ : outParam (Type u)) (m : Type u → Type v) where
  read : m ρ

This means, theoretically, there can be multiple instances of the Of class that are disambiguated by their value. However, the instances of non-Of variant are currently inferred from the instances of their Of variant.

instance (ρ : Type u) (m : Type u → Type v) [MonadReaderOf ρ m] : MonadReader ρ m where
  read := readThe ρ

This inhibits one from defining multiple instances of the Of variant (ex. MonadReaderOf) because this will create overlapping instances of the non-Of variant (ex. MonadReader) which clash in their outParam (ex. ρ).

I am curious why definitions like the following were not used instead:

@[defaultInstance]
instance (ρ : Type u) (m : Type u → Type v) [MonadReader ρ m] : MonadReaderOf ρ m where
  read := read

This would allow there to be other instances of the Of variant without clashing instances of the non-Of variant while still defaulting the Of variant to the one defined (if any) non-Of variant.

I imagine there might be other considerations that I may be missing and would thus be interesting in learning what, if any, they are.

[Sebastian Ullrich]

Solution: just don't be afraid of overlapping instances :) . Mathlib users have long learned how to cope with them, and Lean explicitly supports you in it with support for instance priorities etc. It's not super elegant, but perfectly manageable in practice afaict.

[Mario Carneiro]

I also don't really understand the motivation behind these classes. Which should we implement, and how should generic lemmas look? What are the use cases for the Of version?

[Sebastian Ullrich]

The use case is accessing different instances of the same effect in a stack. https://github.com/leanprover/lean4/blob/27d52a352fad12ef04026ebe4becbb4f30bac645/src/Lean/Elab/Term.lean#L298

[Sebastian Ullrich]

For a specific, new monad you should implement the Of version only. Since this instance will be "after" the transitive Of instance, the non-Of instance will prefer it, i.e. access the outermost effect by default.

[Sebastian Ullrich]

I imagine lemmas as well should be written for the Of version since that is the more general one, then possibly copied to the non-Of version.

[Mario Carneiro]

Heh, I mean lemma and generic (higher order) program interchangeably :sweat_smile:

[Mario Carneiro]

I don't know how actually suitable for proving the monad stack things are. It's pretty rare to have something interesting to prove about them

[Mac]

Sebastian Ullrich said:

Solution: just don't be afraid of overlapping instances :) . Mathlib users have long learned how to cope with them, and Lean explicitly supports you in it with support for instance priorities etc. It's not super elegant, but perfectly manageable in practice afaict.

The problem here is not overlapping instances. They are fine and I like them. The problem is that the non-Of don't support overlapping instances because of the outParam. If you define a new overlapping Of instance it will hide the current non-Of variant and prevent its usage (without explicit providing the instance of the class).

[Sebastian Ullrich]

It's hard to follow your description without an example. If you want to declare a new Of instance but not make it the default one for the non-Of instance, lower its priority.

[Mac]

I was working on an #mwe example when you posted that. Here it is:

universe u

instance {α β : Type u} : MonadStateOf α (StateM (α × β)) where
  get := do (<- get).1
  set a := modify $ Prod.map.{u,u,u,u} (fun _ => a) id
  modifyGet f := modifyGet fun st => f st.1 |>.map id
    fun a => st.map (fun _ => a) id

def getState : StateM (String × Nat) (String × Nat) :=
  get -- Errors: failed to synthesize instance `MonadState (String × Nat) (StateM (String × Nat))`

Thus, with the new instance, I can no longer get the original state. This would not happen in the alternative formulation proposed above.

[Mac]

Also do note that the above example is rather trivial, but I did encounter this same issue in a more complex real world while working on coding the build system.

[Mac]

As a side note, I am also confused as to why providing explicit universes to Prod.map is necessary.

[Sebastian Ullrich]

I don't think your proposal would work with the transitive [MonadLift] Of instances, so please use instance (priority := low)

[Sebastian Ullrich]

I don't know about the universe issue

[Mac]

Sebastian Ullrich said:

I don't think your proposal would work with the transitive [MonadLift] Of instances, so please use instance (priority := low)

Oh, by bad, didn't know you could specify instance priorities like that. Cool! I am curious about the MonadLift concern. If possible, could you elaborate what you mean (i.e., what the issue is)?

[Sebastian Ullrich]

No, I'm afraid I can't elaborate on every posted proposal to show why I don't think it will work. The burden would be on you to show that you have considered all uses (or at least the ones pointed out) of the current design and how to do them in the new one. Or neither one of us does it and we accept the status quo :) .

[Mac]

That's understandable.