Repr instance for functions

Stream: lean4

[Sébastien Michelland]

I have an inductive type for programs with algebraic effects. I'd like to define a Repr instance for it that would more or less print it verbatim like #reduce does, and allow me to use the type with #eval. I have some tests that make whnf timeout and I'd like to study them with #eval, which apparently is a much faster VM.

The type looks like this:

inductive Program (E: Type → Type) (R: Type) where
  | Return (r: R): Program E R
  | Effect {T: Type} (e: E T) (k: T → Program E R): Program E R

I've been trying (unsuccessfully) to take as parameter a Repr instance on E (more specifically on E T for any T), and to have the continuation function printed as a Lean term. I can write [∀ T, Repr (E T)] as parameter, but I don't know how fragile it is nor how to actually define such an instance.

What would be the proper way to approach this problem? I'm not even sure I can print functions at all, which has me slightly worried.

[Chris B]

You probably want to just write a separate Repr/ToString instance instead of trying to put instance parameters on the inductive itself. There's no technical limitation that prevents you from printing functions, but I think in general it's going to be up to you to figure out how to display your function as a string in a way that makes sense. A function on lists might make sense in some context when displayed as f []:

instance {A : Type} [ToString A] : ToString (List A → List A) where
  toString f := s!"{f []}"

#eval (fun l => [0] ++ l ++ [1] : List Nat → List Nat)

So it looks like you would need to figure that out for T -> Program E R.

[Chris B]

Ah yeah, you do have a little bit of a problem with that T constructor arg though.

[Sébastien Michelland]

Thank you. The functions in Effect are quite arbitrary, and I wish to print the underlying term. I'm not sure how much introspection is needed for this, although I suspect a VM might compile/simplify the term for performance reasons and get rid of what I want to print (?).

[Chris B]

Some inspiration maybe:

inductive Program (E: Type → Type) (R: Type) where
  | Return (r: R): Program E R
  | Effect {T: Type} [Inhabited T] (e: E T) (k: T → Program E R): Program E R

partial def showProgram {E : Type → Type} {R : Type} [∀ T, ToString (E T)] [ToString R] : Program E R → String
| Program.Return r => toString r
| @Program.Effect _ _ T i e k =>
  let k' := k (@Inhabited.default T i)
  let p' := showProgram k'
  s!"{e}, {p'}"

instance {A : Type} : ToString (Option A) where
  toString o :=
    match o with
    | none => "none"
    | some x => "some"

def r : Program Option Nat := Program.Return 0
def p : Program Option Nat := Program.Effect (T := Char) (some 'a') (fun _ => r)
#eval showProgram p

[Sebastian Ullrich]

Sébastien Michelland said:

Thank you. The functions in Effect are quite arbitrary, and I wish to print the underlying term. I'm not sure how much introspection is needed for this, although I suspect a VM might compile/simplify the term for performance reasons and get rid of what I want to print (?).

Yes, the original term is gone at run time

[Sébastien Michelland]

Chris B said:

Some inspiration maybe

Thanks. It's not a bad compromise, but since most of the program logic is in the functions, an evaluation is probably not going to be enough for debugging.

I guess there is some XY going on there. Since the terms are gone at runtime and I want to print them, I don't really have a choice but to test with the kernel with #reduce. So maybe I should look first at why it timeouts. I tracked it down to a mutual definition (one that @Leonardo de Moura wrote for me the other day) and according to this post reducing anything with proofs inside is likely to lead to such problems (the proofs being some subterms related to the well-founded definition, I understand). Is there a way to work around this?

[Sebastian Ullrich]

You likely want the following TODO implemented so you can turn on skipProofs https://github.com/leanprover/lean4/blob/be7c71d1c8037a3a9aaa03b0f7d81259bb856712/src/Lean/Elab/BuiltinCommand.lean#L238-L240

[Sebastian Ullrich]

Customizing such smaller commands is relatively simple in Lean 4, here is a quick sketch that you can give a try:

import Lean

open Lean
open Lean.Parser.Term
open Lean.Elab.Command
open Lean.Elab
open Lean.Meta

elab "#reduce " skipProofs:group(atomic("(" &"skipProofs") " := " (trueVal <|> falseVal) ")") term:term : command =>
  let skipProofs := skipProofs[3].isOfKind ``trueVal
  withoutModifyingEnv <| runTermElabM (some `_check) fun _ => do
    dbg_trace term
    let e ← Term.elabTerm term none
    Term.synthesizeSyntheticMVarsNoPostponing
    let (e, _) ← Term.levelMVarToParam (← instantiateMVars e)
    -- TODO: add options or notation for setting the following parameters
    withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
      let e ← withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := skipProofs) (skipTypes := false)
      logInfo e

#reduce (skipProofs := true) id rfl

[Sébastien Michelland]

Excellent! I was setting up a Lean build to give it a try, but it's just as easy like this. Thanks again ^^

My terms can reduce properly now (fairly quickly too), so these proofs were indeed the problem. The result doesn't look nearly as clean as I expected (800 lines for a trivial program xD), I suspect there are some non-computable/non-reducible stuff left in my theory. Sounds like a different problem though!