Zulip Chat Archive

Stream: lean4

Topic: Repr instance for functions


Sébastien Michelland (Mar 24 2022 at 14:08):

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 (Mar 24 2022 at 15:59):

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 (Mar 24 2022 at 16:08):

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

Sébastien Michelland (Mar 24 2022 at 16:09):

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 (Mar 24 2022 at 16:17):

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 (Mar 24 2022 at 16:18):

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 (Mar 24 2022 at 16:30):

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 (Mar 24 2022 at 16:33):

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 (Mar 24 2022 at 16:45):

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 (Mar 24 2022 at 16:53):

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!


Last updated: Dec 20 2023 at 11:08 UTC