Quasiquotation with Binders: A Lean Metaprogramming Example

Example: Church Numerals

One of the best ways to test a normalization procedure is to use Church numerals. Church numerals are an encoding of the natural numbers in the untyped lambda calculus, in which a number n is a function that takes a function f and a base value z, applying f to z a total of n times. For instance, two is \lambda f. \lambda z. f\ (f\ z) and zero is \lambda f.\lambda z. z. Church numerals are an excellent test of normalization because they are fairly easy to recognize with a bit of practice, and they tend to be good exercise for systems that rely on string representations of names due to using many similar local names. Addition of Church numerals is a function that takes two encoded numbers followed by f and z, using one of the numbers in the base value provided to the other: \lambda n. \lambda k. \lambda f.\lambda z. n\ f\ (k\ f\ z).

The corresponding Tm definitions are:

They're already quite difficult to read. The downside of using Church numerals to test a normalization procedure is that it can be hard to know whether a surprising result is due to a mistake in the input or a mistake in the evaluator. It's worth it to devise a way to write ordinary numbers instead of Church numerals. One way to convert a natural number to a Church numeral is syntactic - the chain of applications of f in the body is constructed directly:

Another is more semantic, using the definitions of zero and successor:

While toChurch' is easier to check with a quick glance, toChurch generates much more readable output:

Tm.lam
  { name := "f" }
  (Tm.lam
    { name := "z" }
    (Tm.app
      (Tm.loc { name := "f" })
      (Tm.app (Tm.loc { name := "f" }) (Tm.app (Tm.loc { name := "f" }) (Tm.loc { name := "z" })))))

Tm.app
  (Tm.lam
    { name := "n" }
    (Tm.lam
      { name := "f" }
      (Tm.lam
        { name := "z" }
        (Tm.app
          (Tm.loc { name := "f" })
          (Tm.app (Tm.app (Tm.loc { name := "n" }) (Tm.loc { name := "f" })) (Tm.loc { name := "z" }))))))
  (Tm.app
    (Tm.lam
      { name := "n" }
      (Tm.lam
        { name := "f" }
        (Tm.lam
          { name := "z" }
          (Tm.app
            (Tm.loc { name := "f" })
            (Tm.app (Tm.app (Tm.loc { name := "n" }) (Tm.loc { name := "f" })) (Tm.loc { name := "z" }))))))
    (Tm.app
      (Tm.lam
        { name := "n" }
        (Tm.lam
          { name := "f" }
          (Tm.lam
            { name := "z" }
            (Tm.app
              (Tm.loc { name := "f" })
              (Tm.app (Tm.app (Tm.loc { name := "n" }) (Tm.loc { name := "f" })) (Tm.loc { name := "z" }))))))
      (Tm.lam { name := "f" } (Tm.lam { name := "z" } (Tm.loc { name := "z" })))))

Defining the Evaluator

A traditional McCarthy-style eval-apply evaluator, using closures as the values of functions, works well for NbE. The eval function takes an expression and an environment of values for the expression's free variables, yielding a value. It is mutually recursively defined with apply, which takes the value of a function and the value of its argument and computes the result of the function call. eval calls apply when it has computed the values of the function and argument positions in an application, and apply calls eval in order to compute with the body of a function.

From Evaluation to Normal Forms

Normalizing terms consists of first evaluating them, then converting the value back to syntax. Because the domain of values has been carefully chosen to exhibit all of the equalities desired for the term language, this process must map terms to a canonical member of the equivalence class induced by the desired equalities - that is, the normal form! But the whole point of glued evaluation is to control unfolding, so the quotation process here must take an argument that determines whether to unfold top-level constants (thus computing normal forms) or to leave them as names (thus computing smaller terms in unifiers).

When reading back nested functions, it's important to ensure that the name of the bound variable has not already been used by a surrounding function. Otherwise, occurrences of the variable could end up pointing at the wrong binding site. Because local and global names are separate syntactic categories in this language, and functions bind only local variables, only the locals need to be checked for conflicts:

The actual process of quotation replaces each value with the corresponding expression:

• Closures represent functions, and can be quoted to lambda-expressions by inventing a fresh name for the function's argument. The body of this function is found by quoting the result of applying the closure value to a value that represents the argument.

• Local variable values represent applications of unknown local functions. They can be quoted by constructing an application expression that applies the variable to the results of quoting each value in the spine.

• Global constant values can be quoted in one of two ways:

  1. If normal forms are being computed, the thunk that represents the value of the application is forced, and the resulting value is quoted

  2. If smaller results are being computed, then the value is quoted as if it were a local variable application, quoting each value in the spine and constructing an application expression

Only a bit of glue code is needed to run the normalization procedure. Given a set of top-level constant definitions represented by an array of name-expression pairs, evalTop constructs a top-level environment by evaluating each declaration's expression in the context of the prior expressions, and then evaluates a result expression in the resulting top-level environment. Similarly, nfTop does the same thing, but it also quotes the resulting value, yielding a normal form or partially-evaluated term, as requested.

The array examples contains the prior examples as declarations suitable for nfTop:

Squinting a bit, two plus two is indeed four:

Tm.lam
  { name := "f" }
  (Tm.lam
    { name := "z" }
    (Tm.app
      (Tm.loc { name := "f" })
      (Tm.app
        (Tm.loc { name := "f" })
        (Tm.app (Tm.loc { name := "f" }) (Tm.app (Tm.loc { name := "f" }) (Tm.loc { name := "z" }))))))

Because add and two are top-level definitions, asking nfTop not to unfold top-level definitions results in the original term:

Tm.app (Tm.app (Tm.top { name := "add" }) (Tm.top { name := "two" })) (Tm.top { name := "two" })

Inspecting the normal forms of the results of toChurch and toChurch' shows that they agree:

Tm.lam
  { name := "f" }
  (Tm.lam
    { name := "z" }
    (Tm.app
      (Tm.loc { name := "f" })
      (Tm.app (Tm.loc { name := "f" }) (Tm.app (Tm.loc { name := "f" }) (Tm.loc { name := "z" })))))

Tm.lam
  { name := "f" }
  (Tm.lam
    { name := "z" }
    (Tm.app
      (Tm.loc { name := "f" })
      (Tm.app (Tm.loc { name := "f" }) (Tm.app (Tm.loc { name := "f" }) (Tm.loc { name := "z" })))))

Indeed, they are equal:

true

The glued evaluator seems to be functioning correctly. But constructing input terms and understanding its output is still tedious and error-prone due to the verbosity of the ASTs. The rest of this post concerns techniques for making the prototype easier to interact with.

First Attempt: Reusing Lean's Binders

Because the embedded language contains binding forms, it's important to find a way to associate the appropriate TName and LName values with the names that the user writes. In this first attempt, the code that implements embedded-language binding forms will emit Lean let-expressions that bind the surface name to the underlying value. To keep the multiple implementations separate, each is placed in its own namespace so that scoped rules won't interfere with each other:

The new syntax is given meaning by defining it as a macro. Each case of the macro translates a quotation of the embedded language to Lean code that constructs the appropriate AST. Whenever a variable is bound in the embedded language, it is implemented by a let-binding in the generated code. The placement of this let determines the variable's scope, so it's important that the case for let places the expansion of e outside the scope of the binding for $x.

With this macro in place, toChurch can be implemented using quasiquotations, and the bindings of f and z can cross the boundaries of antiquotations and be used in nested quotations:

{{{ fun f z => f (f (f (f (f z)))) }}}

This strategy has a number of nice properties:

• Because embedded language binding forms are represented by native Lean binding forms, features like occurrence highlighting and go-to-definition work properly for quotations with no additional work.

• The scoping rules of the embedded language can be read directly from the implementation.

• Mistakes in variable names are caught while writing the program, rather than while running it.

• Macros are easier to write than other kinds of metaprograms.

Unfortunately, there is a key downside to this approach that undermines its usability in practice. Even though Lean and the embedded language conceptually have completely separate namespaces, Lean binders intrude into embedded language terms, leading to error messages that leak details about the encoding. One way that this can go wrong is when Lean binders are accidentally referred to from the embedded language:

application type mismatch
  Tm.lam { name := "xyz" } n
argument
  n
has type
  Nat : Type
but is expected to have type
  Tm : Type

Similarly, embedded language bindings leak into Lean, shadowing Lean's functions:

application type mismatch
  toChurch n
argument
  n
has type
  Tm : Type
but is expected to have type
  Nat : Type

{{{ fun f z => f (f (f z)) }}}

Second Attempt: Distinguishing Scopes

Lean's macros are hygienic: this means that, by default, bindings introduced by a macro expansion will neither capture nor be captured by bindings introduced by other steps of macro expansion. Taking a cue from Matthew Flatt's 2016 paper, Lean distinguishes identifiers introduced at different steps of macro expansion using scopes, which are unique tokens generated for each step. The scope token is added to identifiers in quotations, so binding forms and uses introduced by the macro will refer to each other, but not to anything else. Lean's implementation of hygienic macros is described in detail in a paper by my colleagues Sebastian Ullrich and Leo de Moura.

Even though the hygiene system was designed to prevent bindings introduced by macros from interfering with each other or with other bindings, it can be repurposed to prevent interference between bindings in the embedded language and bindings in Lean. With a bit of trickery, it is possible to obtain a unique scope token that can be added to all embedded language bindings and uses. Adding it to the bindings prevents Lean terms from accessing them, and adding it to the use sites causes them to avoid Lean's bindings and gives them access to the correct bindings.

Each step of macro expansion needs its own scope. To implement this, Lean provides a global supply of macro scopes for each module, and one of them is distinguished as the "current" scope. Between steps of expansion, the current scope is replaced by a fresh one from the supply.

The API to access the macro scopes contains getCurrMacroScope, which accesses the current macro scope, and withFreshMacroScope, which runs a monadic action with the current scope set to a unique, fresh scope. These tools can be combined to create a Lean command that defines a top-level constant that refers to a unique scope:

Running this command defines specialEmbeddedScope to be the desired scope along with the module's name:

The next step is to write a function that adds this scope to a name:

Because macro scopes are usually added by quotations, there's no particularly easy way to add the scope to an identifier (that is, a piece of syntax that represents a name occurrence). In Lean, the datatype of syntax is essentially an encoding of arbitrary trees, which allows the same type to be used for the results of parsers even when they're extensible with arbitrary new productions. The wrapper TSyntax tracks the syntactic category of a piece of syntax at the type level, which can prevent accidental confusion of syntax and also enables the use of the coercion machinery to automate the translation from one category to another. TSyntax postdates the paper on the macro system, but it's described in detail in section 4.4 of Sebastian Ullrich's thesis. Here, the parsed name inside identifier syntax is enriched with the embedded language's designated scope:

The term quasiquotation macro that uses this designated scope is identical to the previous iteration, except it calls addEmbeddedScope at each ocurrence of embedded-language identifiers.

Now, implementation details no longer leak through variable capture. The embedded language term correctly fails to refer to the surrounding Lean binding of n:

unknown identifier 'n✝'

Furthermore, the embedded language's binding of n no longer capture's Lean's binding, so this example now works:

The implementation of the normalization test command is identical to the version without separate scopes, with the exception of the addition of the embedded language scope to identifier names:

This version similarly keeps embedded language bindings separate from Lean's bindings: