A nice revelation about meta code

Stream: lean4

[Sebastian Reichelt]

After struggling with some meta code involving lots of Exprs that need to be passed around correctly, I found a nice solution that I'd like to share. Not sure if the benefit can be seen from these simple examples; in my use case it was more like hours of debugging vs. getting it to work on the first try.

The main idea is to annotate the Expr type with an Expr instance that specifies the (expected/inferred/...) object-level type. This annotation doesn't really do anything by itself, but it makes that second Expr known to the elaborator.

-- Although `α` is completely superfluous, we can use it to infer arguments.
@[reducible] def TypedExpr (α : Expr) := Expr

-- For `α : Expr`, introduce `a : α` as a shorthand for `a : TypedExpr α`.
scoped instance : CoeSort Expr Type := ⟨TypedExpr⟩

As an example, here is how you could write mkEq from AppBuilder.lean using TypedExpr and its CoeSort:

def mkEq' {u : Level} {α : mkSort u} (a b : α) : mkSort levelZero :=
  mkApp3 (mkConst ``Eq [u]) α a b

def mkEqRefl' {u : Level} {α : mkSort u} (a : α) : mkEq' a a :=
  mkApp2 (mkConst ``Eq.refl [u]) α a

So instead of determining u and α at runtime like mkEq does, mkEq' takes them as implicit arguments. This isn't much of a change (though maybe a bit more efficient?) -- the real benefit arises from attaching type classes to such terms, e.g.

-- Reflect the type class `Inhabited` as a type class on the meta level.
class _Inhabited {u : Level} (α : mkSort u) where
(s : mkApp (mkConst ``Inhabited [u]) α)

-- Make an instance of `_Inhabited` directly usable as an expression.
instance {u : Level} (α : mkSort u) : Coe (_Inhabited α) Expr :=
  ⟨λ s => s.s⟩

-- Reflect `Inhabited.default`.
def _Inhabited.mkDefault {u : Level} (α : mkSort u) [s : _Inhabited α] : α :=
  mkApp2 (mkConst ``Inhabited.default [u]) α s

Then code like this tends to just work as soon as it compiles:

def example_defaultEqSelf {u : Level} (α : mkSort u) [_Inhabited α] :=
  mkEq' (_Inhabited.mkDefault α) (_Inhabited.mkDefault α)

Note how the instance of _Inhabited α is automatically passed on to _Inhabited.mkDefault (of course), and especially how the two implicit arguments of mkEq are inferred automatically because _Inhabited.mkDefault is defined to return α (i.e. TypedExpr α).

Finally, instances of such reflected type classes can easily be sythesized on the spot, like this:

example {u : Level} (α : mkSort u) : MetaM (mkSort levelZero) := do
  let s : _Inhabited α := ⟨← TypedExpr.synthesize⟩  -- `TypedExpr.synthesize` defined in the obvious way
  example_defaultEqSelf α

Here is a gist with the entire example code: https://gist.github.com/SReichelt/860ec32e85e05311cc51a5b10b70dfef
I guess it could be ported to Lean 3, but I haven't tried.

There are some aspects that could be improved. For instance the CoeSort on Expr might be a bit far-reaching. It would be nice to define

class IsTypeExpr (e : Expr)

and restrict that coercion to all (e : Expr) [IsTypeExpr e]. But for me, it already worked exceptionally well.

[Gabriel Ebner]

The idea sounds very much like this library: https://github.com/gebner/quote4/

[Sebastian Reichelt]

Oh, indeed, oops! Although I had seen some discussions about expression quotation, I didn't realize that your library also did type inference like this. Very nice. :-)
I think the type class aspect is a bit different, but I'm not sure. In https://github.com/gebner/quote4/blob/master/examples/typeclass.lean, I don't quite understand whether the second q(inferInstance) is guaranteed to refer to the instance that has been synthesized in the line before. Also, I'm wondering how q(Inhabited.default) picks up inst in the definition of typeClassArgument. I guess the macros are basically meta-meta code that automatically picks up variables from the context of the meta code?

Just for comparison, in my case I'd use a type class on the meta level, somewhat like:

def typeClassArgument (α : Q(Sort u)) [inst : Q(Inhabited $α)] : Q($α) :=
  q(Inhabited.default)

And then inst would be inferred from context when using typeClassArgument. Since I have quite a few such type class instances floating around, it's nice to pass them implicitly from function to function.

[Gabriel Ebner]

In an early version, I used a structure for Q(Inhabited $a) and you could indeed use it as [Q(Inhabited $a)]. But this no longer works after switching to a definition.

[Gabriel Ebner]

I guess the macros are basically meta-meta code that automatically picks up variables from the context of the meta code?

Yes, that is exactly what happens. If you have a Q(Inhabited Foo) in the local context, then Inhabited Foo is in the local context inside the quotation. (And will be used for type class synthesis.)

[Sebastian Reichelt]

Thanks a lot. I'll play around with your library over the weekend and then probably switch to it -- or maybe a slightly modified version of it. I really like how many things work magically in your quotations, but picking up arbitrary variables from the local context is a bit too magical for my taste. If I come up with something that I like better, does it make sense to open a PR to your repo? What are the plans regarding this library?

[Sebastian Reichelt]

Oh wait, I just realized that Lean will always use arbitrary variables to instantiate type classes. I had assumed that it would only look at type class instances. So the thing that seemed too magical to me is just normal Lean behavior.

[Gabriel Ebner]

Feel free to open issues and PRs! I have too many other things going on, but my plan is to clean up the code and integrate it in mathlib4. One interesting case study there would be to make a "type-safe" ring tactic. But while typed quotations are a key part of that, there's lots of additional complications.

For example you have a type HornerExpr of horner expressions and a function e : HornerExpr α → Q($α) that converts this representation into an actual expression. Importantly, you then have proofs of statements like $((xadd ....).e) = $(b.e) + $(c.e) where you need to unfold e. This works okay if e is a simple recursion, but the mathlib ring implementation is a bit more complicated.

Then there's the whole can of worms of pattern-matching. The Lean 3 expression pattern matching was purely syntactic, which means that 1) it won't unfold definitions (but in Lean 4 we now use reducible definitions more and more, for example x>y should always be interchangeable with y<x), and 2) it won't complain if you use the wrong type-class instances (which leads to nasty bugs like https://github.com/leanprover/lean4/issues/755). The quote4 library provides the syntax match e with | ~q($b + $c) => .. which is implemented using the Lean 4 unifier. But the implementation is horribly ugly and inflexible. For example: what type should b have? I have a Semiring α instance in the context, should it check that the + is the same as the + from the instance or should I get a new HAdd instance? I'm tending to think that it would be better to have the user explicitly specify the free variables like letmvar (b c : α) [CommRing α]; letdefeq ‹Semiring α› = ‹CommRing α›; .... This is all a bit complicated because you need to do the matching with an increased mctx depth, after matching e should be replaced by a + b, etc...

Did I mention rewriting the motive after a pattern match? This is another issue I ran into when trying it out on ring. There was something like structure Foo (α : Q(Sort u)) where bla : Q(α) which looks fine, compiles fine, but if α and β are def eq expressions, then Foo α and Foo β are not even equal.

[Patrick Massot]

What would be the goal of a "type-safe" ring tactic? Would it have less bugs? Would it be faster?

[Gabriel Ebner]

Right, ring has a lot of code like this:

      return (t, c.cs_app ``horner_mul_horner
        [a₁, x₁.1, n₁.1, b₁, a₂, n₂.1, b₂, aa, haa, ab, bb, t, h₁, h₂, h₃, h₄, H])

Each of these arguments needs to have the correct type. With typed quotations, 1) you can leave out half of the arguments because they can be filled in automatically, 2) the type of the expressions is clear from the type (i.e., it's not just Expr but an Expr with type a1*a2=ab), 3) the types of the arguments are checked at compile time (these bugs pop up from time to time even though the tactics are well-tested, see e.g. #4682).

[Gabriel Ebner]

Performance-wise, the mathlib ring and norm_num tactics use a lot of custom caching (this is the reason why all lemmas used by these tactics can only have a single type-class argument). Even with this caching, the cs_app call above still needs to do type inference and unification. The typed quotations do not need to do any type inference or type class synthesis when constructing expressions.

[Mario Carneiro]

cs_app shouldn't be doing any type inference or unification AFAIK, that's the whole point

[Mario Carneiro]

it's just using expr constructors

[Sebastian Reichelt]

I'm tending to think that it would be better to have the user explicitly specify the free variables

If I wanted to use pattern matching in my use case, I think that I'd quickly run into a situation where I need to supply some variables from the context and introduce (typed) metavariables for the rest. So what you are describing looks like a useful feature to me (though at the moment I'm content with isDefEq).

There was something like structure Foo (α : Q(Sort u)) where bla : Q(α) which looks fine, compiles fine, but if α and β are def eq expressions, then Foo α and Foo β are not even equal.

I have a somewhat similar situation in some places, but just in the sense that I need to convert an f : Foo α to Foo β. Since everything is just an Expr in reality (which is why you write "type-safe" in quotation marks, right?), this particular case is easily solved by writing ⟨f.bla⟩. But I can imagine that pattern matching introduces cases that are a lot more tricky.