Higher-Order Abstract Syntax in Lean🔗

Sooner or later, many programs grow a language: business rules, filters, templates, queries, workflows. Once that language has variables, the program has to handle variable binding, and binding is where the bugs are: variables captured by the wrong definition, off-by-one index errors, and theorems that hold only "up to renaming". Higher-order abstract syntax (HOAS) hands most of that work to the language the implementation is written in. This document builds the idea from scratch in Lean: first the pain, then the naive idea and why Lean rejects it, then the parametric version (PHOAS) that works, and finally a typed language with an interpreter and a verified optimization.

Two words recur. The object language is the language being implemented, the one whose syntax trees we build. The host language is the language doing the implementing, here Lean.In the literature the host language is also called the meta-language.

Who this is for. Working programmers who are comfortable with functions, types, recursion and pattern matching, and curious about Lean or about how language tools work inside. No computer science degree is assumed, and this is not a textbook. Terms from programming-language theory are explained in margin notes where they first appear, so readers who already know them can skip the notes. The Lean code is meant to be read, not memorized, and every block is checked by Lean when the book is built.

Where to start. If you know the λ-calculus, α-equivalence, and de Bruijn indices, skip ahead to Binders, the Hard Way. Otherwise start with You Have Built This Before, a short bridge from the rules and filter languages you may have built to the vocabulary used here.

How to read it. The code in this book is live. Hover over a name, or tap it on a phone, to see its type. In a proof, click or tap a step such as simp or funext to see the proof state at that point: what is known, and what remains to be shown. The sources are literate Lean, with text and code in the same files, and they open in any editor with Lean support. Clone the repository, change an example, and Lean tells you at once what broke. Good first experiments: make Term.subst in Binders, the Hard Way avoid capture, try to write the exotic term against parametric HOAS, or break constant folding and watch its proof fail.