4. Metaprogramming II: Lean Metaprogramming Monads and the Lean Expr Backend

A promise from chapter 2 comes due here: it kept U : U as a shortcut, and said this chapter would hold that shortcut up against a checker that refuses it. This chapter keeps the promise and widens it into a second opinion: our checker approves terms, and before trusting it, we hand those terms to a checker that has been reviewed for a decade. The plan is a backend: a structural translation from our core terms into Lean's Expr, followed by a command that hands the result to Lean's own type checking. Getting there requires living inside the elaborator's monads, so the chapter starts with the machinery chapter 0 deliberately postponed: monad transformers, and the tower Lean builds with them.

Transformers, finally motivated

Every interesting metaprogram wants several effects at once: read some configuration, mutate some state, fail with a message. Transformers compose single-effect monads into stacks, each layer adding one capability to whatever sits beneath. A miniature of the shape the elaborator uses, a reader over state over exceptions, fits in a definition, a step function, and two checks:

abbrev CheckM := ReaderT Bool (StateT Nat (Except String))

def step : CheckM Unit := do
  modify (· + 1)
  if (<- get) > 3 then
    let verbose <- read
    throw (if verbose then "out of steps after 3" else "out of steps")
  else
    pure ()

#guard (((step *> step).run true).run 0).toOption == some ((), 2)

#guard match ((step *> step *> step *> step).run false).run 0 with
  | .error "out of steps" => true
  | _ => false

Reading the type right to left: computations may throw a String, thread a Nat through every step, and consult a Bool that nobody ever writes. The do-notation of chapter 0 works unchanged, with read, get, modify, and throw supplied by whichever layer owns them.

The zoo

Lean's elaboration monads are exactly such stacks, and there is no need to take anyone's word for it: #print shows each definition, and each is a reader over a context and mutable state over the layer beneath.

#print Lean.MacroM

#print Lean.Core.CoreM

#print Lean.Meta.MetaM

#print Lean.Elab.Term.TermElabM

#print Lean.Elab.Command.CommandElabM

The tower reads: MacroM is the small pure world of chapter 3's macros; CoreM owns the environment of declared constants; MetaM adds the metavariable context, the missing feature our checker was honest about; TermElabM adds what term elaboration needs, and CommandElabM is the top level. A command that wants MetaM powers lifts into them, which is precisely what our second-opinion command below does with liftTermElabM. One resident, TacticM, the proof-state layer above TermElabM, waits for the end of the chapter, where these lectures write tactics of their own. The failure channel deserves its own sentence: the tower throws Lean's structured Exception, which carries a position and a formatted message, not the bare IO.Error of the surrounding IO world.

The backend

The translation itself is the least clever function in these lectures, and that is its virtue: one constructor to one constructor, indices to indices, since Expr uses de Bruijn exactly as chapter 2 did. Three lines carry all the content. Our U becomes Sort 1, this universe's first dishonesty made explicit; Unit and unit become the constants of Lean's own unit type; and the unannotated lambda has no translation at all.

def compile : Tm -> Except String Expr
  | .var i => pure (.bvar i)
  | .univ => pure (.sort 1)
  | .unitType => pure (.const ``Unit [])
  | .unitElem => pure (.const ``Unit.unit [])
  | .lam x none _ =>
    throw s!"the lambda binding {x} carries no annotation; \
      this hole is where an elaborator would put a metavariable"
  | .lam x (some dom) body => do
    pure (.lam (.mkSimple x) (<- compile dom) (<- compile body) .default)
  | .app fn arg => do
    pure (.app (<- compile fn) (<- compile arg))
  | .pi x dom cod => do
    pure (.forallE (.mkSimple x) (<- compile dom) (<- compile cod) .default)
  | .letE x ty val body => do
    pure (.letE (.mkSimple x) (<- compile ty) (<- compile val)
      (<- compile body) false)

The refusal deserves its sentence: an Expr.lam must carry its domain, our checker permits lambdas that inherited theirs from an expected type, and so a checked term can still hold a hole no structural translation can fill. Lean's elaborator, standing in the same spot, mints a metavariable and lets unification find the domain later. That is the entire difference between the two pipelines, located in one match arm.

The second opinion

One command chains the whole course so far: chapter 1's parser, chapter 2's checker, the backend, and then Meta.check, which asks Lean to type the compiled term with the full weight of its implementation behind it. The opinion comes from the elaborator's own checker; the kernel proper sits one addDecl deeper. The program still arrives as a quoted string, the limitation chapter 2 already regretted, and one chapter still separates us from the cure.

open Elab Command in
elab "#second_opinion " s:str : command => do
  let some raw := parseRaw s.getString
    | throwError "parse error"
  match synth Cxt.empty raw with
  | .error e => throwError "our checker refuses: {e}"
  | .ok (tm, _) =>
    match compile tm with
    | .error e => throwError e
    | .ok e =>
      liftTermElabM do
        Meta.check e
        let ty <- Meta.inferType e
        logInfo m!"{e} : {ty}"

/-- info: fun A x => x : (A : Type) → A → A -/
#guard_msgs in
#second_opinion "\\(A : U). \\(x : A). x"

/-- info: (fun x => x) () : Unit -/
#guard_msgs in
#second_opinion "(\\(x : Unit). x) unit"

The identity function of our object language, printed back by Lean as fun A x => x at type (A : Type) → A → A: two implementations of type theory agreeing on a term, one of them ours. The hole travels too. A checked term whose lambda inherited its type compiles to nothing, and the error message says what an elaborator would have done instead:

/--
error: the lambda binding x carries no annotation; this hole is where an elaborator would put a metavariable
-/
#guard_msgs in
#second_opinion "let f : Unit -> Unit = \\x. x; f"

Where the two theories part

The agreement is not total, and the disagreement is the most honest exhibit these lectures can offer. Our checker takes U : U; Lean's universes are stratified, so the compiled claim becomes Type : Type, and Lean's checker refuses it with the two universes named:

/-- info: let A : U = U; A : U -/
#guard_msgs in
#check_dtt "let A : U = U; A"

/--
error: invalid let declaration, term
  Type
has type
  Type 1
but is expected to have type
  Type
-/
#guard_msgs in
#second_opinion "let A : U = U; A"

In the other direction there is a quieter agreement: chapter 2 built eta for Unit into quotation, and Lean has definitional eta for structures, so a neutral function into Unit and the constant function agree on both sides of the divide. The exhibit is also where these lectures reach for chapter 3's Qq once more, its typed quotations building both sides:

/-- info: true -/
#guard_msgs in
open Meta Qq in
#eval show MetaM Bool from
  withLocalDeclD `f q(Unit -> Unit) fun f => do
    let f : Q(Unit -> Unit) := f
    isDefEq f q(fun (_ : Unit) => ())

Both exhibits are pinned by the build, like everything else on these pages: if a Lean upgrade ever changes either verdict, the site will refuse to compile until the prose tells the truth again.

Tactics, the last resident

The zoo tour skipped one cage, and the promised visit is due. Printing TacticM open shows the same reader-over-state shape as every other monad in the tower, and printing its State shows how small the secret is: the proof state is a list of metavariables, the goals, and nothing else.

#print Lean.Elab.Tactic.TacticM

#print Lean.Elab.Tactic.State

A tactic is one more fitting of chapter 3's trench coat, a function Syntax -> TacticM Unit behind an attribute, and the sugar is the same as ever: a tactic that merely abbreviates other tactics is a macro, no monad required.

macro "exact_unit" : tactic => `(tactic| exact Unit.unit)

example : Unit := by exact_unit

Real tactics read and write the state. The goal list is ordinary data behind getGoals and setGoals, and every goal-management combinator in the library, replaceMainGoal, appendGoals and their kin, is sugar over one modify of that list. A two-line tactic makes the point by doing something honest and slightly absurd, reversing the goal order, and the example watches it happen: after constructor splits the pair, the Bool goal is answered first because the swap put it first. Keeping custom state rides the same rails: a tactic needing its own bookkeeping wraps TacticM in one more StateT, exactly the move this chapter opened with.

elab "swap_goals" : tactic => do
  let goals <- getGoals
  setGoals goals.reverse

example : Unit × Bool := by
  constructor
  swap_goals
  exact true
  exact ()

The third register is a tactic that works for its living: it walks the local context looking for a hypothesis whose type is definitionally equal to the goal, and closes the goal with it. Everything learned in this chapter appears in ten lines: the main goal is a metavariable, isDefEq is MetaM's conversion checking riding up the tower, assignment is how metavariables are solved, and the empty goal list is the tactic's way of saying done. The last example shows the failure channel carrying a position and message, pinned like every other error on these pages:

elab "first_assumption" : tactic => do
  let goal <- getMainGoal
  goal.withContext do
    let target <- goal.getType
    for h in <- getLCtx do
      if !h.isImplementationDetail then
        if <- isDefEq h.type target then
          goal.assign h.toExpr
          replaceMainGoal []
          return
    throwError "no hypothesis has the goal's type"

example (u : Unit) : Unit := by first_assumption

example (_n : Nat) (b : Bool) : Bool := by first_assumption

/-- error: no hypothesis has the goal's type -/
#guard_msgs in
example (_n : Nat) : Bool := by first_assumption

Attributes, the registration made yours

The third part of every metaprogramming object has so far been used and never minted: the attribute. Lean exposes the minting too, and the smallest useful attribute is a tag, a persistent set of declaration names. One initialize registers it; a companion command stamps out a whole @[simp]-like simp set, attribute and index included, in one line:

initialize unitLemmaAttr : TagAttribute <-
  registerTagAttribute `unit_lemma "a lemma about Unit, collected by tag"

register_simp_attr unit_simp

One rule of the game is visible only between files: registration runs inside initialize, which executes when a module is imported, so an attribute must live one module upstream of its first use; @[simp] itself obeys the same law, minted in the library long before any lemma wears it. Downstream, the tags do their work: the tag query answers from the environment, and simp only [unit_simp] runs simp on our own private simp set, the very mechanism behind every custom simp set in Mathlib:

@[unit_lemma, unit_simp] theorem unit_eq_unit (u : Unit) : u = () := rfl

/-- info: true -/
#guard_msgs in
#eval show CoreM Bool from do
  return unitLemmaAttr.hasTag (<- getEnv) ``unit_eq_unit

example (f : Unit -> Unit) (u : Unit) : f u = f () := by
  simp only [unit_simp]

Further reading

• The Lean 4 Metaprogramming Book: the MetaM, Elaboration, and Tactics chapters are this chapter's territory at survey depth, including the metavariable machinery our backend honestly lacks. <- back
• Functional Programming in Lean: the monad-transformer chapters, for the stack-building this chapter compressed into one definition. <- back