1. Parser Combinators

What their objects are need not be specified; the important thing is how they act upon each other.
Raymond Smullyan, To Mock a Mockingbird, 1985

The object language of these lectures is a minimal dependent type theory: functions whose result type may depend on the argument, a unit type, and a universe. Its programs arrive as strings, and this chapter turns strings into trees. The tool is the parser combinator: instead of a grammar file handed to a generator, a parser is an ordinary value of the language, and small parsers compose into larger ones with ordinary functions. We build the library twice. The first version is as small as it can be, so that every design decision is visible; the second revises what failure means, and the grammar is built on it.

The surface language

\begin{array}{rll} t &::=& x \mid \texttt{U} \mid \texttt{Unit} \mid \texttt{unit} \\ &\mid& \backslash x.\; t \;\mid\; \backslash (x : A).\; t \\ &\mid& t\;\; t \\ &\mid& A \;\texttt{->}\; B \;\mid\; (x : A) \;\texttt{->}\; B \\ &\mid& \texttt{let}\; x : A = t \texttt{;}\; u \\ &\mid& (t) \end{array}

Variables, the universe U, the unit type Unit with its element unit, lambdas plain and annotated, application by juxtaposition associating to the left, function arrows associating to the right with the dependent form (x : A) -> B, and let with a mandatory annotation. The reserved words are let, U, Unit, and unit.

The design follows Kovács' elaboration-zoo, which is also one of the reference implementations of chapter 2. Why an annotation on let but not on every lambda is a question this chapter cannot yet answer; it is answered in chapter 2.

A type for parsers

A parser consumes a prefix of the input and either produces a value and the rest, or refuses. Written as a type:

def Parser (a : Type) : Type :=
  List Char -> Option (a × List Char)

The type Parser a is a plain function type; there is nothing else in it. Sequencing two parsers means running the first, and, if it succeeded, running the second on what remains. That is exactly a bind, so the vocabulary of chapter 0 applies verbatim:

def Parser.pureImpl (x : a) : Parser a := fun input =>
  some (x, input)

def Parser.bindImpl (xs : Parser a) (k : a -> Parser b) : Parser b := fun input =>
  match xs input with
  | none => none
  | some (x, rest) => k x rest

instance : Monad Parser where
  pure := Parser.pureImpl
  bind := Parser.bindImpl

With the Monad instance in place, do-notation works, and the primitive parsers are one-liners:

def fail : Parser a := fun _ =>
  none

def item : Parser Char := fun input =>
  match input with
  | [] => none
  | c :: rest => some (c, rest)

def satisfy (pred : Char -> Bool) : Parser Char := do
  let c <- item
  if pred c then pure c else fail

def char (c : Char) : Parser Char :=
  satisfy (· == c)

#guard item "ab".toList == some ('a', "b".toList)
#guard char 'a' "ab".toList == some ('a', "b".toList)
#guard char 'b' "ab".toList == none

Choice tries one parser and falls back to another. In this first version, falling back means starting over on the original input, since k receives input untouched:

def orElse (xs : Parser a) (k : Unit -> Parser a) : Parser a := fun input =>
  match xs input with
  | some result => some result
  | none => k () input

instance : OrElse (Parser a) where
  orElse := orElse

#guard (char 'a' <|> char 'b') "bc".toList == some ('b', "c".toList)

An identifier is a letter followed by any number of further characters, an application is an atom followed by any number of atoms. The textbook combinator for repetition parses one element, then as many more as possible. Ask Lean to accept it:

/--
error: fail to show termination for
  Course.Chapter1_ParserCombinators.First.manyNaive
with errors
failed to infer structural recursion:
Not considering parameter a of Course.Chapter1_ParserCombinators.First.manyNaive:
  it is unchanged in the recursive calls
Not considering parameter xs of Course.Chapter1_ParserCombinators.First.manyNaive:
  it is unchanged in the recursive calls
no parameters suitable for structural recursion

well-founded recursion cannot be used, `Course.Chapter1_ParserCombinators.First.manyNaive` does not take any (non-fixed) arguments
-/
#guard_msgs in
def manyNaive (xs : Parser a) : Parser (List a) :=
  (do
    let x <- xs
    let ys <- manyNaive xs
    pure (x :: ys))
  <|> pure []

Lean insists on termination proofs, and here there is none to be had, because the definition can genuinely run forever: xs may succeed without consuming anything, and then manyNaive xs calls itself on exactly the input it started with. No decreasing measure exists. Hence we should say this function is not guaranteed to terminate in its definition:

partial def many (xs : Parser a) : Parser (List a) :=
  (do
    let x <- xs
    let ys <- many xs
    pure (x :: ys))
  <|> pure []

def many1 (xs : Parser a) : Parser (List a) := do
  let x <- xs
  let ys <- many xs
  pure (x :: ys)

The keyword partial def asks Lean to compile the recursion without a termination proof. Simple parser combinators are partial functions. Partiality has a price on this very page, and the coin is proof, not evaluation. The command #guard runs compiled code, exactly as #eval does, so it checks many without complaint; but the kernel will not unfold a partial definition, so the rfl checks of chapter 0 have nothing to reduce, and nothing about many can be proved from its definition:

#guard many (char 'a') "aab".toList == some (['a', 'a'], ['b'])

/--
error: Tactic `rfl` failed: The left-hand side
  many (char 'a') "aab".toList
is not definitionally equal to the right-hand side
  some (['a', 'a'], ['b'])

⊢ many (char 'a') "aab".toList = some (['a', 'a'], ['b'])
-/
#guard_msgs in
example : many (char 'a') "aab".toList = some (['a', 'a'], ['b']) := by rfl

The demonstrations below stay with #eval, which shows the parse result rather than asserting one, and the build pins each printed result, so they remain part of the checked content:

/-- info: some (['a', 'a'], ['b']) -/
#guard_msgs in
#eval many (char 'a') "aab".toList

/-- info: some ([], ['b']) -/
#guard_msgs in
#eval many (char 'a') "b".toList

/-- info: none -/
#guard_msgs in
#eval many1 (char 'a') "b".toList

Real input has whitespace, and the classic discipline is to let every token consume the whitespace after it, with a single skip at the very front of the file. Keywords add one subtlety: matching the characters of let is not enough, because lettuce also starts that way. A keyword must end where an identifier could not continue:

def ws : Parser Unit := fun input =>
  some ((), input.dropWhile (·.isWhitespace))

def lexeme (xs : Parser a) : Parser a := do
  let x <- xs
  ws
  pure x

#guard lexeme (char 'a') "a  b".toList == some ('a', "b".toList)

def chars : List Char -> Parser Unit
  | [] => pure ()
  | c :: cs => do
    _ <- char c
    chars cs

def isIdentChar (c : Char) : Bool :=
  c.isAlphanum || c == '_' || c == '\''

def keywordBoundary : Parser Unit := fun input =>
  match input with
  | [] => some ((), [])
  | c :: _ => if isIdentChar c then none else some ((), input)

def keyword (s : String) : Parser Unit :=
  lexeme (do
    chars s.toList
    keywordBoundary)

#guard keyword "let" "let x".toList == some ((), "x".toList)
#guard keyword "let" "lettuce".toList == none
#guard keyword "unit" "unity".toList == none

What failure should mean

The library so far works, and for this chapter's grammar it would suffice. Its two weaknesses only show at scale. First, a failed parse reports none: no position, no hint, nothing to print. Second, <|> restarts alternatives from the original input no matter how far the first alternative got, so a deeply failed branch costs its whole length, and the eventual error points at the beginning rather than at the offending character. The Megaparsec tradition, whose tutorial by Karpov is the canonical walk-through, resolves both with one idea: failure records whether input was consumed, and choice only falls back on failures that consumed nothing. Backtracking becomes something a grammar author requests explicitly, exactly where the grammar needs it.

inductive Result (a : Type) where
  | ok (consumed : Bool) (x : a) (rest : List Char) (pos : Nat)
  | error (consumed : Bool) (pos : Nat)
deriving Repr, BEq

def Parser (a : Type) : Type :=
  List Char -> Nat -> Result a

/-- `partial` definitions need their type provably nonempty; failing at
position zero is as good a witness as any. -/
instance : Inhabited (Result a) where
  default := .error false 0

Every outcome now carries a position, and every outcome says whether the parser moved. Sequencing threads positions and combines consumption; choice reads the flag:

def Parser.pureImpl (x : a) : Parser a := fun input pos =>
  .ok false x input pos

def Parser.bindImpl (xs : Parser a) (k : a -> Parser b) : Parser b := fun input pos =>
  match xs input pos with
  | .error consumed pos' => .error consumed pos'
  | .ok consumed x rest pos' =>
    match k x rest pos' with
    | .error consumed' pos'' => .error (consumed || consumed') pos''
    | .ok consumed' y rest' pos'' => .ok (consumed || consumed') y rest' pos''

instance : Monad Parser where
  pure := Parser.pureImpl
  bind := Parser.bindImpl

def orElse (xs : Parser a) (k : Unit -> Parser a) : Parser a := fun input pos =>
  match xs input pos with
  | .error false _ => k () input pos
  | other => other

instance : OrElse (Parser a) where
  orElse := orElse

The one new combinator is the explicit request to backtrack: it converts a consuming failure into a non-consuming one, at the position where the alternative began.

def attempt (xs : Parser a) : Parser a := fun input pos =>
  match xs input pos with
  | .error _ _ => .error false pos
  | ok => ok

def fail : Parser a := fun _ pos =>
  .error false pos

def satisfy (pred : Char -> Bool) : Parser Char := fun input pos =>
  match input with
  | [] => .error false pos
  | c :: rest =>
    if pred c then .ok true c rest (pos + 1) else .error false pos

def char (c : Char) : Parser Char :=
  satisfy (· == c)

def run (xs : Parser a) (s : String) : Result a :=
  xs s.toList 0

#guard run (char 'a') "ab" == .ok true 'a' "b".toList 1
#guard run (char 'b') "ab" == .error false 0

The behavior worth staring at, with two parsers that both begin with a:

def ab : Parser Char := do
  _ <- char 'a'
  char 'b'

#guard run (ab <|> char 'a') "ab" == .ok true 'b' [] 2
#guard run (ab <|> char 'a') "ax" == .error true 1
#guard run (attempt ab <|> char 'a') "ax" == .ok true 'a' "x".toList 1

On "ax", the parser ab consumes the a and then fails, and the plain alternation fails with it, at position 1, without ever trying char 'a': consumption committed the choice. Wrapping the branch in attempt is the author saying: this branch shares a prefix with the next one, restart is intended. The failure at position 1 rather than 0 is also the better error report, and the same flag that drives commitment is what error labels would hang on; these lectures mention labels and leave them unimplemented. For better error messages there are ariadne and diagnose. And keyword now needs attempt on its own account: matching unit against the input unity consumes four characters before the boundary check fails, and without attempt that consumption would poison the alternation that tries an identifier next. This is the trade chapter 0 left for this chapter to name: a choice operator sensitive to consumption gives up part of the algebra of choice, the unconditional fallback above all, in exchange for the commitment and the sharper error position just seen.

The grammar

The tree a parse produces is the raw, named syntax:

inductive Raw where
  | var (x : String)
  | univ
  | unitType
  | unitElem
  | lam (x : String) (dom? : Option Raw) (body : Raw)
  | app (fn arg : Raw)
  | pi (x : String) (dom cod : Raw)
  | letE (x : String) (ty val body : Raw)
deriving Repr, BEq

The inductive type Raw is nothing but the grammar with the sugar removed: the non-dependent arrow A -> B is stored as a pi whose binder is "_", and the lambda's annotation is an Option. The printer walks the tree with a precedence level and parenthesizes exactly where the level demands:

/-- Precedence levels: 0 binders, 1 arrows, 2 application, 3 atoms. -/
def Raw.render' : Raw -> Nat -> String
  | .var x, _ => x
  | .univ, _ => "U"
  | .unitType, _ => "Unit"
  | .unitElem, _ => "unit"
  | .app fn arg, prec =>
    paren (prec > 2) (fn.render' 2 ++ " " ++ arg.render' 3)
  | .pi "_" dom cod, prec =>
    paren (prec > 1) (dom.render' 2 ++ " -> " ++ cod.render' 1)
  | .pi x dom cod, prec =>
    paren (prec > 1)
      ("(" ++ x ++ " : " ++ dom.render' 0 ++ ") -> " ++ cod.render' 1)
  | .lam x none body, prec =>
    paren (prec > 0) ("\\" ++ x ++ ". " ++ body.render' 0)
  | .lam x (some dom) body, prec =>
    paren (prec > 0)
      ("\\(" ++ x ++ " : " ++ dom.render' 0 ++ "). " ++ body.render' 0)
  | .letE x ty val body, prec =>
    paren (prec > 0)
      ("let " ++ x ++ " : " ++ ty.render' 0 ++ " = " ++ val.render' 0
        ++ "; " ++ body.render' 0)
where
  paren (needed : Bool) (s : String) : String :=
    if needed then "(" ++ s ++ ")" else s

def Raw.render (t : Raw) : String :=
  t.render' 0

#guard (Raw.lam "x" none (.var "x")).render == "\\x. x"
#guard (Raw.pi "A" .univ (.pi "_" (.var "A") (.var "A"))).render
    == "(A : U) -> A -> A"
#guard (Raw.app (.lam "x" none (.var "x")) .unitElem).render
    == "(\\x. x) unit"
#guard (Raw.app (.var "f") (.app (.var "g") (.var "h"))).render == "f (g h)"

Identifier is the first grammar rule. Note that after reading the characters, we should refuse if they spell a reserved word.

def keywords : List String :=
  ["let", "U", "Unit", "unit"]

def ident : Parser String :=
  attempt (lexeme (do
    let c <- satisfy fun c => c.isAlpha || c == '_'
    let cs <- many (satisfy isIdentChar)
    let x := String.ofList (c :: cs)
    if keywords.contains x then fail else pure x))

def sym (s : String) : Parser Unit :=
  lexeme (chars s.toList)

#guard run ident "x1 y" == .ok true "x1" "y".toList 3
#guard run ident "let x" == .error false 0
#guard run ident "unity" == .ok true "unity" [] 5

The grammar itself is a handful of mutually recursive parsers, organized by precedence level, and two of its corners carry all the design content. Application is not written as the left-recursive rule the grammar suggests, which would recurse without consuming; it is an atom followed by many atoms, folded to the left. And after an opening parenthesis, the input alone cannot say whether a dependent binder (x : A) -> B or a parenthesized term follows: the grammar is not LL(1) there. The attempt over the ( ident : prefix is precisely the lookahead that decides, and this is the left-factoring that chapter 5 will watch Lean's own parser perform silently.

def eof : Parser Unit := fun input pos =>
  match input with
  | [] => .ok false () [] pos
  | _ => .error false pos

mutual

partial def pTerm : Parser Raw :=
  pLam <|> pLet <|> pArrows

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))

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)

/-- 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)

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

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))

end

def parseRaw (s : String) : Option Raw :=
  match (do ws; let t <- pTerm; eof; pure t : Parser Raw) s.toList 0 with
  | .ok _ t _ _ => some t
  | .error _ _ => none

Parses, pretty-printed back, and one refusal:

/-- info: some "(A : U) -> A -> A" -/
#guard_msgs in
#eval (parseRaw "(A : U) -> A -> A").map Raw.render

/-- info: some "(\\x. x) unit" -/
#guard_msgs in
#eval (parseRaw "(\\x. x) unit").map Raw.render

/-- info: some "f (g h)" -/
#guard_msgs in
#eval (parseRaw "f (g h)").map Raw.render

/-- info: true -/
#guard_msgs in
#eval parseRaw "\\(A : U). \\x. x"
    == some (.lam "A" (some .univ) (.lam "x" none (.var "x")))

/-- info: true -/
#guard_msgs in
#eval parseRaw "let id : (A : U) -> A -> A = \\A. \\x. x; id Unit unit"
    == some (.letE "id" (.pi "A" .univ (.pi "_" (.var "A") (.var "A")))
        (.lam "A" none (.lam "x" none (.var "x")))
        (.app (.app (.var "id") .unitType) .unitElem))

/-- info: none -/
#guard_msgs in
#eval parseRaw "let x"

The printer is a right inverse of the parser on well-formed trees, and the build checks a sample of that claim: parse after print is the identity.

def roundTrips (t : Raw) : Bool :=
  parseRaw t.render == some t

/-- info: true -/
#guard_msgs in
#eval [
    Raw.lam "x" none (.var "x"),
    Raw.lam "A" (some .univ) (.lam "x" (some (.var "A")) (.var "x")),
    Raw.pi "A" .univ (.pi "_" (.var "A") (.var "A")),
    Raw.app (.lam "x" none (.var "x")) .unitElem,
    Raw.app (.app (.var "f") (.var "g")) (.var "h"),
    Raw.app (.var "f") (.app (.var "g") (.var "h")),
    Raw.letE "u" .unitType .unitElem (.var "u")
  ].all roundTrips

Patterns and anti-patterns

The discipline this chapter applied piecemeal has a catalogue: Willis and Wu's Design Patterns for Parser Combinators, under Further reading, organizes combinator practice into named patterns and anti-patterns, and the chapter can be re-read as an instance of it. Three of the paper's anti-patterns bear directly on this chapter, quoted here in its own words:

Grammar Refactoring: “modifying the grammar to remove left recursion exposes implementation details and complicates the grammar.” The cure is the chain family of patterns, Homogeneous Chains, Heterogeneous Chains, and Precedence Tables; our left-folded application spine is the smallest specimen of the idea.
Lexing then Parsing: “preprocessing the input with a dedicated lexer has no contextual awareness with which to selectively construct tokens.” A combinator parser needs no separate pass; our token layer is built from the same parsers as the grammar.
Inline Bookkeeping: “incorporating metadata inline into the parser is intrusive and brittle.” The cure is smart constructors, the Lifted and Deferred Constructor patterns; our grammar stayed clean of position plumbing precisely because the Result type carries it.

On whitespace the paper is categorical, and its two rules are the argument behind this chapter's convention: whitespace should be read uniformly, and it should be unintrusive to the rest of the parser. Reading whitespace before each token backtracks excessively, forces attempt into every alternation whose branches begin with it, and skews reported positions to before the token; hence trailing consumption through lexeme (the paper's Whitespace Combinators pattern) with a single initial skip, exactly as our grammar does. Among the patterns not yet named here, Tokenizing Combinators and the two error disciplines of Verified Errors by positive lookahead and Preventative Errors by negative lookahead are the road onward from the error labels this chapter left unimplemented.

Precedence and associativity

The object language kept one classic subject small: application associates left, arrows right, and only those two conventions ever meet. Arithmetic is where every parsing tradition meets precedence and associativity in full, and the running example of Willis and Wu's catalogue is this grammar, its lexical rules for numbers and identifiers elided:

\begin{array}{rll} \langle\textit{expr}\rangle &::=& \langle\textit{expr}\rangle \;\texttt{+}\; \langle\textit{term}\rangle \;\mid\; \langle\textit{expr}\rangle \;\texttt{-}\; \langle\textit{term}\rangle \;\mid\; \langle\textit{term}\rangle \\ \langle\textit{term}\rangle &::=& \langle\textit{term}\rangle \;\texttt{*}\; \langle\textit{negate}\rangle \;\mid\; \langle\textit{negate}\rangle \\ \langle\textit{negate}\rangle &::=& \texttt{negate}\; \langle\textit{negate}\rangle \;\mid\; \langle\textit{atom}\rangle \\ \langle\textit{atom}\rangle &::=& \texttt{(}\, \langle\textit{expr}\rangle \,\texttt{)} \;\mid\; \langle\textit{number}\rangle \;\mid\; \langle\textit{ident}\rangle \end{array}

The shape encodes both concerns. Precedence is the layering: each rule hands off to the next tighter one, so + and - bind loosest, * tighter, the prefix negate tighter still, and parentheses restart the tower from an atom. Associativity is the self-reference: the rules for +, -, and * recurse on their left operand, so all three associate to the left. Read as a procedure, that left recursion is the trap application already avoided, a call that consumes nothing, and the cure is the same fold, upgraded from a one-off into a combinator: the catalogue's Homogeneous Chains pattern, classically named chainl1. It parses one operand, then any number of operator-and-operand pairs, and folds to the left:

def chainl1 (xs : Parser a) (op : Parser (a -> a -> a)) : Parser a := do
  let x <- xs
  let rest <- many (do
    let f <- op
    let y <- xs
    pure (f, y))
  pure (rest.foldl (fun x (f, y) => f x y) x)

The classic name is not sacred: Megaparsec itself dropped the chains, arguing that expression parsing belongs to its precedence-table module, and the removal proposal carries the discussion.

The tree is the paper's own, and its printer parenthesizes every compound node, so the shape of each parse is its own demonstration:

inductive Expr where
  | num (n : Int)
  | var (x : String)
  | neg (x : Expr)
  | mul (x y : Expr)
  | add (x y : Expr)
  | sub (x y : Expr)
deriving Repr, BEq

/-- Parenthesize every compound node, so association is visible. -/
def Expr.render : Expr -> String
  | .num n => toString n
  | .var x => x
  | .neg x => "(negate " ++ x.render ++ ")"
  | .mul x y => "(" ++ x.render ++ " * " ++ y.render ++ ")"
  | .add x y => "(" ++ x.render ++ " + " ++ y.render ++ ")"
  | .sub x y => "(" ++ x.render ++ " - " ++ y.render ++ ")"

The grammar then transcribes rule by rule, one chainl1 per infix layer. The word negate needs the boundary discipline that let needed: negated is an identifier, not an application of negate:

def addDigit (n : Int) (c : Char) : Int :=
  n * 10 + (c.toNat - '0'.toNat)

def number : Parser Expr :=
  lexeme (do
    let ds <- many1 (satisfy (·.isDigit))
    pure (.num (ds.foldl addDigit 0)))

def identifier : Parser String :=
  attempt (lexeme (do
    let c <- satisfy (·.isAlpha)
    let cs <- many (satisfy (·.isAlphanum))
    let x := String.ofList (c :: cs)
    if x == "negate" then fail else pure x))

mutual

partial def expr : Parser Expr :=
  chainl1 term ((do sym "+"; pure .add) <|> (do sym "-"; pure .sub))

partial def term : Parser Expr :=
  chainl1 negate (do sym "*"; pure .mul)

partial def negate : Parser Expr :=
  (do
    keyword "negate"
    let x <- negate
    pure (.neg x))
  <|> atom

partial def atom : Parser Expr :=
  (do
    sym "("
    let x <- expr
    sym ")"
    pure x)
  <|> number
  <|> (do let x <- identifier; pure (.var x))

end

def parseExpr (s : String) : Option Expr :=
  match (do ws; let x <- expr; eof; pure x : Parser Expr) s.toList 0 with
  | .ok _ x _ _ => some x
  | .error _ _ => none

/-- info: some "((1 - 2) - 3)" -/
#guard_msgs in
#eval (parseExpr "1 - 2 - 3").map Expr.render

/-- info: some "(1 + (2 * 3))" -/
#guard_msgs in
#eval (parseExpr "1 + 2 * 3").map Expr.render

/-- info: some "((1 + 2) * 3)" -/
#guard_msgs in
#eval (parseExpr "(1 + 2) * 3").map Expr.render

/-- info: some "((negate x) * 2)" -/
#guard_msgs in
#eval (parseExpr "negate x * 2").map Expr.render

/-- info: some "(((negate (1 + x)) * 3) - y)" -/
#guard_msgs in
#eval (parseExpr "negate (1 + x) * 3 - y").map Expr.render

/-- info: some "(negated + 1)" -/
#guard_msgs in
#eval (parseExpr "negated + 1").map Expr.render

/-- info: none -/
#guard_msgs in
#eval parseExpr "1 + + 2"

An evaluator closes the loop: an environment for the variables, Option for the unbound ones, and structural recursion throughout, no partial in sight. The associativity just displayed becomes arithmetic: 1 - 2 - 3 evaluates to -4, not 2:

def Expr.eval (env : List (String × Int)) : Expr -> Option Int
  | .num n => some n
  | .var x => env.lookup x
  | .neg x => do
    let n <- x.eval env
    pure (-n)
  | .mul x y => do
    let n <- x.eval env
    let m <- y.eval env
    pure (n * m)
  | .add x y => do
    let n <- x.eval env
    let m <- y.eval env
    pure (n + m)
  | .sub x y => do
    let n <- x.eval env
    let m <- y.eval env
    pure (n - m)

/-- info: some (-4) -/
#guard_msgs in
#eval (parseExpr "1 - 2 - 3").bind (Expr.eval [])

/-- info: some 7 -/
#guard_msgs in
#eval (parseExpr "1 + 2 * 3").bind (Expr.eval [])

/-- info: some 9 -/
#guard_msgs in
#eval (parseExpr "(1 + 2) * 3").bind (Expr.eval [])

/-- info: some (-2) -/
#guard_msgs in
#eval (parseExpr "negate (1 + x) * 3 - y").bind
    (Expr.eval [("x", -2), ("y", 5)])

/-- info: none -/
#guard_msgs in
#eval (parseExpr "x + 1").bind (Expr.eval [])

Swierstra's Data types à la carte can help improve this little language.

Termination analysis

Partiality was a choice, and there are two principled ways out. The dependent way makes the parser's type carry its progress: in agdarsec, Allais indexes parsers by how much input they may consume, so that many only accepts parsers that provably consume, and the whole library is total by construction. The staged way observes that monadic bind is what obstructs analysis: the rest of a monadic parser is an arbitrary function, so no tool can inspect the grammar before running it. Willis, Wu, and Pickering's work restricts the interface to selective and applicative combinators, recovering both static analysis and, in the staged version, compiled parsers with the combinator surface. Both are further reading, not the road of these lectures. The road behind, meanwhile, has a name: parsing with monadic combinators is the subject of Hutton and Meijer's 1998 functional pearl, which named the pattern this chapter rebuilt from scratch.

More examples

/-- info: some "\\(A : U). \\f. \\x. f (f x)" -/
#guard_msgs in
#eval (parseRaw "\\(A : U). \\f. \\x. f (f x)").map Raw.render

/-- info: some "(A : U) -> (P : A -> U) -> (x : A) -> P x -> P x" -/
#guard_msgs in
#eval (parseRaw "(A : U) -> (P : A -> U) -> (x : A) -> P x -> P x").map
    Raw.render

/-- info: some "(A -> B) -> (B -> C) -> A -> C" -/
#guard_msgs in
#eval (parseRaw "(A -> B) -> (B -> C) -> A -> C").map Raw.render

/-- info: some "f (g x) (h y) z" -/
#guard_msgs in
#eval (parseRaw "((f (g x)) (h y)) z").map Raw.render

/-- info: some "lettuce unity Units" -/
#guard_msgs in
#eval (parseRaw "lettuce unity Units").map Raw.render

/-- info: some "let twice : (A : U) -> (A -> A) -> A -> A = \\A. \\f. \\x. f (f x); twice (Unit -> Unit) (\\f. f) (\\x. x) unit" -/
#guard_msgs in
#eval (parseRaw "let twice : (A : U) -> (A -> A) -> A -> A = \\A. \\f. \\x. f (f x);
  twice (Unit -> Unit) (\\f. f) (\\x. x) unit").map Raw.render

/-- info: true -/
#guard_msgs in
#eval parseRaw "(x : Unit) -> Unit -> Unit"
    == some (.pi "x" .unitType (.pi "_" .unitType .unitType))

/-- info: none -/
#guard_msgs in
#eval parseRaw "let id : U -> U = \\x. x"

Group project recommendations: a Megaparsec for Lean

The library of this chapter stops where the grammar stops needing it. A good group project is to keep building: a Megaparsec-like library for Lean 4, Megaparsec being Haskell's standard parser combinator library, with parser-combinators beside it carrying the generally useful repetition, permutation, and expression-table combinators. Before writing, research how the traditions disagree on what choice should mean:

Parsec, Megaparsec, and Trifecta: a consumed failure is a cut, and their try, this chapter's attempt, undoes the cut.
Attoparsec: failure rolls back automatically, however far the branch ran, and a branch that succeeds is chosen immediately.
Polyparse: failures are soft and roll back, until an explicit commit cuts.

Two directions to grow. Error reports can become beautiful, in the manner of ariadne and diagnose. And a parser combinator never cared what it consumes: the input can be a string, bytes, or something else entirely, so the library can aim beyond characters, at Lean's own Syntax-shaped types.