Expression quotations for Lean 4
This package implements typesafe expression
quotations, which are a particularly
convenient way of constructing objectlevel
expressions (Expr
) in metalevel code.
It combines the intuitiveness of modal sequent calculus with the power and speed of Lean 4's metaprogramming facilities.
Show me some code!
import Qq open Qq Lean
 Construct an expression
def a : Expr := q([42 + 1])
 Construct a typed expression
def b : Q(List Nat) := q([42 + 1])
 Antiquotations
def c (n : Q(Nat)) := q([42 + $n])
 Dependentlytyped antiquotations
def d (u : Level) (n : Q(Nat)) (x : Q(Type u × Fin ($n + 1))) : Q(Fin ($n + 3)) :=
q(⟨$x.2, Nat.lt_of_lt_of_le $x.2.2 (Nat.le_add_right _ 2)⟩)
Typing rules
The Q(·)
modality quotes types:
Q(α)
denotes an expression of type α
.
The type former comes with the following
natural introduction rule:
$a₁ : α₁, …, $aₙ : αₙ ⊢ t : Type

a₁ : Q(α₁), …, aₙ : Q(αₙ) ⊢ Q(t) : Type
The lowercase q(·)
macro serves
as the modal inference rule,
allowing us to construct values in Q(·)
:
$a₁ : α₁, …, $aₙ : αₙ ⊢ t : β

a₁ : Q(α₁), …, aₙ : Q(αₙ) ⊢ q(t) : Q(β)
Example
Let us write a typesafe version of mkApp
:
import Qq
open Qq
set_option trace.compiler.ir.result true in
 Note: `betterApp` actually has two additional parameters
 `{u v : Lean.Level}` autogenerated due to option
 `autoBoundImplicitLocal`.
def betterApp {α : Q(Sort u)} {β : Q($α → Sort v)}
(f : Q((a : α) → $β a)) (a : Q($α)) : Q($β $a) :=
q($f $a)
#eval betterApp q(Int.toNat) q(42)
There are many things going on here:
 The
betterApp
function compiles to a singlebetaRev
call.  It does not require the
MetaM
monad (in contrast toAppBuilder.lean
in the Lean 4 code). Q(…)
is definitionally equal toExpr
, so each variable in the example is just anExpr
. Nevertheless, implicit arguments of the definition (such as
α
oru
) get filled in by type inference, which reduces the potential for errors even in the absence of strong type safety at the meta level.  All quoted expressions, i.e. all code inside
Q(·)
andq(·)
, are typesafe (under the assumption that the values ofα
,f
, etc. really have their declared types).  The second argument in the
#eval
example,q(42)
, correctly constructs an expression of typeInt
, as determined by the first argument.
Because betterApp
takes α
and u
(and β
and v
) as arguments,
it can also perform more interesting tasks compared
to the untyped function mkApp
: for example,
we can change q($f $a)
into q(id $f $a)
without changing the interface
(even though the resulting expression
now contains both the type and the universe level).
The arguments do not need to refer
to concrete types like Int
either:
List ((u : Level) × (α : Q(Sort u)) × List Q(Option $α))
does what you think it does!
In fact it is a crucial feature that we can write metaprograms transforming terms of nonconcrete types in inconsistent contexts:
def tryProve (n : Q(Nat)) (i : Q(Fin $n)) : Option Q($i > 0) := ...
If the i > 0
in the return type were a concrete type in the metalanguage,
then we could not call tryProve
with n := 0
(because we would need to provide a value for i : Fin 0
).
Furthermore,
if n
were a concrete value,
then we could not call tryProve
on
the subterm t
of fun n : Nat => t
.
Implementation
The type family on which this package is built is called QQ
:
def QQ (α : Expr) := Expr
The intended meaning of e : QQ t
is that
e
is an expression of type t
.
Or if you will,
isDefEq (← inferType e) t
.
(This invariant is not enforced though,
but it can be checked with QQ.check
.)
The QQ
type is not meant to be used manually.
You should only interact with it
using the Q(·)
and q(·)
macros.
Comparison
Template Haskell provides a similar mechanism
for typesafe quotations,
writing Q Int
for an expression of type Int
.
This is subtly different
to the QQ
type family considered here:
in Lean notation,
TH's family has the type Q : Type u → Type
,
while ours has the type QQ : Expr → Type
.
In Lean, Q
is not sufficiently expressive
due to universe polymorphism:
we might only know at runtime which universe the type is in,
but Q
version fixes the universe at compile time.
Another lack of expressivity concerns dependent types:
a telescope such as {α : Q Type} (a : Q α)
is not welltyped
with TH's Q
constructor,
because α
is not a type.
To do

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

ql(imax u (v+1))

Automatically create free variables for recursion. Maybe something like this:
def turnExistsIntoForall : Q(Prop) → MetaM Q(Prop)
 ~q(∃ x, $p x) => do
q(∀ x, $(x => turnExistsIntoForall q($p $x)))
 e => e
 Matching should provide control over typeclass diamonds, such as
~q((a + b : α) where
Semiring α
commutes ∀ n, OfNat α n
a + a defEq 0)

Matching on types should be possible, that is,
match (e : Expr) with  ~q($p ∧ $q) => ...
. 
Other bug fixes, documentation, and assorted polishing.