With notation for context managers

Stream: general

[Eric Wieser]

Eric Wieser said:

Though maybe the answer is "frame everything in a way suitable for with", just as we already do for for

I guess this also reveals a hack for using for to implement with

[Eric Wieser]

import Lean
import Qq

open Lean Meta Qq

section with_notation

/-- Typeclass to provide `with ctx as v` notation in the monad `m`, where `ctx : ρ` and `v : α`. -/
class WithNotation (m : Type → Type) (ρ : Type) (α : outParam Type) where
  with_ {β : Type _} [Monad m] (xs : ρ) (f : α → m (ForInStep β)) : m β

structure WithHandler (α) where handler : α

instance [WithNotation m ρ α] : ForIn m (WithHandler ρ) α where
  forIn ctx v f := WithNotation.with_ ctx.handler fun a => f a v

macro "with" t:term "as" v:ident "do" body:doSeq : doElem => `(doElem| for $v in WithHandler.mk $t do $body)

end with_notation

/-! Example usage -/

structure LocalDeclCtx where
  name : Name
  bi : BinderInfo
  ty : Expr

instance : WithNotation Lean.Meta.MetaM LocalDeclCtx Expr where
  with_ ctx f := do
    return (← withLocalDecl ctx.name ctx.bi ctx.ty f).value

run_meta do
  with LocalDeclCtx.mk `foo default q(Nat) as v do
    Lean.logInfo v

[Joe Hendrix]

There may be a generic way to handle this for callbacks in monads with call/cc, but I think otherwise interface changes would be needed.

Indeed, that's a nice observation on using for.

[Eric Wieser]

Another example:

structure TheReaderOf (α : Type) where
  val : α → α

abbrev theReader := @TheReaderOf.mk

instance [MonadWithReaderOf ρ m] : WithNotation m (TheReaderOf ρ) Unit where
  with_ ctx f := do
    return (← withTheReader ρ ctx.val (f ())).value

#eval show IO Unit from ReaderT.run (do
  with theReader (fun x : Nat => x + 1) as _x do
    IO.println s!"{← read}"
  ) (1 : Nat)

[Jovan Gerbscheid]

That is so cool! And the as clause could be made optional for cases like withReader, so that it would just be with ... do ...

[Joe Hendrix]

That's pretty nice. Syntactically, it seems like it may be good to match let if, with let x := do.

[Eric Wieser]

Jovan Gerbscheid said:

That is so cool! And the as clause could be made optional for cases like withReader, so that it would just be with ... do ...

I tried this and got annoyed with the syntax ambiguity, but I imagine it's not too hard to fix

[Eric Wieser]

A particularly useful context manager to have would be python's ExitStack, which seems more work to build here

[Notification Bot]

8 messages were moved here from #general > Discussion: Lean FRO roadmap, year 3 by Eric Wieser.

[Jovan Gerbscheid]

Wouldn't it be possible to make it work without any special type class, but just passing the function directly? So

with withLocalDecl `foo default q(Nat) as v do
    Lean.logInfo v

and

#eval show IO Unit from ReaderT.run (do
  with withReader (fun x : Nat => x + 1) do
    IO.println s!"{← read}"
  ) (1 : Nat)

[Eric Wieser]

I think there's value in the type wrapper, just as there is for for

[Jovan Gerbscheid]

With for the actual implementation is usually quitecomplicated, because of it has to be recursive. With with, I want to be able to do this using any function that has the same type as withReader (fun _ => _), without needing to define a separate structure for each function.

[Eric Wieser]

I guess the question is whether you want to be able to write things like with someFileHandle for automatic closing, etc

[Jovan Gerbscheid]

Are you're saying that this kind of file handling can't be described by a function that has a similar type to withLocalDecl?

[Eric Wieser]

No, I'm saying that you're losing the option to have an implicit conversion happen. You could also imagine a world where you have to write for x in myArray.iter instead of for x in myArray, where ForIn also only works directly with a (complex) function type