Imperative catches

Stream: metaprogramming / tactics

[Mirek Olšák]

While imperative programming features (let mut, break) are convenient, and especially helpful to people not used to functional code, there are a bunch of well known catches.

import Lean.Meta.Basic
import Qq
open Lean
open Qq

def x : Meta.MetaM Unit := do
  let mut x : Bool := true
  let l : List Nat := [1,2,3]
  let l2 : List Nat ← l.mapM fun x => do
    pure (x + 3)
    -- x := false -- not compatible with monadic functions
  Meta.withTransparency .reducible do
    logInfo "hello"
    -- x := false -- annoyingly including context modifications
  let e : Q(Nat) := q(1 + 2)
  match e with
  | ~q($a + $b) => logInfo "sum"
  | _ =>
    logInfo "not a sum"
    -- x := false -- or Qq match

I was curious if there is any plan to something with that. My intuitive expectation would be that e.g. let mut should create something like StateT, and program flow commands such as break / return something like ExceptT. Are there reasons why it is not the case? Efficiency? Breaking / too slow type inference?

One of the reasons I am asking is that I thought if commands like run_cmd could run each line under a different Ref, so for example:

run_cmd
  logInfo "A"
  logInfo "B"

would shows "A", "B" on the corresponding lines rather than all at the first line run_cmd. I could imagine running each line with withRef but I am unsure how to make it compatible with imperative programming features.

[Kyle Miller]

The logInfo problem wouldn't be helped by adding withRef to each line. This is a compile-time/run-time staging problem. At runtime, the ref is not going to be the source code being run, but instead whatever the ref happens to be in the monad reader context. The run_cmd elaborator sets the ref to run_cmd before evaluating the compiled code.

The easiest solution to this is probably making a macro for logging that's specifically for #eval/run_cmd/etc., which captures the ref and quotes it to produce a logInfoAt syntax.

[Kyle Miller]

Mirek Olšák said:

I was curious if there is any plan to something with that

I've heard some ideas before about being able to extend what counts as control flow for do notation. I don't know much about it though, other than that rewriting do notation is one of this year's tasks for the FRO, so we'll finally start seeing some improvements in this area.

[Kyle Miller]

Kyle Miller said:

making a macro for logging

Quick example of this:

import Lean

open Lean

deriving instance ToExpr for String.Pos
deriving instance ToExpr for Substring
deriving instance ToExpr for SourceInfo
deriving instance ToExpr for Syntax

elab tk:"log_info_here!" s:interpolatedStr(term) : term => do
  let refExpr ← Elab.Term.exprToSyntax (toExpr tk)
  let stx ← ``(logInfoAt $refExpr m!$s)
  Elab.Term.elabTerm stx none

run_cmd do
  let mut x : Nat := 1
  log_info_here! "msg {x}"
  x := 2
  log_info_here! "msg {x}"

The messages are localized to each log_info_here!

[Kyle Miller]

This must not be used in compiled code that gets run in a different module.

It would be kind of neat though if there were an option you could set where all the debug messages that could appear in the current file do appear in the current file. I've definitely wanted this before, though with unique enough trace messages you can figure out where everything's coming from, so it's not blocking debugging things.

[Eric Wieser]

This must not be used in compiled code that gets run in a different module

Could you elaborate on why?

[Kyle Miller]

It will show the error in the current file, using whatever source range was compiled into the function.

I forget the exact number, but it would be like the "line 45 problem" in Lean 3, where certain errors showed up at a specific spot in the current file, because that's the line the macro was defined on in another file.

[Kyle Miller]

It's possible to detect that it's running from a different module (assuming you have access to the environment), and you could choose some policy, like "don't log" or "log at the current ref instead", but the point is that you can't use the prototype above as-is as a general solution.

[Mirek Olšák]

Kyle Miller said:

The logInfo problem wouldn't be helped by adding withRef to each line. This is a compile-time/run-time staging problem. At runtime, the ref is not going to be the source code being run, but instead whatever the ref happens to be in the monad reader context. The run_cmd elaborator sets the ref to run_cmd before evaluating the compiled code.

The easiest solution to this is probably making a macro for logging that's specifically for #eval/run_cmd/etc., which captures the ref and quotes it to produce a logInfoAt syntax.

This is not exactly how I imagine it should work. When I have an arbitrary function calling some logInfo's inside, it makes more sense to see the messages on that line rather than at the top. But thanks for the example, this is what I meant by inserting withRefs (which in general could break do syntax if I wanted to do it more automated)

elab "withRefHere" s:term : term => do
  let refExpr ← Elab.Term.exprToSyntax (toExpr s.raw)
  let stx ← ``(withRef $refExpr $s)
  Elab.Term.elabTerm stx none

def helloWorld : Lean.Elab.Command.CommandElabM Unit := do
  logInfo "hello world!"

run_cmd do
  withRefHere helloWorld

[Mirek Olšák]

Kyle Miller said:

Mirek Olšák said:

I was curious if there is any plan to something with that

I've heard some ideas before about being able to extend what counts as control flow for do notation. I don't know much about it though, other than that rewriting do notation is one of this year's tasks for the FRO, so we'll finally start seeing some improvements in this area.

Good to hear that Lean's FRO sees the do notation as worth improving.

[Mirek Olšák]

Actually, maybe it doesn't break do notation if I only wrap insides of all the do commands.

[Kyle Miller]

Mirek Olšák said:

this is what I meant by inserting

I understood that, but I was suggesting something else that seemed better (inserting withRefHeres automatically is interesting, but it also seems like it might lead to surprising behaviors — still, doesn't hurt to try it out).

The example with putting the message on the line in the run_cmd does clarify what you're going for.

Maybe you could look at all the possible doElems and evaluate which ones you can put withRefHere in front of, or into. Presumably you'd also want it inside (<- ...) term notation.