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 spelling follows Kovács' elaboration-zoo, the reference implementation that chapter 2 cross-reads, with two deliberate deviations: everything is ASCII, and the annotated lambda \(x : A). t exists because chapter 4 will need it. Why an annotation on let but not on every lambda is a question this chapter cannot yet answer; it is the heart of 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 (p : Parser a) (f : a -> Parser b) : Parser b := fun input =>
  match p input with
  | none => none
  | some (x, rest) => f x rest

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

Lawful? Probably. Proved? No. Needed? No. 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 q receives input untouched:

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

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

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

The loop the checker refuses

Grammars repeat: 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 p 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 (p : Parser a) : Parser (List a) :=
  (do
    let x <- p
    let xs <- manyNaive p
    pure (x :: xs))
  <|> pure []

The refusal is not pedantry; chapter 0 promised that Lean insists on termination proofs, and here there is none to be had, because the definition can genuinely run forever: p may succeed without consuming anything, and then manyNaive p calls itself on exactly the input it started with. No decreasing measure exists. The honest response is to say so in the definition:

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

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

The keyword partial def is the escape hatch chapter 0 declined: it asks Lean to compile the recursion without a termination proof. Simple parser combinators are partial functions, and pretending otherwise would misdescribe the design space; the closing section names two ways to buy the proof back. Partiality has a price on this very page: the kernel will not unfold a partial definition, so #guard cannot check many. The demonstrations below are #eval outputs instead, 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

Tokens

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 (p : Parser a) : Parser a := do
  let x <- p
  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 but "no". 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 (p : Parser a) (f : a -> Parser b) : Parser b := fun input pos =>
  match p input pos with
  | .error consumed pos' => .error consumed pos'
  | .ok consumed x rest pos' =>
    match f 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 (p : Parser a) (q : Unit -> Parser a) : Parser a := fun input pos =>
  match p input pos with
  | .error false _ => q () 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 (p : Parser a) : Parser a := fun input pos =>
  match p 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 (p : Parser a) (s : String) : Result a :=
  p 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. 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 the algebraic laws of choice, in exchange for the commitment and the sharper error position just seen.

The grammar, at last

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

Identifiers are the first grammar production, and the mirror image of keyword: after reading the characters, 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 and the parser are mutual inverses 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.

Roads not taken

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 and Wu'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.