Qq and reflecting meta-level values

Stream: lean4

[Alex Keizer]

I'm using Qq and I want to turn some i : Foo into a i : Q(Foo), so that I can use it in subsequent q/Q macros. I noticed that for n : Nat this just works, but for other types I get an unknown identifier error.

import Qq
open Qq

example (n : Nat) : Q(Nat) :=
  q($n)

example (i : Fin 2) : Q(Fin 2) :=
  q($i)
--   ^------ unknown identifier '«$i»'

Is Nat just hard-coded, or is there some typeclass I can implement to make this work?

[Eric Wieser]

Does docs4#Fin have a docs4#Lean.ToExpr instance?

[Eric Wieser]

In lean 3 it was docs#fin.reflect

[Eric Wieser]

I would guess we just dropped it when porting

[Alex Keizer]

Yeah, ToExpr is the typeclass I was looking for, after implementing it for Fin the error disappears

[Alex Keizer]

Is there a reason ToExpr takes Type u rather than Sort u? I implemented ToExpr (Fin n) by translating proofs of x < y to Expr, so I figured I could define ToExpr (x < y) as well, but that of course doesn't work if ToExpr only takes types.

import Qq

open Qq
open Lean (ToExpr)

def Nat.lt.toExpr : {x y : Nat} → (x < y) → Q($x < $y)
  | 0, 0, h     => by contradiction
  | 0, y+1, _   => q(Nat.zero_lt_succ $y)
  | x+1, y+1, h =>
      have h : x < y := Nat.lt_of_succ_lt_succ h
      let r : Q($x < $y) := toExpr h
      q(Nat.succ_lt_succ $r)

instance {n : Nat} : ToExpr (Fin n) where
  toExpr      := fun ⟨i, h⟩ => q(Fin.mk $i $(Nat.lt.toExpr h))
  toTypeExpr  := q(Fin $n)

[Kyle Miller]

Looks like we created effectively the same implementation in parallel:

open Lean in
/-- Returns a proof of a < b -/
def ltToExpr (a b : Nat) (h : a < b) : Expr :=
  match a, b with
  | _, 0 => (Nat.not_lt_zero _ h).elim
  | 0, b + 1 => .app (.const ``Nat.succ_pos []) (toExpr b)
  | a + 1, b + 1 =>
    let e := ltToExpr a b (Nat.lt_of_succ_lt_succ h)
    mkApp3 (.const ``Nat.succ_lt_succ []) (toExpr a) (toExpr b) e

open Lean in
instance : ToExpr (Fin n) where
  toExpr x := mkApp3 (.const ``Fin.mk []) (toExpr n) (toExpr x.1) (ltToExpr _ _ x.2)
  toTypeExpr := .app (.const ``Fin []) (toExpr n)

set_option pp.proofs true
#eval Lean.PrettyPrinter.ppExpr <| Lean.toExpr (3 : Fin 5)
-- { val := 3, isLt := Nat.succ_lt_succ (Nat.succ_lt_succ (Nat.succ_lt_succ (Nat.succ_pos 1))) }

[Kyle Miller]

Maybe ToExpr takes a Type _ because there's no runtime values associated to proofs (they're erased)?

We could use PLift here to create these sorts of instances anyway, at the cost of needing to insert some PLift.ups and PLift.downs:

import Qq

open Qq
open Lean

def Nat.lt.toExpr : {x y : Nat} → (x < y) → Q($x < $y)
  | _, 0, h     => (Nat.not_lt_zero _ h).elim
  | 0, y+1, _   => q(Nat.zero_lt_succ $y)
  | x+1, y+1, h =>
      let r : Q($x < $y) := toExpr (Nat.lt_of_succ_lt_succ h)
      q(Nat.succ_lt_succ $r)

instance {x y : Nat} : ToExpr (PLift (x < y)) where
  toExpr h := q(PLift.up $(Nat.lt.toExpr h.down))
  toTypeExpr := q(PLift ($x < $y))

instance {n : Nat} : ToExpr (Fin n) where
  toExpr      := fun ⟨i, h⟩ =>
    let h' : Q(PLift ($i < $n)) := toExpr <| PLift.up h
    q(Fin.mk $i (PLift.down $h'))
  toTypeExpr  := q(Fin $n)

[Arthur Adjedj]

Another possible reason might be that most terms in Prop can’t be eliminated to Type _, making ToExpr only useful for subsingleton types, for which the rendered expressions would be trivial anyway

[Kyle Miller]

I don't think that's explaining it -- all ToExpr p needs to do is synthesize a proof of p using the symbolic structure of p itself, given a proof of p. Look at how Nat.lt.toExpr is defined. It recurses on x and y, and then it only uses h when it's equivalent to False to be able to omit a case.

The situation seems to be similar to Decidable instances. In fact, one could imagine a typeclass DecideExpr p that synthesizes an expression for either a proof of p or a proof of not p, depending on which is true. Then given one of these you can just use that proof directly for a ToExpr instance (since you know ahead of time the DecideExpr instance will never produce the negation proof).

Edit: I suppose this is all to say that you're right that it's important that propositions are subsingletons, with the caveat that since typeclass inference can look at the symbolic structure of the proposition there's still a lot you can do.

[Alex Keizer]

Kyle Miller said:

Maybe ToExpr takes a Type _ because there's no runtime values associated to proofs (they're erased)?

That's true, but Expr isn't quite a runtime value yet. We do want to be able to construct expressions that correspond to proofs of Props (as witnessed by our implementations of ToExpr (Fin n)). The PLift trick is a cool workaround (thanks for showing it!), but for me it just reaffirms that it would be useful to have some built-in way to reflect a Prop.

Another possible reason might be that most terms in Prop can’t be eliminated to Type _, making ToExpr only useful for subsingleton types, for which the rendered expressions would be trivial anyway

That's fair, the translation cannot inspect the actual meta-level proof object, so maybe ToExpr is not the right class. Effectively, we just want to know that Q(p) is inhabited, for some p : Prop.

Possibly a solution is to special case Qq so that q($h) where the type of his a P : Prop instead tries to synthesize Inhabited Q($P)

[Kyle Miller]

Alex Keizer said:

That's true, but Expr isn't quite a runtime value yet.

I agree (and the PLift trick shows these sorts of instances aren't useless). What I meant is that I believe the intended use was to be able to #eval an expression and then toExpr it. We're sort of misusing it here (not to say that we shouldn't be allowed to misuse it!) because we're using the fact that typeclass inference is symbolic, so from the elaboration-time type we can get x and y.

[Eric Wieser]

Shouldn't Fin.toExpr generate ofNat like it did in Lean 3?

[Eric Wieser]

I thought the idea was that it generate the canonical expression, as opposed to the most efficient one

[Alex Keizer]

I mean, I just learned about ToExpr yesterday, so I'm maybe not the most qualified person on that subject, but it seems that for Qq's purposes it's beneficial to generate more efficient representations if we can. Compile-times are already not great, so if we can cut that down a bit, that seems good. (If there are other issues that I'm overlooking, please do tell me).

Now, since Kyle mentioned that maybe we're misusing ToExpr, I figured I could try making a dedicated QuoteExpr typeclass that does allow for Props. It also uses the QQ type-family for some extra type-safety (at the cost of flexibility with the universe)

/--
  Gives a meta-level representation of the universe in which some type `α` lives
-/
class QuoteUnivOf (α : Sort u) where
  /-- Object representing the universe of `α` -/
  quoteUniv : Level



/--
  Converts a value of type `α` into an expression that represents this value in Lean.

  This class differs from the built-in `ToExpr` in two ways:
    * It allows implementation for `α : Prop`, whereas `ToExpr` is only for `Type _`s
    * We use the `QQ` type family to assert the type of the returned expressions.
      This ensures this type information is available when implementors use the `q(⋅)` macro
      to construct the expression.
-/
class QuoteExpr (α : Sort u) extends QuoteUnivOf α where
  /-- Expression representing the type `α` -/
  quoteTypeExpr : QQ (Expr.sort quoteUniv)
  /-- Convert a value `a : α` into an expression that denotes `a` -/
  quoteExpr     : α → QQ quoteTypeExpr

With this class, we can write the following

import Qq.QuoteExpr
import Qq.Macro

open Lean (Level ToExpr)

namespace Qq

instance (α : Sort 0) : QuoteUnivOf α := ⟨Level.ofNat 0⟩
instance (α : Sort 1) : QuoteUnivOf α := ⟨Level.ofNat 1⟩


/--
  Define a fallback instance of `QuoteExpr` for implementors of `ToExpr`
-/
instance (priority := low) {α : Type u} [ToExpr α] [QuoteUnivOf α] : QuoteExpr α where
  quoteTypeExpr := ToExpr.toTypeExpr α
  quoteExpr a   := ToExpr.toExpr a



instance (a b : Nat) : QuoteExpr (a < b) where
  quoteTypeExpr := q($a < $b)
  quoteExpr := go where
    go {a b : Nat} (h : a < b) : Q($a < $b) := match a, b with
    | 0, 0      => by contradiction
    | 0, b+1    => q(Nat.zero_lt_succ $b)
    | a+1, b+1  =>
      have h := Nat.lt_of_succ_lt_succ h
      let h := go h
      q(@Nat.succ_lt_succ $a $b $h)


instance (n : Nat) : QuoteExpr (Fin n) where
  quoteTypeExpr := q(Fin $n)
  quoteExpr := fun ⟨i, h⟩ => q(⟨$i, $h⟩)

end Qq

[Alex Keizer]

Re: the universe flexibility. I think we do lose the flexibility to define universe polymorphic instances, since we have provide a Level object .
Is it possible to define some universe polymorphic quoteLevel.{u} : Level so that

quoteLevel.{0}  =  Level.ofNat 0
quoteLevel.{1}  =  Level.ofNat 1
quoteLevel.{2}  =  Level.ofNat 2
...

I would expect not.
Then again, I also wonder whether it's even possible to write a correct universe polymorphic ToExpr instance. Presumably, if the constructed expression indeed lives in some arbitrary universe u, the expressions contains a Level representation of this universe anyway.

[Eric Wieser]

We already have this, its docs4#ToLevel

[Alex Keizer]

Hmm, that link 404's

[Alex Keizer]

I found it at https://github.com/leanprover-community/mathlib4/blob/94c39a2c516923d789c4061d221b746708eed5dd/Mathlib/Tactic/ToLevel.lean
That one is indeed better than my attempt, thanks!
What I meant, though, is some definition of quoteLevel where even

universe u

quoteLevel.{u}

Would do the right thing, I expect this to be impossible

[Eric Wieser]

What would be the point?

[Eric Wieser]

Just write [ToLevel.{u}] as a hypothesis instead

[Eric Wieser]

In all the cases where you actually need it I think Lean will find the instance

[Alex Keizer]

Yeah, I also think ToLevel is enough, I was just wondering if I was overlooking something.
My definition of QuoteExpr \alpha (where \alpha : Sort u ) indeed depends on a ToLevel.{u} instance being found, whereas it is possible to define ToExpr \alpha without it. Hence, in theory, you lose some flexibility. In practice, I expect actually defining a correct ToExpr instance is impossible without ToLevel.{u}. Unless something like quoteLevel as I described it were possible

[Alex Keizer]

Alex Keizer said:

I mean, I just learned about ToExpr yesterday, so I'm maybe not the most qualified person on that subject, but it seems that for Qq's purposes it's beneficial to generate more efficient representations if we can. Compile-times are already not great, so if we can cut that down a bit, that seems good. (If there are other issues that I'm overlooking, please do tell me).

Now, since Kyle mentioned that maybe we're misusing ToExpr, I figured I could try making a dedicated QuoteExpr typeclass that does allow for Props. It also uses the QQ type-family for some extra type-safety (at the cost of flexibility with the universe)

/--
  Gives a meta-level representation of the universe in which some type `α` lives
-/
class QuoteUnivOf (α : Sort u) where
  /-- Object representing the universe of `α` -/
  quoteUniv : Level



/--
  Converts a value of type `α` into an expression that represents this value in Lean.

  This class differs from the built-in `ToExpr` in two ways:
    * It allows implementation for `α : Prop`, whereas `ToExpr` is only for `Type _`s
    * We use the `QQ` type family to assert the type of the returned expressions.
      This ensures this type information is available when implementors use the `q(⋅)` macro
      to construct the expression.
-/
class QuoteExpr (α : Sort u) extends QuoteUnivOf α where
  /-- Expression representing the type `α` -/
  quoteTypeExpr : QQ (Expr.sort quoteUniv)
  /-- Convert a value `a : α` into an expression that denotes `a` -/
  quoteExpr     : α → QQ quoteTypeExpr

With this class, we can write the following

import Qq.QuoteExpr
import Qq.Macro

open Lean (Level ToExpr)

namespace Qq

instance (α : Sort 0) : QuoteUnivOf α := ⟨Level.ofNat 0⟩
instance (α : Sort 1) : QuoteUnivOf α := ⟨Level.ofNat 1⟩


/--
  Define a fallback instance of `QuoteExpr` for implementors of `ToExpr`
-/
instance (priority := low) {α : Type u} [ToExpr α] [QuoteUnivOf α] : QuoteExpr α where
  quoteTypeExpr := ToExpr.toTypeExpr α
  quoteExpr a   := ToExpr.toExpr a



instance (a b : Nat) : QuoteExpr (a < b) where
  quoteTypeExpr := q($a < $b)
  quoteExpr := go where
    go {a b : Nat} (h : a < b) : Q($a < $b) := match a, b with
    | 0, 0      => by contradiction
    | 0, b+1    => q(Nat.zero_lt_succ $b)
    | a+1, b+1  =>
      have h := Nat.lt_of_succ_lt_succ h
      let h := go h
      q(@Nat.succ_lt_succ $a $b $h)


instance (n : Nat) : QuoteExpr (Fin n) where
  quoteTypeExpr := q(Fin $n)
  quoteExpr := fun ⟨i, h⟩ => q(⟨$i, $h⟩)

end Qq

@Gabriel Ebner would you be interested in a PR to Qq with this typeclass? Even if ToExpr gets changed to also accept Props, having a Qq specific typeclass (with instances going back and forth) has the benefit of propagating expected types a bit better, if implementors use q(...) to construct their expression. Of course, it has the downside of being a bit confusing, having ToExpr and QuoteExpr for basically the same purpose.

[Kyle Miller]

Here's another design:

import Mathlib.Tactic
import Mathlib.Tactic.ToExpr
import Qq

open Lean Qq

class ReflectType (α : Sort u) [ToLevel.{u}] where
  reflectType : QQ (Expr.sort toLevel.{u})

export ReflectType (reflectType)

class Reflect (α : Sort u) [ToLevel.{u}] [ReflectType α] where
  reflect : α →  QQ (reflectType α)

export Reflect (reflect)

[Kyle Miller]

This lets you reflect types even if their terms aren't in general reflectable. For example, function types:

instance (α : Type u) (β : Type v) [ToLevel.{u+1}] [ToLevel.{v+1}] [ReflectType α] [ReflectType β]
    [ToLevel.{max (u+1) (v+1)}] : ReflectType (α → β) where
  reflectType := Expr.forallE `x (reflectType α) (reflectType β) .default

[Kyle Miller]

It's also easy to use pre-existing ToExpr instances to define these instances:

instance : ReflectType Nat where
  reflectType := toTypeExpr Nat

instance : Reflect Nat where
  reflect := toExpr

[Kyle Miller]

I don't think I've got things quite right yet; universe variables don't seem to be handled properly. Ideally that function instance could be written using q(...) somehow.

[Eric Wieser]

Eric Wieser said:

Shouldn't Fin.toExpr generate ofNat like it did in Lean 3?

I've attempted to PR this in !4#3486, though I can't work out how to use =Q

[Eric Wieser]

This lets you reflect types even if their terms aren't in general reflectable.

This is the design we had in Lean 3 I think with docs#reflect vs docs#reflected (and also docs#reflected_value)

[Kyle Miller]

I got as far as getting exciting new errors with this version:

open Lean Qq in
unsafe instance toExpr (n : ℕ) : ToExpr (Fin n) where
  toTypeExpr := q(Fin $n)
  toExpr := match h : n with
    | 0 => finZeroElim
    | n' + 1 => fun i =>
      let i' : Q(ℕ) := Lean.toExpr (i : ℕ)
      let _n_eq : ($n' + 1) =Q $n := ⟨⟩
      let pf : Q(NeZero $n) := q(@NeZero.succ $n')
      q((haveI : NeZero $n := $pf; OfNat.ofNat $i' : Fin $n))

Error:

reduceEval: failed to evaluate argument
  n

[Alex Keizer]

I was also thinking of making the value to be reflected a parameter to the class

import Mathlib.Tactic
import Mathlib.Tactic.ToExpr
import Qq

open Lean Qq

class ReflectType (α : Sort u) [ToLevel.{u}] where
  reflectType : QQ (Expr.sort toLevel.{u})


class Reflect {α : Sort u} (a : α) [ToLevel.{u}] [ReflectType α] where
  reflect : QQ (ReflectType.reflectType α)

export Reflect (reflect)

That would allow us to reflect specific terms of types that we may not know how to reflect in general. In particular, with some clever instances we can make reflect work on types, too, making ReflectType just an internal implementation detail.

instance [ToLevel.{u}] : ReflectType (Sort u) where
  reflectType := .sort toLevel.{u}

instance {α : Sort u} [ToLevel.{u}] [r : ReflectType α] : Reflect α where
  reflect := r.reflectType

instance {α : Sort u} [ToLevel.{u}] [Reflect α] : ReflectType α where
  reflectType := reflect α



instance : Reflect Nat where
  reflect := toTypeExpr Nat

instance {n : Nat} : Reflect n where
  reflect := toExpr n


#check reflect Nat
#check reflect 1

[Alex Keizer]

With this version we can even (ab)use typeclass synthesis for some symbolic reasoning:

/--
  Some structure that incorporates a function, thus cannot be reflected in general
-/
structure Foo where
  n : Nat
  f : Nat → Nat

/--
  Construct a `Foo` from just a `Nat`, using `id` as the function
-/
def Foo.ofNat (n : Nat) : Foo := ⟨n, id⟩



instance : Reflect Foo where
  reflect := q(Foo)

instance (n : Nat) : Reflect (Foo.ofNat n) where
  reflect := q(Foo.ofNat $n)


section
  variable (foo : Foo)

  /-
    Whoops, we cannot reflect `Foo` in general:
    failed to synthesize instance
      Reflect foo
  -/
  #check reflect foo

  variable (n : Nat)

  /-
    But this does work!
  -/
  #check
    let bar := Foo.ofNat n
    reflect bar
end

I'm not sure actually defining these instances is a good idea, but it's cool!

[Eric Wieser]

Congrats, you've reinvented (a QQ-friendly version of) docs#reflected! But I agree that design looks useful, and I don't know why it was changed between Lean 3 and Lean 4

[Eric Wieser]

docs#Lean.ToLevel now exists. Is there a straightforward way to teach Qq about this? nevermind, I guess it already existed above!