Yet another expression quotation package

Stream: lean4

[Gabriel Ebner]

In Lean 3, it often annoyed me that `(%%x = %%y) didn't work. And even if it did work, you couldn't use it to implement functions such as mk_pairwise_equality : list expr → expr (because there is no way to provide the universe level to the quotation).

Fortunately, such syntax extensions are easy to implement in Lean 4 these days:

import Quote
open Quote

def mkPairwiseEquality {α : quote Sort u} : List (quote α) → quote Prop
  | [a, b] => quote a = b
  | a :: b :: cs =>
    let bEqCs := mkPairwiseEquality (b :: cs)
    quote a = b ∧ bEqCs
  | _ => quote True

[Mario Carneiro]

This has almost certainly been done before somewhere else, by somebody else.

I think there is something similar in a haskell extension (that is, a type-safe splice operator)

[Gabriel Ebner]

Mario Carneiro said:

I think there is something similar in a haskell extension (that is, a type-safe splice operator)

Thanks for the pointer, but it is indeed only similar. The Template Haskell type is Q : Type → Type, while my type is QQ : Expr → Type. The Type → Type version doesn't work in Lean due to universe polymorphism: we might only know at runtime which universe the type is in, but the Type u → Type version fixes it at compile time.

[Mario Carneiro]

There seems to be a syntactic ambiguity between the two uses of quote for terms and types. How are they disambiguated?

[Mario Carneiro]

Also what are the actual types of quote x : quote α and quote α : Type?

[Gabriel Ebner]

Mario Carneiro said:

There seems to be a syntactic ambiguity between the two uses of quote for terms and types. How are they disambiguated?

By the expected type. Maybe it would be less confusing to use capitalization as in quote x : Quote α.

[Gabriel Ebner]

Mario Carneiro said:

Also what are the actual types of quote x : quote α and quote α : Type?

For example, quote Type : Type expands to QQ (mkSort (mkLevelSucc levelZero)).
And quote Nat : quote Type expands to QQ.mk (mkConst ``Nat)

[Mac]

Mario Carneiro said:

There seems to be a syntactic ambiguity between the two uses of quote for terms and types. How are they disambiguated?

I am also somewhat concerned with the name clash between this quote/Quote and the built-in Lean quote/Quote for generating Syntax.

[Gabriel Ebner]

This is literally one of the todo items:

Pick another name. There is already a Lean.Quote type, which means something slightly different.

Unfortunately, I only learned of Lean.Quote after I wrote this. Suggestions for other names are welcome.

[Mac]

Gabriel Ebner said:

Unfortunately, I only learned of Lean.Quote after I wrote this. Suggestions for other names are welcome.

I believe @Mario Carneiro was using reflect as his name for exhibiting a similar concept so that might fit here.

EDIT: Though now looking through the repository, I see that you are already using that terminology for untyped Expr quotations.

[Mac]

Since you are already naming the class QQ why not name the whole thing QQ and the command qq as well?

[Mac]

Alternatively, since it is a typed reflect you could name it reflectT/ReflectT

[Mario Carneiro]

Ever since the postfix ! on macros went away, I've had difficulty mentally parsing expressions involving macros, and this one is an example.

    let bEqCs := mkPairwiseEquality (b :: cs)
    quote a = b ∧ bEqCs

If I didn't know quote was a macro, then this would be returning (quote a) = b ∧ bEqCs, which has the wrong binding and also does not make it obvious that some major syntactic magic is happening. I would prefer that this use a notation closer to `(...) , which already has an association to quotation in lean. Another possible way to signal the use of a macro is to have mandatory parens and no space, as in quote(a = b ∧ bEqCs). Since this is no longer a valid way to write application of a regular function that seems like a good candidate for "special" functions

[Mario Carneiro]

How about q!(...)?

[Gabriel Ebner]

Yeah, it's confusing that the default precedence for macros is different from functions.

Since this is no longer a valid way to write application of a regular function that seems like a good candidate for "special" functions

Wait, what?!? You're right..

[Gabriel Ebner]

Mario Carneiro said:

How about q!(...)?

I think I'll go with q(...), since ! is no longer supposed to be used for macros.

[Mario Carneiro]

I think we should make an exception for that rule for one-letter macros to accomodate s! and m!

[Gabriel Ebner]

Tbh, I'd prefer s"foo: {x}" like in Scala.

[Sebastian Ullrich]

Mario Carneiro said:

I think we should make an exception for that rule for one-letter macros to accomodate s! and m!

https://github.com/leanprover/lean4/issues/406

[Mario Carneiro]

but if name(...) catches on as a signal for macros then I can get behind that as well

[Mario Carneiro]

s"..." also seems good. Generally, no space after = funny syntax is happening

[Sebastian Ullrich]

(also, https://github.com/leanprover/lean4/issues/407)

[Mario Carneiro]

also name[...] and name{...} (depending on the macro) a la rust

[Gabriel Ebner]

The quote a = b was much easier to parse in the editor because quote is highlighted as a keyword. Now with q(a = b), only the first q( is highlighted. The second ) remains black. :bug:

[Mario Carneiro]

re: escaping in format strings, rust uses "{{foo}}", although "\{foo\}" would also be reasonable

[Mario Carneiro]

I suppose you technically only have to escape the open brace

[Mac]

Mario Carneiro said:

I suppose you technically only have to escape the open brace

True, and "\{foo}" looks better than "\{foo\}" to me. Rust's "{{foo}}" is harder to parse because it could just as easily mean interpolate {foo}.

[Mario Carneiro]

I agree (although I think the escape \} should still be defined and mean }, even if it isn't required, just so people can use the other version if they prefer). Since we already have backslash-escapes in strings it seems needlessly complicated to have more than one kind of escape

[Isaia Nisoli]

Hi, I'm having some problems with the installation of lean on Ubuntu and some uncaught exception messages in leanpkg...

[Isaia Nisoli]

what is the best channel to ask help/relate bugs?

[Mario Carneiro]

which lean?

[Isaia Nisoli]

lean4

[Gabriel Ebner]

I have now also implemented pattern matching (though I had to do some creative hacks to extend the match and do notation):

import Qq
open Qq Lean

def frob : Q(Prop) → MetaM Q(Prop)
  | ~q(∃ x y : α, p x y) => q(∀ x y, p y x)
  | ~q(∃ x y, p x y) => q(∀ x y, p x y)
  | e => throwError "{e}"

#eval frob q(∃ x y, x ≤ y + 0)
#eval frob q(∃ x : String, let x := x.length; ∃ y, x ≤ y + 42)

[Gabriel Ebner]

The syntax has changed a bit. The example at the beginning of the thread is now written as follows:

import Qq
open Qq

def mkPairwiseEquality {α : Q(Sort u)} : List Q(α) → Q(Prop)
  | [a, b] => q(a = b)
  | a :: b :: cs => q(a = b ∧ %(mkPairwiseEquality (b :: cs)))
  | _ => q(True)

[Mario Carneiro]

Is there a reason why you have to use %(...) instead of $(...) for antiquotation? The latter would be better for consistency, of course

[Gabriel Ebner]

Because that would break the syntax matchers (because $(...) is now parsed as a term).

[Mario Carneiro]

doesn't $(...) work on any syntax class?

[Gabriel Ebner]

syntax "$(" term ")" : term
macro_rules | `($(foo) + $(bar)) => foo
/- unknown identifier 'foo' -/

[Mario Carneiro]

can you avoid the syntax "$(" term ")" : term part?

[Mario Carneiro]

antiquotation already exists in the grammar

[Mario Carneiro]

you just need to attach a meaning to it in your macro

[Gabriel Ebner]

I get a parsing error:

#check q( $x )
-- expected '`(tactic|'

[Gabriel Ebner]

Same with $(x). Even if it worked, it would be really ugly to match using macro_rules.

[Mario Carneiro]

Probably, but I'd really like this to work from the user side of things

[Mario Carneiro]

The implementation of `(x) itself might give some clues

[Mac]

The ability to use the antiquotation syntax outside of quotations was removed in a previous update: https://github.com/leanprover/lean4/commit/f0960b7f89c61ba4e28ea8239076812255b078be

[Mario Carneiro]

so in that case the q macro just needs to use incQuotDepth

[Mac]

however, that may result in a clash with the normal antiquotation expansion

[Mac]

(especially in nested quotations)

[Mario Carneiro]

Yes, if you have mixed q(...) and `(...) things might get weird

[Mario Carneiro]

I will let sebastian handle the macro macro stuff, that's a bit too mind bending for me

[Mario Carneiro]

You don't need quotations to implement q(...), it's just a convenience, you can always just wrangle Syntax objects directly

[Mario Carneiro]

so I would just fall back on that when the syntax gets mixed up

[Gabriel Ebner]

I'll see if I can make this incQuotDepth work. I'm not happy about the zoo of antiquotations either.

[Gabriel Ebner]

BTW, what do you think of the q(x + y). Would you prefer q($x + $y)?

[Mario Carneiro]

I don't see that example above, but if x and y are coming from the context then I think they should be $x and $y

[Mario Carneiro]

In short, it should act roughly like lean 3 expr quotation but with better typing

[Mario Carneiro]

Having no sigils like your original version looks nice but talking about the different meta levels is confusing as it is and syntax that is too sugary may obscure this

[Gabriel Ebner]

One motivation was that you could do q(by rwa [add_zero] at h) but q(by rwa [add_zero] at %h) would have been a parse error (because I don't think you can declare additional ident parsers). With the dollar, q(by rwa [add_zero] at $h) should parse though.

[Mac]

Gabriel Ebner said:

(because I don't think you can declare additional ident parsers).

Nope, sadly. :sad: I already ran into this issue in this thread: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Custom.20identifiers.3F/near/234409388.