Higher-Order Abstract Syntax in Lean

9. When PHOAS Is Inconvenient🔗

PHOAS deliberately hides the identity of variables behind parametricity. That is what makes renaming and substitution free, and it is also the cost: operations that need to look at variable identity have to work for it.

  • A PHOAS term is a function, so it has no built-in equality test, printer, hash, or serialization. Each is an interpretation you write, like Term.toNamed.

  • Term quantifies over all types, so it is itself a "large" type, in Type 1. Anything declared to take an ordinary Type, including the v of Term' itself, cannot take a Term. Code works with Term' v inside and quantifies over v only at the edges, as squash does.

  • Theorems that relate two interpretations, such as printing and evaluation, need the well-formedness hypothesis, which must be proved for each term they are used on.

  • Questions such as "which variables are free here?" or "are these two occurrences the same variable?" need a v that can be inspected, such as Nat, or a conversion to de Bruijn form.

  • Going the other way, from a parser's output with names or indices to a PHOAS term, needs an environment and must handle unbound names. The bookkeeping the rest of the book avoids reappears at that boundary.

  • When renaming and substitution are themselves the subject of study, as in proofs about a type system itself, explicit first-order syntax keeps them visible.

Named and nameless representations are not obsolete. A reasonable design is first-order syntax at the edges, for parsing, storage, and error messages, and PHOAS in the middle, where terms are transformed, evaluated, and reasoned about.