5. Embedded Domain-Specific Language

「今有物，不知其數。三三數之，賸二；五五數之，賸三；七七數之，賸二。問：物幾何？答曰：二十三。

術曰：三三數之，賸二，置一百四十；五五數之，賸三，置六十三；七七數之，賸二，置三十。并之，得二百三十三，以二百一十減之，即得。凡三三數之，賸一，則置七十；五五數之，賸一，則置二十一；七七數之，賸一，則置十五。一百六以上，以一百五減之，即得。」

The object language becomes embedded in Lean, its programs written directly in Lean files, parsed by Lean, spliced into Lean definitions, and run, with no external pipeline left. The second promise, that something be proved about the language, is chapter 6's, and the embedding is what makes it convenient to keep.

The grammar, declared

In chapter 1 the surface grammar grew out of combinators, one design decision at a time. Here is the same grammar again, as a syntax category:

declare_syntax_cat dtt

syntax:max (name := dttIdent) ident : dtt
syntax:max "U" : dtt
syntax:max "Unit" : dtt
syntax:max "unit" : dtt
syntax:max "(" dtt ")" : dtt
syntax:65 dtt:65 ppSpace dtt:66 : dtt
syntax:25 dtt:26 " -> " dtt:25 : dtt
syntax:25 "(" ident " : " dtt ")" " -> " dtt:25 : dtt
syntax:10 "fun " ident "." ppSpace dtt:10 : dtt
syntax:10 "fun " "(" ident " : " dtt ")" ". " dtt:10 : dtt
syntax:10 "let " ident " : " dtt " = " dtt "; " dtt:10 : dtt

The declarations carry the precedence table in their level annotations: application at 65 binding tighter than arrows at 25, binders lowest at 10, atoms at the maximum. The numbers are ordinals, not magnitudes; all that matters is their order, and the gaps are headroom for productions added later. Associativity hides in the off-by-ones: the arrow parses its left operand at 26 while sitting at 25 itself, so a second arrow can only continue on the right, which is right associativity, and application parses its right operand at 66, one above itself, so a chain can only grow leftward. Chapter 1 encoded the same two facts as a right-recursive descent and a left fold. The left-factor that chapter 1 spent a section on, the two productions beginning with (, is nowhere to be seen: Lean's parser tries same-token alternatives with backtracking and keeps the longest match, silently performing what attempt had to request. One token did not survive the move, and the swap is instructive. A backslash would clear the tokenizer without complaint, and the printer on this very page still emits one, in the backslash lambdas the demonstrations below display. What it collides with is the abbreviation convention every Lean editor builds in, where a leading backslash begins a Unicode abbreviation rather than a term. The embedded lambda is therefore spelled fun, borrowing the host's own binder keyword, and the rent is paid to the host's conventions rather than to its lexer.

Down to Raw, again

The bridge back to the rest of the lectures is one function: syntax patterns destruct each production into chapter 1's Raw, and everything downstream, the checker of chapter 2, the backend of chapter 4, works unchanged. The same strings, one keyword aside; two parsers, one tree.

/-- Lean's `ident` lexes more than the object language means by a name: a
dotted path like `a.x` arrives as one identifier token. Names here are
single words, so anything else is refused rather than truncated. -/
def simpleName (x : Ident) : Except String String :=
  match x.getId.eraseMacroScopes with
  | .str .anonymous s => pure s
  | n => throw s!"object-language names are single words; {n} is not"

partial def rawOfSyntax (stx : TSyntax `dtt) : Except String Raw :=
  match stx with
  | `(dtt| $x:ident) => do pure (.var (<- simpleName x))
  | `(dtt| U) => pure .univ
  | `(dtt| Unit) => pure .unitType
  | `(dtt| unit) => pure .unitElem
  | `(dtt| ($t)) => rawOfSyntax t
  | `(dtt| $fn $arg) => do
    pure (.app (<- rawOfSyntax fn) (<- rawOfSyntax arg))
  | `(dtt| $dom -> $cod) => do
    pure (.pi "_" (<- rawOfSyntax dom) (<- rawOfSyntax cod))
  | `(dtt| ($x:ident : $dom) -> $cod) => do
    pure (.pi (<- simpleName x) (<- rawOfSyntax dom) (<- rawOfSyntax cod))
  | `(dtt| fun $x. $body) => do
    pure (.lam (<- simpleName x) none (<- rawOfSyntax body))
  | `(dtt| fun ($x:ident : $dom). $body) => do
    pure (.lam (<- simpleName x) (some (<- rawOfSyntax dom))
      (<- rawOfSyntax body))
  | `(dtt| let $x : $ty = $val; $body) => do
    pure (.letE (<- simpleName x) (<- rawOfSyntax ty) (<- rawOfSyntax val)
      (<- rawOfSyntax body))
  | _ => throw "unsupported syntax"

The issue promised in chapter 3 appears here: identifiers arriving through quotations carry hygiene marks, and eraseMacroScopes strips them so the object language sees the name the user wrote. A quieter mismatch is settled here too. Lean's ident means more than this language does by a name: a dotted path like a.x arrives as one identifier token, naming a namespace the object language does not have. The helper simpleName accepts exactly the single-word names and refuses the rest, rather than quietly truncating them to their last component; the commands below show the refusal, pinned like every other error.

Two parsers, rule by rule

Placing the two parsers side by side, production by production, shows what the declarations buy. On the left, chapter 1's combinators: every design decision, the commit points, the explicit attempt, the left fold that builds application spines, is spelled out in code. On the right, the same production as one declaration, the decisions compressed into precedence numbers. The comparison echoes the one chapter 2 drew between undirected typing rules and their moded versions: a grammar on paper is a relation between strings and trees, not an algorithm. By hand, chapter 1 turned that relation into one, choosing where to commit and where to backtrack; the syntax command performs the same turn mechanically, and the two algorithms disagree only where the chapter's opening said, at the token for lambda.

And the comparison need not stay on paper. A small helper runs both parsers on the same program, chapter 1's on a string and Lean's on the quoted syntax, and demands the same Raw tree, so each row below closes with parses that really execute, pinned by the build:

/-- Run both parsers on the same program, chapter 1's on the string and
Lean's on the quoted syntax, and demand the same `Raw` tree. -/
def parsersAgree (s : String) (stx : Unhygienic (TSyntax `dtt)) : Bool :=
  match parseRaw s, rawOfSyntax (Unhygienic.run stx) with
  | some fromCombinators, .ok fromSyntax => fromCombinators == fromSyntax
  | _, _ => false

The atoms: keywords, variables, and the parenthesis:

partial def pAtom : Parser Raw :=
  (do
    sym "("
    let t <- pTerm
    sym ")"
    pure t)
  <|> (do keyword "U"; pure .univ)
  <|> (do keyword "Unit"; pure .unitType)
  <|> (do keyword "unit"; pure .unitElem)
  <|> (do let x <- ident; pure (.var x))

syntax:max (name := dttIdent) ident : dtt
syntax:max "U" : dtt
syntax:max "Unit" : dtt
syntax:max "unit" : dtt
syntax:max "(" dtt ")" : dtt

#guard parsersAgree "U" `(dtt| U)
#guard parsersAgree "Unit" `(dtt| Unit)
#guard parsersAgree "unit" `(dtt| unit)
#guard parsersAgree "(x)" `(dtt| (x))

Application, a left-growing spine: the spine is the head's list of arguments, and it grows to the left, f x y grouping as (f x) y:

partial def pSpine : Parser Raw := do
  let fn <- pAtom
  let args <- many pAtom
  pure (args.foldl .app fn)

syntax:65 dtt:65 ppSpace dtt:66 : dtt

#guard parsersAgree "f x y" `(dtt| f x y)
#guard parsersAgree "f (g x)" `(dtt| f (g x))

Arrows and the dependent binder, with the left-factor on one side and longest-match backtracking on the other:

/-- The left-factor: commit to a dependent binder only after `( ident :`. -/
partial def pBinder : Parser (String × Raw) := do
  let x <- attempt (do
    sym "("
    let x <- ident
    sym ":"
    pure x)
  let dom <- pTerm
  sym ")"
  pure (x, dom)

partial def pArrows : Parser Raw :=
  (do
    let (x, dom) <- pBinder
    sym "->"
    let cod <- pArrows
    pure (.pi x dom cod))
  <|> (do
    let dom <- pSpine
    (do
      sym "->"
      let cod <- pArrows
      pure (.pi "_" dom cod))
    <|> pure dom)

syntax:25 dtt:26 " -> " dtt:25 : dtt
syntax:25 "(" ident " : " dtt ")" " -> " dtt:25 : dtt

#guard parsersAgree "A -> B -> C" `(dtt| A -> B -> C)
#guard parsersAgree "(A : U) -> A -> A" `(dtt| (A : U) -> A -> A)

The lambda, annotated and bare:

partial def pLam : Parser Raw := do
  sym "\\"
  (do
    let (x, dom) <- pBinder
    sym "."
    let body <- pTerm
    pure (.lam x (some dom) body))
  <|> (do
    let x <- ident
    sym "."
    let body <- pTerm
    pure (.lam x none body))

syntax:10 "fun " ident "." ppSpace dtt:10 : dtt
syntax:10 "fun " "(" ident " : " dtt ")" ". " dtt:10 : dtt

#guard parsersAgree "\\x. x" `(dtt| fun x. x)
#guard parsersAgree "\\(x : Unit). x" `(dtt| fun (x : Unit). x)

And let, one keyword and three separators on both sides:

partial def pLet : Parser Raw := do
  keyword "let"
  let x <- ident
  sym ":"
  let ty <- pTerm
  sym "="
  let val <- pTerm
  sym ";"
  let body <- pTerm
  pure (.letE x ty val body)

syntax:10 "let " ident " : " dtt " = " dtt "; " dtt:10 : dtt

#guard parsersAgree "let u : Unit = unit; u" `(dtt| let u : Unit = unit; u)

One asymmetry has no right-hand counterpart at all: chapter 1's pTerm dispatches between lambda, let, and arrows by trying them in order, and no declaration answers it, because ordering alternatives is exactly what the precedence levels already do. The identifier row hides the opposite asymmetry: the borrowed ident accepts dotted names that chapter 1's one-word identifiers never could, which is why the bridge back to Raw refuses them.

Judgments with contexts

The commands can grow declaration contexts now that the grammar is Lean's: a telescope of typed names before the turnstile, each inheriting the universe and bound in order. The two commands share their whole front half, one helper that binds the context and synthesizes the term; what remains is the difference between checking and evaluating: the checking command reports the elaborated term as it stands, and the evaluating command normalizes it first, then reports. The names flip with the parser, and the flip is deliberate, because both generations survive in the build: #check_dtt and #eval_dtt are chapter 2's commands, a quoted string handed to chapter 1's parser, while #dtt_check and #dtt_eval take the program itself, parsed by Lean from the same file that states the judgment. The quotes are gone, and with them the escaped backslashes.

syntax dttDecl := "(" ident " : " dtt ")"

open Elab Command in
/-- The front half both judgment commands share: bind each declaration
into the context, then expand, translate, and synthesize the term. -/
def elabJudgment (decls : TSyntaxArray ``dttDecl) (t : TSyntax `dtt) :
    CommandElabM (Cxt × Tm × Val) := do
  let mut cxt := Cxt.empty
  for decl in decls do
    let `(dttDecl| ($x : $ty)) := decl
      | throwError "malformed declaration"
    let name <- ofExcept (simpleName x)
    let ty : TSyntax `dtt := ⟨<- liftMacroM (expandMacros ty)⟩
    let tyRaw <- ofExcept (rawOfSyntax ty)
    match inherit cxt tyRaw .univ with
    | .error e => throwError e
    | .ok ty' =>
      cxt := cxt.bind name (<- ofExcept (eval cxt.env ty'))
  let t : TSyntax `dtt := ⟨<- liftMacroM (expandMacros t)⟩
  let raw <- ofExcept (rawOfSyntax t)
  match synth cxt raw with
  | .error e => throwError e
  | .ok (tm, ty) => return (cxt, tm, ty)

open Elab Command in
elab "#dtt_check " decls:dttDecl* " |- " t:dtt : command => do
  let (cxt, tm, ty) <- elabJudgment decls t
  logInfo s!"{showTm cxt tm} : {<- ofExcept (showTy cxt ty)}"

open Elab Command in
elab "#dtt_eval " decls:dttDecl* " |- " t:dtt : command => do
  let (cxt, tm, ty) <- elabJudgment decls t
  let v <- ofExcept (eval cxt.env tm)
  let tm' <- ofExcept (quote cxt.lvl ty v)
  logInfo s!"{showTm cxt tm'} : {<- ofExcept (showTy cxt ty)}"

/-- info: \(x : A). x : (x : A) -> A -/
#guard_msgs in
#dtt_check (A : U) |- fun (x : A). x

/-- info: x : A -/
#guard_msgs in
#dtt_check (A : U) (x : A) |- x

/-- error: unknown variable y -/
#guard_msgs in
#dtt_check (A : U) (x : A) |- y

/-- error: object-language names are single words; a.x is not -/
#guard_msgs in
#dtt_check |- a.x

Longer programs ride the same turnstile. A chain of definitions reads like a file in the object language, and the two commands answer two different questions about it: #dtt_check echoes the elaborated program with its type, and #dtt_eval normalizes it away:

/--
info: let id : (A : U) -> A -> A = \A. \x. x; let twice : (A : U) -> (A -> A) -> A -> A = \A. \f. \x. f (f x); twice Unit (id Unit) unit : Unit
-/
#guard_msgs in
#dtt_check |-
  let id : (A : U) -> A -> A = fun A. fun x. x;
  let twice : (A : U) -> (A -> A) -> A -> A = fun A. fun f. fun x. f (f x);
  twice Unit (id Unit) unit

/-- info: unit : Unit -/
#guard_msgs in
#dtt_eval |-
  let id : (A : U) -> A -> A = fun A. fun x. x;
  let twice : (A : U) -> (A -> A) -> A -> A = fun A. fun f. fun x. f (f x);
  twice Unit (id Unit) unit

/-- info: \x. unit : (x : Unit) -> Unit -/
#guard_msgs in
#dtt_eval (f : Unit -> Unit) |- fun (x : Unit). f x

Arithmetic without numbers

The language has no numbers, yet it can count. A Church numeral is a function that iterates: given a type, a step, and a start, the numeral n applies the step n times. The type of numerals quantifies over the universe and lands back in it, which is the U : U shortcut of chapter 2 earning its keep; a stratified theory would need a universe level here. Addition iterates the successor, and the answer is computed by nothing but normalization, the evaluator of chapter 2 running under three binders:

/-- info: \A. \f. \x. f (f (f (f (f x)))) : (A : U) -> (f : A -> A) -> (x : A) -> A -/
#guard_msgs in
#dtt_eval |-
  let N : U = (A : U) -> (f : A -> A) -> (x : A) -> A;
  let two : N = fun A. fun f. fun x. f (f x);
  let three : N = fun A. fun f. fun x. f (f (f x));
  let add : N -> N -> N = fun m. fun n. fun A. fun f. fun x. m A f (n A f x);
  add two three

/--
info: \A. \f. \x. f (f (f (f (f (f (f x)))))) : (A : U) -> (f : A -> A) -> (x : A) -> A
-/
#guard_msgs in
#dtt_eval |-
  let N : U = (A : U) -> (f : A -> A) -> (x : A) -> A;
  let two : N = fun A. fun f. fun x. f (f x);
  let three : N = fun A. fun f. fun x. f (f (f x));
  let add : N -> N -> N = fun m. fun n. fun A. fun f. fun x. m A f (n A f x);
  two N (add two) three

The second command deserves a second look: the numeral two is instantiated at the type of numerals itself, so its step function is “add two” and its start is three, computing $3 + 2 + 2$. Numerals consuming numerals is the impredicativity of U : U made tangible, and the normal forms the build pins are the whole proof that the machinery works.

The splice

Residence is completed by one elaborator, and its name declares its ancestry: as by embeds the tactic language in term position, by_dtt embeds the object language, the program compiled through chapter 4's backend into the Expr Lean was about to elaborate anyway. An object program is now an ordinary Lean value; #guard runs it, and a spliced function applies to Lean arguments.

open Elab Term in
elab "by_dtt " t:dtt : term => do
  let t : TSyntax `dtt := ⟨<- liftMacroM (expandMacros t)⟩
  let raw <- ofExcept (rawOfSyntax t)
  match synth Cxt.empty raw with
  | .error e => throwError "our checker refuses: {e}"
  | .ok (tm, _) => compile tm

#guard (by_dtt (fun (x : Unit). x) unit) == ()

def applyTwice :=
  by_dtt fun (f : Unit -> Unit). fun (x : Unit). f (f x)

#guard applyTwice (fun u => u) () == ()

Like by, the form is open at the right, so a multi-line program may follow the keyword, and a splice standing as an argument wears parentheses. With that, an object program stands wherever a Lean term stands: inside a pair, handed to List.map, sandwiched between Lean's id and a spliced function of the object language's own. One price of the embedding also shows here: declaring Unit a token of the object grammar reserves that spelling globally for the rest of the file, so a Lean-position ascription like (y : Unit) can no longer be written below the grammar, and the definitions here leave their types to Lean instead. The host lends its lexer, and the lease has terms.

#guard ((by_dtt let u : Unit = unit; u), (by_dtt (fun (x : Unit). x) unit))
    == ((), ())

#guard List.map (by_dtt fun (x : Unit). x) [(), (), ()] == [(), (), ()]

def sandwich := fun y =>
  id (applyTwice (by_dtt fun (x : Unit). x) y)

#guard sandwich () == ()

A language that does not look like Lean

The point of owning the grammar is that nothing forces it to resemble the host. A handful of productions and macro rules host a Chinese-keyword variant of the object language, just in time, inside the file. The frame productions carry two binding forms, 设 x 类型为 A 其义为 t; u for let and 将 x 映射为 t for the lambda, with an annotated variant 将 (x 类型为 A) 映射为 t, and three tokens name the constants: 宇宙 for the universe, with 幺元类型 and 唯一元 for the unit type and its element. Words like 恒等 are a fourth kind of thing, names rather than keywords, about which more below:

namespace Zh

scoped syntax:max "宇宙" : dtt
scoped syntax:max "幺元类型" : dtt
scoped syntax:max "唯一元" : dtt
scoped syntax:10 "设 " dtt:max " 类型为 " dtt " 其义为 " dtt "; " dtt:10 : dtt
scoped syntax:10 "将 " dtt:max " 映射为 " dtt:10 : dtt
scoped syntax:10 "将 " "(" dtt:max " 类型为 " dtt ")" " 映射为 " dtt:10 : dtt

/-- A name slot holds an ordinary identifier or a declared name token;
either way, out comes the identifier it stands for. -/
def nameOf (x : TSyntax `dtt) : MacroM Ident :=
  match x with
  | `(dtt| $i:ident) => pure i
  | _ => do
    let .node _ _ #[.atom _ tok] := x.raw
      | Macro.throwUnsupported
    pure (mkIdent (.mkSimple tok))


def isIdeograph (ch : Char) : Bool :=
  0x4e00 <= ch.val && ch.val <= 0x9fff

open Lean.Parser in
/-- A maximal run of ideographs lexes as an ordinary identifier, unless the
word is a declared token: keywords stay keywords. -/
def zhIdentFn : ParserFn := fun c s =>
  let start := s.pos
  let s := takeWhile1Fn isIdeograph "Chinese identifier" c s
  if s.hasError then s
  else if (c.tokens.find? (c.extract start s.pos)).isSome then
    s.mkUnexpectedErrorAt "keyword" start
  else
    mkIdResult start none (.mkSimple (c.extract start s.pos)) true c s

open Lean.Parser in
def zhIdent : Parser :=
  { fn := zhIdentFn }

open PrettyPrinter in
@[combinator_formatter zhIdent]
def zhIdent.formatter : Formatter :=
  Formatter.identNoAntiquot.formatter

open PrettyPrinter in
@[combinator_parenthesizer zhIdent]
def zhIdent.parenthesizer : Parenthesizer :=
  Parenthesizer.identNoAntiquot.parenthesizer

/-- The bridge for a Lean-level word: the token becomes the identifier it
abbreviates. -/
def zhTermMacro : Macro := fun stx => do
  let x <- nameOf ⟨stx⟩
  pure x.raw

open Parser Elab Command in
/-- The category dispatch peeks the token table and gives up before trying
any production, so no production alone can admit new words. This command
rewires the dispatch for `dtt` alone: the standard parsers run first, so
every keyword wins, and a run of ideographs that matched nothing else
comes back as the identifier production. Any word is a name. -/
elab "zh_free_names" : command => do
  modifyEnv fun env =>
    categoryParserFnExtension.modifyState env fun prev => fun cat =>
      if cat != `dtt then prev cat
      else fun c s =>
        let iniSz := s.stackSize
        let iniPos := s.pos
        let s' := prev cat c s
        if !s'.hasError then s'
        else
          let s := s'.restore iniSz iniPos
          let s := zhIdentFn c s
          if s.hasError then s'
          else
            let s := s.mkNode ``dttIdent iniSz
            let s := { s with lhsPrec := Parser.maxPrec }
            match (parserExtension.getState c.env).categories.find? `dtt with
            | some catObj => Parser.trailingLoop catObj.tables c s
            | none => s

zh_free_names

open Elab Command in
/-- Abbreviate in Chinese: `略名 名 为 t` declares the abbreviation and
teaches the term grammar the word itself, so later uses need no «». -/
scoped elab "略名 " x:zhIdent " 为 " t:term : command => do
  let id : Ident := ⟨x.raw⟩
  elabCommand (<- `(abbrev $id:ident := $t))
  let kind := mkIdent (Name.mkSimple s!"zhTerm{id.getId.getString!}")
  elabCommand (<- `(scoped syntax:max (name := $kind) $(quote id.getId.getString!):str : term))
  elabCommand (<- `(attribute [macro $kind] zhTermMacro))

scoped macro "#推演 " decls:dttDecl* " |- " t:dtt : command =>
  `(#dtt_eval $decls* |- $t)

scoped syntax (name := zhGuard) (docComment)? "#验辞 " "in " command : command

scoped macro_rules
  | `($dc:docComment #验辞 in $c) => `($dc:docComment #guard_msgs in $c)

scoped macro_rules
  | `(dtt| 宇宙) => `(dtt| U)
  | `(dtt| 幺元类型) => `(dtt| Unit)
  | `(dtt| 唯一元) => `(dtt| unit)
  | `(dtt| 设 $x 类型为 $ty 其义为 $val; $body) => do
    let x <- nameOf x
    `(dtt| let $x : $ty = $val; $body)
  | `(dtt| 将 $x 映射为 $body) => do
    let x <- nameOf x
    `(dtt| fun $x. $body)
  | `(dtt| 将 ($x 类型为 $ty) 映射为 $body) => do
    let x <- nameOf x
    `(dtt| fun ($x:ident : $ty). $body)

end Zh

The design is the division of labor from chapter 3: the Chinese layer is macros, syntax to syntax, and the elaborator never learns Chinese. Because the rules are scoped, the layer switches on with open; because macro expansion preserves positions, an error in a 设 declaration points at the line the reader wrote; and because the productions extend the same category, mixing scripts in one term is not a stunt but the default. Two details earn their keep. The frame productions do not merely swap one keyword for another: 设 and 将 interleave their keywords between the moving pieces, so the declarations read as Chinese sentences, and the macro rewrite, being structural rather than textual, does not care where the pieces sit. And names, at last, need no door at all, though the reason took a fight to learn. Lean's tokenizer rejects CJK ideographs as identifier characters, and the category dispatch peeks the token table and gives up before trying any production, so neither an identifier nor any clever new production can admit a Chinese word. The layer's answer is one command: zh_free_names rewires the dispatch for dtt alone, standard parsers first, so every keyword keeps winning, and a run of ideographs that matched nothing else comes back as the identifier production. Any word is a name, no declaration anywhere. The same freedom one level up costs one line: 略名 名 为 t abbreviates at the Lean level and teaches the term grammar the word itself, and the layer aliases the eval judgment as #推演 and the message pin as #验辞, so a program is written, checked, and pinned in one script:

open Zh

/-- info: let 恒等 : (A : U) -> A -> A = \A. \x. x; 恒等 : (A : U) -> A -> A -/
#验辞 in
#dtt_check |- 设 «恒等» 类型为 (A : 宇宙) -> A -> A 其义为 fun A. fun x. x; «恒等»

/-- info: let v : Unit = u; v : Unit -/
#验辞 in
#dtt_check (u : 幺元类型) |- 设 v 类型为 幺元类型 其义为 u; v

/-- info: unit : Unit -/
#验辞 in
#推演 |-
  设 «恒等» 类型为 (A : 宇宙) -> A -> A 其义为 将 A 映射为 将 x 映射为 x;
  设 w 类型为 幺元类型 其义为 «恒等» 幺元类型 唯一元;
  w

/--
info: let 再施 : (Unit -> Unit) -> Unit -> Unit = \f. \x. f (f x); 再施 : (Unit -> Unit) -> Unit -> Unit
-/
#验辞 in
#dtt_check |-
  设 «再施» 类型为 (幺元类型 -> 幺元类型) -> 幺元类型 -> 幺元类型
    其义为 将 f 映射为 将 x 映射为 f (f x);
  «再施»

/--
info: let 取先 : (A : U) -> A -> A -> A = \A. \x. \y. x; 取先 : (A : U) -> A -> A -> A
-/
#验辞 in
#dtt_check |-
  设 «取先» 类型为 (A : 宇宙) -> A -> A -> A
    其义为 将 A 映射为 将 x 映射为 将 y 映射为 x;
  «取先»

The splice composes with the layer, so object programs written in Chinese embed in ordinary Lean terms and run under #guard like any other value; the elaborator behind by_dtt expands the macros first and never notices the script. The closing definition is the composition in full: a Lean definition whose body is a multi-line Chinese program, dependently typed, its lambdas annotated because the backend demands domains. And the last guard runs the composition in both directions at once: the command 略名 lends a Chinese name to Nat, sparing Lean's own escape hatch «...», and a polymorphic Chinese 再施 instantiates at it, doubling (· + 20) from 2 to land on 42:

#guard (by_dtt 设 v 类型为 幺元类型 其义为 唯一元; v) == ()

def zhProgram :=
  by_dtt
    设 «恒等» 类型为 (A : 宇宙) -> A -> A
      其义为 将 (A 类型为 宇宙) 映射为 将 (x 类型为 A) 映射为 x;
    «恒等» 幺元类型 唯一元

#guard zhProgram == ()

略名 «自然数» 为 Nat

#guard
  (by_dtt
    设 «再施» 类型为 (A : 宇宙) -> (A -> A) -> A -> A
      其义为 将 (A 类型为 宇宙) 映射为
        将 (f 类型为 A -> A) 映射为 将 (x 类型为 A) 映射为 f (f x);
    «再施»)
    自然数 (· + 20) 2 == 42

Scaled from a demonstration to a discipline, the same machinery carries natural language tactics: verbose-lean4, under Further reading, provides natural language tactics to teach mathematics using Lean 4, in French and in English, and the animated gif in its README shows the controlled language at work with its point-and-click interface.

A combinator cheatsheet

The grammar above used a handful of combinators; the toolbox a syntax declaration may draw on is larger, and it divides into families worth one table each. Every row below is verified against the parser sources of the pinned toolchain, and the demonstrations are checked like everything else on these pages, with parse-level refusals pinned by running the parser on strings, the oldest trick in these lectures. First, the pretty-printing hints. Each parses nothing at all; each instructs the formatter, the return leg chapter 3 drew:

Seeing a hint act takes the pretty-printer, so the demonstration builds a two-word category and prints it: at parse time the hints are invisible, and under ppCategory the ppLine breaks and the ppIndent indents:

declare_syntax_cat demo
syntax "cell" : demo
syntax "row " ppLine ppIndent(demo) : demo

open Elab Command PrettyPrinter in
/--
info: row
  cell
-/
#guard_msgs in
#eval show CommandElabM Unit from do
  let stx <- `(demo| row cell)
  let fmt <- liftCoreM <| ppCategory `demo stx
  logInfo (toString fmt)

The position guards are the mirror family: each constrains parsing and is invisible to the formatter. A guard consults the position saved by an enclosing withPosition, and this is the one standing trap: with no withPosition in scope, a guard compares against nothing and silently succeeds.

The demonstration is a block whose items must sit strictly right of the keyword: the saved position is the keyword's own, each string answers to colGt, and a string at the margin is refused with the guard's internal name in the message:

syntax withPosition("blockD" (ppLine colGt str)+) : term

macro_rules
  | `(blockD $[$xs:str]*) => return (quote xs.size : Term)

def blockDemo : Nat :=
  blockD
    "a"
    "b"

#guard blockDemo == 2

open Parser in
/-- info: <input>:2:0: expected checkColGt -/
#guard_msgs in
#eval show CoreM Unit from do
  let .error e := runParserCategory (<- getEnv) `term "blockD\n\"a\""
    | logInfo "parsed"
  logInfo e

Repetition and choice read like the combinators of chapter 1, and one difference is load-bearing: the built-in choice does not backtrack.

The megaparsec commit discipline of chapter 1 returns here exactly: two bracketed forms share their opening token, the bare choice commits on [ and cannot back out, and atomic is the attempt that rewinds:

syntax identBox := "[" ident "]"
syntax numBox := "[" num "]"

syntax "probeA " (atomic(identBox) <|> numBox) : term
syntax "probeB " (identBox <|> numBox) : term

macro_rules
  | `(probeA $_:identBox) => `(1)
  | `(probeA $_:numBox) => `(2)
  | `(probeB $_:identBox) => `(1)
  | `(probeB $_:numBox) => `(2)

#guard probeA [x] == 1
#guard probeA [3] == 2
#guard probeB [x] == 1

open Parser in
/-- info: <input>:1:8: expected identifier -/
#guard_msgs in
#eval show CoreM Unit from do
  let .error e := runParserCategory (<- getEnv) `term "probeB [3]"
    | logInfo "parsed"
  logInfo e

The atoms, last. Two spellings of keyword differ in one worldly consequence this chapter has already paid for twice: a quoted token reserves its spelling globally, while an ampersand keyword matches without reserving.

The demonstration mints a keyword the gentle way: soft parses as a keyword after the probe, and remains an ordinary name for a definition on the next line, the rent this chapter paid for Unit left uncharged:

syntax "probeC " &"soft" : term

macro_rules
  | `(probeC soft) => `(42)

#guard probeC soft == 42

def soft := 7

#guard soft == 7

What remains are the header forms: a leading syntax:70 ... sets the new production's precedence, (name := k) fixes the node kind chapter 3 taught, (priority := high) arbitrates between overlapping productions, and (behavior := both), legal only on declare_syntax_cat, tunes how a category treats its leading identifiers.

Group project recommendations: a Typed Racket flavor

The Chinese layer is a technique, not a destination, and a good group project is to aim it at a different surface: Typed Racket, the typed sister language of Racket, writes binders in annotated brackets, (struct pt ([x : Real] [y : Real])), declares types with (: distance (-> pt pt Real)), and switches on with a single #lang line (the guide's quick start shows one program in both spellings). A Racket-flavored skin for the object language needs exactly this chapter's moves: new productions in the dtt category for the parenthesized forms, macro_rules translating them into the ASCII grammar, scoped syntax in a namespace so the flavor activates by open; the elaborator never learns S-expressions, as it never learned Chinese. The rents will be charged at new counters: Racket's hyphenated names, list-ref, will not lex as identifiers any more than ideographs did, and the free-names rewire is the pattern to imitate.

Then read how the real thing is built. Languages as Libraries walks Racket's extension interface through the implementation of a small typed sister language and lands on the point this chapter kept making: the whole extension is a library, requiring no changes to the host.

Further reading

• Massot, verbose-lean4: natural language tactics to teach mathematics using Lean 4; the animated gif in the README shows the tactics and their point-and-click interface in action. <- back
• Lean/Parser in the Lean 4 sources at the pinned toolchain: the cheatsheet's ground truth; Basic.lean for the guards and choice, Extra.lean for the pretty-printing hints and the indentation bundles, Syntax.lean for the grammar of syntax declarations themselves. <- back
• 《文言陰符》, An Introduction to Programming in Wenyan Language. <- back
• The Typed Racket Guide. <- back
• Tobin-Hochstadt, St-Amour, Culpepper, Flatt, and Felleisen, Languages as Libraries. <- back
• Tobin-Hochstadt and Felleisen, The Design and Implementation of Typed Scheme: the flavor's origin, occurrence typing included. <- back