do notation for reader monads

Stream: lean4

[Eric Wieser]

Would it be possible to extend do notation to support Reader monads? That is, have syntax for

import Lean

abbrev MyMonad := ReaderT Nat IO

def main : MyMonad Int := do
  let mut i := 1
  withReader (fun x => x * 2) do
    i := i + (← read)  -- error, `i` is not in the right do block
  return i

which performs the necessary transformation to modify i within the reader monad then copy it back out?

[Mario Carneiro]

there is a general mechanism for supporting combinators, but it's not exposed at the user level, which means you have to modify Do.lean to do it

[Mario Carneiro]

and in the past I have gotten a lot of pushback on making any changes to Do.lean

[Eric Wieser]

Having user-accessible hooks for such combinators would I think also resolve a large class of Qq bugs

[Kyle Miller]

I don't think changes to Do.lean would be welcome at the moment, but if there were a solid RFC that proposes how to get mut variables to cross into combinators, that would would be a great first step.

One question I have is whether a goal would be to have return work inside these combinators. I think it would be a necessary feature, since otherwise it would be confusing having the dos only partially connected, but this would be a large breaking change, with a lot of code that would need to be carefully re-reviewed.

[Eric Wieser]

I agree that return and let mut should be handled at the same time

[Joachim Breitner]

I wanted this before as well, but my main worry here is predictability. A user should be able to look at some code and have a reasonable chance of understanding which monadic effects reach where (without having to hover every single return or throw).

Is it possible today to extend the do notation with custom per-combinator syntax in a library, e.g. for withReader?

Or maybe there could be generic syntax that makes it clear what's happening, e.g.

under withReader (...) do

where under ... do is syntax and expects a (polymorphic enough) monad combinator. But then one would want to generalize that to combinators taking multiple monadic actions, or some with arguments... And there is the risk that there result will be too hard to understand, and we'll lose users to perl6 for its simple syntax.

[Eric Wieser]

I think my request here is not to have direct support for arbitrary combinators, but for it to be possible to extend the do syntax from outside core for particular combinators

[Eric Wieser]

So with_reader syntax rather than directly handling the withReader function

[Mac Malone]

I have a work-in-progress extensible do syntax over at tydeu/imperia, but it is not ready for prime time yet. I probably could implement a PoC of this idea (either in the with_reader or under form) there soon (e.g., in a weekend or two).