4. Parametric HOAS🔗

Parametric HOAS (PHOAS) makes one change: abstract over the type of variables.Due to Adam Chlipala (2008), building on Geoffrey Washburn and Stephanie Weirich's "Boxes Go Bananas" (2003). Binders stay Lean functions, but their argument is now an opaque v instead of a whole term. Term' no longer occurs to the left of its own arrow, so the datatype is positive and Lean accepts it. The exotic term of the previous chapter can no longer be written: a binder receives a v of unknown type, and there is nothing to pattern-match on. Going under a binder means handing it a v, and each operation is free to choose what v is.

namespace PHOAS

inductive Term' (v : Type) where
  | var : v → Term' v
  | lam : (v → Term' v) → Term' v
  | app : Term' v → Term' v → Term' v

def Term := ∀ v, Term' v

open Term'

A closed term, one with no free variables, must work for every choice of v.∀ v, Term' v is the type of functions that take a type v and return a Term' v. So every Term below starts with fun v =>, or fun _ => when the body never mentions v. Haskell writes this type forall v. Term' v. We read this as "the term cannot depend on what v is", a reading called parametricity. Lean does not enforce that reading; a later chapter shows where it breaks and how to repair it.

Names and indices are gone, and binding is Lean's:

def I : Term := fun _ => lam fun x => var x
def K : Term := fun _ => lam fun x => lam fun _ => var x
def two : Term := fun _ =>
  lam fun f => lam fun x =>
    app (var f) (app (var f) (var x))
def omega : Term := fun _ =>
  lam fun x => app (var x) (var x)

two applies its first argument twice to its second; omega applies its argument to itself, and comes back in the chapter on types.

Renaming needs no separately defined relation: renaming the Lean variable that stands for an object-language binder does not change the PHOAS term. Lean's own terms use indices for bound variables, so the chore of the previous chapter is done once, inside Lean.rfl proves equations that hold by definition, with no reasoning beyond unfolding and computation.

example : I = fun _ => lam fun y => var y := rfl

4.1. One Term, Many Interpretations🔗

This is the central idea of the book:

PHOAS lets each operation choose the representation of variables that is most convenient for that operation.

With nothing to remember about a variable, we can count occurrences:

def Term'.count : Term' Unit → Nat
  | var _ => 1
  | lam b => (b ()).count
  | app f a => f.count + a.count

def Term.count (e : Term) : Nat := (e Unit).count

example : two.count = 3 := rfl

With a name per variable, we can print. Fresh names come from a depth counter: binders that are in scope at the same point sit at different depths, so their names never clash.

def Term'.toNamed : Term' String → Nat → Named.Term
  | var x, _ => .var x
  | lam b, n =>
    let x := s!"x{n}"
    .lam x ((b x).toNamed (n + 1))
  | app f a, n => .app (f.toNamed n) (a.toNamed n)

def Term.toNamed (e : Term) : Named.Term :=
  (e String).toNamed 0

λx0. λx1. x0 (x0 x1)#eval two.toNamed

λx0. λx1. x0 (x0 x1)

With a binder depth per variable, the first-order representation of the previous chapter (a tree of plain data, with no functions inside) falls out. Each variable stores the depth of its binder, its de Bruijn level; at a use of depth d, the index is the number of binders in between, d - l - 1. From here on, this is the only index arithmetic in the book:

def Term'.toDeBruijn : Term' Nat → Nat → DeBruijn.Term
  | var l, d => .var (d - l - 1)
  | lam b, d => .lam ((b d).toDeBruijn (d + 1))
  | app f a, d => .app (f.toDeBruijn d) (a.toDeBruijn d)

def Term.toDeBruijn (e : Term) : DeBruijn.Term :=
  (e Nat).toDeBruijn 0

example : K.toDeBruijn = .lam (.lam (.var 1)) := rfl

end PHOAS

The next chapters make two more choices: syntax itself, which gives substitution, and semantic values, which give evaluation.