General quotation mechanism to convert a term into `Expr`

Stream: metaprogramming / tactics

[David Deng]

Is there a general way in Lean to translate a normal term into its meta-level equivalent, an Expr? Essentially, I am looking for a functionality similar to Agda's quote and MetaCoq's tmQuote.

[Kyle Miller]

docs#Lean.ToExpr

[David Deng]

Thanks! It works great for primitive types. And I wonder if I want to extend it to work also for functions, what should I do in their implementation? For example,

def plus (n: Nat) (m: Nat) : Nat := n + m
#eval Lean.ToExpr.toExpr plus -- failed to synthesize ToExpr (Nat → Nat → Nat)

instance : ToExpr (Nat → Nat → Nat) where
  toExpr     := sorry -- what should I use here?
  toTypeExpr := sorry -- And here?

[Kyle Miller]

There's no way to do that — is that something that Agda/MetaCoq can somehow do? If so, I'm curious what they're doing.

[David Deng]

So MetaCoq is using Ffix to denote recursive constructs in the meta program:

Check plus. (* : forall (_ : nat) (_ : nat), nat *)
Compute tmQuote plus.
(* = @tmQuote (forall (_ : nat) (_ : nat), nat) *)
(*          (fix Ffix (x x0 : nat) {struct x} : nat := *)
(*             match x return nat with *)
(*             | @O => x0 *)
(*             | @S x1 => S (Ffix x1 x0) *)
(*             end) *)
(*      : TemplateMonad term *)

I believe Agda can do something similar based on one usage of quote _+_ in their documentation https://agda.readthedocs.io/en/latest/language/reflection.html

[Kyle Miller]

Ah, ToExpr is for turning runtime values into Exprs, but do I have it right that Agda's quote is taking the compile-time expression and turning it into an expr that represents the Expr?

[Kyle Miller]

(That's why ToExpr (Nat -> Nat -> Nat) can't possibly work — how do you take an arbitrary run-time closure and reflect it to an Expr? But there's no problem if you're working with Expr and only Expr.)

[Kyle Miller]

Mathlib has a ToExpr Expr instance, and with it you can do

import Mathlib.Tactic.ToExpr

open Lean Elab Meta

elab "quote_expr% " t:term : term => do
  let e ← Term.withSynthesize <| Term.elabTerm t none
  return toExpr (← instantiateMVars e)

#check quote_expr% fun a b : Nat => a + b
/-
Expr.lam `a (Expr.const `Nat [])
  (Expr.lam `b (Expr.const `Nat [])
    (((((((Expr.const `HAdd.hAdd [Level.zero, Level.zero, Level.zero]).app (Expr.const `Nat [])).app
                      (Expr.const `Nat [])).app
                  (Expr.const `Nat [])).app
              (((Expr.const `instHAdd [Level.zero]).app (Expr.const `Nat [])).app (Expr.const `instAddNat []))).app
          (Expr.bvar 1)).app
      (Expr.bvar 0))
    BinderInfo.default)
  BinderInfo.default : Expr
-/

[Kyle Miller]

Anyway, that's the idea. If you want the behavior where it takes an identifier instead of an expression and quotes the declaration's definition, that's easy to do as well.

[David Deng]

Kyle Miller said:

Ah, ToExpr is for turning runtime values into Exprs, but do I have it right that Agda's quote is taking the compile-time expression and turning it into an expr that represents the Expr?

I am not familiar with the internals of a proof assistant. Would you mind explaining me a bit more on what is runtime and what is compile-time? What is the essential difference between a runtime closure and a compile-time function?

[David Deng]

Kyle Miller said:

Anyway, that's the idea. If you want the behavior where it takes an identifier instead of an expression and quotes the declaration's definition, that's easy to do as well.

Yes. I think that would be what I wanted to do. The mathlib example looks great, but do I need the library in order to reflect an identifier's definition?

[Kyle Miller]

By "compile time expression" I'm loosely referring to meta representations of values, like Expr or maybe Syntax. This is the representation that elaboration makes use of, but an Expr whose type is computed to be an Expr that represents Nat -> Nat -> Nat is not itself an executable function.

By "runtime" I'm meaning the terms of a type after code extraction. So for example, a term of Nat -> Nat -> Nat in this case is more-or-less machine code. If you are running a program that makes use of terms of Nat -> Nat -> Nat, there is no reflection of that value that you are allowed to do.

[Kyle Miller]

David Deng said:

but do I need the library in order to reflect an identifier's definition?

That's where there's a ToExpr Expr instance. If you don't want to use mathlib, you can try to extract the relevant code.

There's a project in progress to move this instance to core Lean, but you shouldn't expect it for the next release.

[Kyle Miller]

Could you say a bit about what you're doing? I'm worried you might be going into some direction here that's not how people normally do metaprogramming. It's very niche turning an Expr into an Expr that evaluates to the Expr.

[David Deng]

Kyle Miller said:

By "compile time expression" I'm loosely referring to meta representations of values, like Expr or maybe Syntax. This is the representation that elaboration makes use of, but an Expr whose type is computed to be an Expr that represents Nat -> Nat -> Nat is not itself an executable function.

By "runtime" I'm meaning the terms of a type after code extraction. So for example, a term of Nat -> Nat -> Nat in this case is more-or-less machine code. If you are running a program that makes use of terms of Nat -> Nat -> Nat, there is no reflection of that value that you are allowed to do.

I see what you are saying. I am not trying to do reflection on runtime terms.
I only want to "quote" the expressions based on their face value at the definition site, as in the examples above.

[David Deng]

Kyle Miller said:

David Deng said:

but do I need the library in order to reflect an identifier's definition?

That's where there's a ToExpr Expr instance. If you don't want to use mathlib, you can try to extract the relevant code.

There's a project in progress to move this instance to core Lean, but you shouldn't expect it for the next release.

Okay, that makes sense. Can you explain a bit more on what the elab command is doing here though?

elab "quote_expr% " t:term : term => do
  let e ← Term.withSynthesize <| Term.elabTerm t none
  return toExpr (← instantiateMVars e)

[Kyle Miller]

David Deng said:

I only want to "quote" the expressions based on their face value at the definition site, as in the examples above.

Could you explain more about what your application is?

[David Deng]

Kyle Miller said:

Could you say a bit about what you're doing? I'm worried you might be going into some direction here that's not how people normally do metaprogramming. It's very niche turning an Expr into an Expr that evaluates to the Expr.

Yeah, sure, though I guess what I am trying to do is indeed a bit unconventional. I am trying to embed another language using Lean's regular terms (e.g. functions), and then convert those terms in Lean into string format of its corresponding language. The reason that I want to use Lean's regular term as a host language is because its dependent type can be used to embed extra information (e.g. the stack length of a PostScript program) to verify program correctness.

In other words, I am trying to replicate https://dl.acm.org/doi/10.1145/3486609.3487201 in Lean. The original paper used Agda.

[Kyle Miller]

Term.elabTerm takes Syntax and elaborates it to an Expr. The withSynthesize function completes the elaboration, and in the end you have to be sure to instantiate metavariables that might still be present in the expression.

[Kyle Miller]

Having skimmed some of the paper, I'm having doubts that you want to use ToExpr Expr. All the examples in the paper using quote seem to be not much more than doing basic constructions for expressions.

[David Deng]

Kyle Miller said:

Term.elabTerm takes Syntax and elaborates it to an Expr. The withSynthesize function completes the elaboration, and in the end you have to be sure to instantiate metavariables that might still be present in the expression.

Thanks for the explanation -- mostly make sense to me.
Still,

1. What does the <| operator do?
2. How can a term contain uninstantiated meta variables if the term's definition is already available?

[Kyle Miller]

I think I'll have to direct you to resources such as https://leanprover-community.github.io/lean4-metaprogramming-book/ and https://lean-lang.org/functional_programming_in_lean/

The <| operator is $, it's like a ( that gets closed as late as possibel.

Metavariables are represented by Expr.mvar, and the table of assignments is part of the elaborator's state. Since everything is immutable, you need to do an explicit step to do the substitutions for all the assignments that have accumulated.

[David Deng]

Kyle Miller said:

Having skimmed some of the paper, I'm having doubts that you want to use ToExpr Expr. All the examples in the paper using quote seem to be not much more than doing basic constructions for expressions.

Well, I think the quote section of the paper is just giving an overview of Agda's reflection interface. In the repository, they do use quote to reflect functions whose type signature contains customly defined inductive structures, similar to the plus function above.

[Kyle Miller]

Is it that they're quoting an arbitrary function, or that there's a global constant?

[David Deng]

Kyle Miller said:

Is it that they're quoting an arbitrary function, or that there's a global constant?

I believe the latter. The function being quoted is defined as a global constant.

[Kyle Miller]

Yeah, that's what I was understanding from looking at the paper. In Lean you can access the environment and inspect constants' values. You can also refer to Expr.const ``nameOfConstant [..] where .. stands for any universe levels you might need.

There's also the Qq library do do this with some more compile-time typechecking.

[David Deng]

Kyle Miller said:

In Lean you can access the environment and inspect constants' values.

Are you referring to getLCtx? Can I inspect constant values if they are functions?

[Kyle Miller]

No, that's the local context, not the environment.

[Kyle Miller]

Here:

#eval do
  let info ← getConstInfo ``Nat.add
  logInfo m!"{info.value?}"
/-
fun x x_1 =>
  Nat.brecOn (motive := fun x => Nat → Nat) x_1
    (fun x f x_2 =>
      (match (motive := Nat → (x : Nat) → Nat.below (motive := fun x => Nat → Nat) x → Nat) x_2, x with
        | a, Nat.zero => fun x => a
        | a, b.succ => fun x => (x.1 a).succ)
        f)
    x
-/

[David Deng]

Kyle Miller said:

#eval do
  let info ← getConstInfo ``Nat.add
  logInfo m!"{info.value?}"

I got the following error:

▶ 71:3-71:36: error:
typeclass instance problem is stuck, it is often due to metavariables
  Bind ?m.2800

[David Deng]

Kyle Miller said:

(That's why ToExpr (Nat -> Nat -> Nat) can't possibly work — how do you take an arbitrary run-time closure and reflect it to an Expr? But there's no problem if you're working with Expr and only Expr.)

I don't think we are taking "arbitrary runtime closures," because toExpr : α → Lean.Expr also takes an object of type α that we want to reflect, and it should be possible for toExpr to analyze the structure of the object, reflecting it into an Expr object?

[Mario Carneiro]

I was recently discussing this kind of thing with some adga devs, because agda actually does support this (quoting runtime values into expressions) and it was a bit mind bending for me.

[Mario Carneiro]

The trick is that the evaluation of the metaprogram is happening via what we would call whnf or kernel evaluation, i.e. it's expression normalization rather than interpretation, and as a result all of the values are available in expression form. So when you normalize a call to the magic quote function it just grabs the expression it is applied to and quotes it into a deeply embedded expression value

[Mario Carneiro]

@David Deng the issue you are having with Kyle's code is solved by adding a type annotation (this is fixed on nightly and I think Kyle is on the development version), i.e. #eval show MetaM _ from do ...

[Mario Carneiro]

But for lean, reflecting objects of function type is not possible. toExpr is a typeclass function, so even if you call it someone has to implement it, and there is no way to implement an instance for ToExpr (A -> B) because that code receives only a runtime closure object, not an expression, and is somehow tasked with building an expression from the closure object

[Kyle Miller]

I'm wondering how impossible an (unsafe) ToExpr (A -> B) is — I imagine a sufficiently smart decompiler could trace runtime objects and figure out an expression that represents the function, though I'd hate to try to un-erase all the types, proofs, and type parameters.

[Kyle Miller]

But David, what Mario's saying is pointing toward how implementing that paper in Lean will probably look fairly different. In Lean, you can do computations with Expr directly and there's no need to quote, since the Expr is already an Expr.

[Henrik Böving]

Kyle Miller said:

I'm wondering how impossible an (unsafe) ToExpr (A -> B) is — I imagine a sufficiently smart decompiler could trace runtime objects and figure out an expression that represents the function, though I'd hate to try to un-erase all the types, proofs, and type parameters.

Doing such an unerasing just from runtime information for proofs seems impossible to me. A proof is just lean_box(0) (or sometimes not even that and just completely gone as a value), you cannot recover any information about it at all. So the unerasing procedure would need to be equivalent to writing a proof automatically. I guess it might be possible if you had access to the original Lean source code but even then it would be pretty horrific to implementz.

[Kyle Miller]

At least you know that there was a proof to begin with, so All You Need To Do:tm: is enumerate all expressions until you stumble across the proof :-)

[Mario Carneiro]

You can probably do it for a limited class of runtime types. This is, after all, exactly what Normalization by Evaluation (NbE) is about

[Mario Carneiro]

you may need to tweak some details of the interpreter, but it can definitely be done in principle if the system is cooperating with this goal

[David Deng]

Kyle Miller said:

But David, what Mario's saying is pointing toward how implementing that paper in Lean will probably look fairly different. In Lean, you can do computations with Expr directly and there's no need to quote, since the Expr is already an Expr.

But wouldn't that basically "force" all expressions to have the same type (e.g. Expr) and give up the ability to use Lean's dependent type checker to provide some sort of correctness guarantee?

[Eric Wieser]

You might be interested in the quote4 / import Qq library, which while providing no correctness guarantee, does make it easier to avoid typing mistakes