Parametric Higher-Order Abstract Syntax

In contrast to first-order encodings, higher-order encodings avoid explicit modeling of variable identity. Instead, the binding constructs of an object language (the language being formalized) can be represented using the binding constructs of the meta language (the language in which the formalization is done). The best known higher-order encoding is called higher-order abstract syntax (HOAS), and we can start by attempting to apply it directly in Lean.

Remark: this example is based on an example in the book Certified Programming with Dependent Types by Adam Chlipala.

Here is the definition of the simple type system for our programming language, a simply typed lambda calculus with natural numbers as the base type.

inductive 
Ty: Type
Ty where
  | 
nat: Ty
nat
  | 
fn: Ty → Ty → Ty
fn : 
Ty: Type
Ty → 
Ty: Type
Ty → 
Ty: Type
Ty

We can write a function to translate Ty values to a Lean type — remember that types are first class, so can be calculated just like any other value. We mark Ty.denote as [reducible] to make sure the typeclass resolution procedure can unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance Add (Ty.denote Ty.nat). Since Ty.denote is marked as [reducible], the typeclass resolution procedure can reduce Ty.denote Ty.nat to Nat, and use the builtin instance for Add Nat as the solution.

Recall that the term a.denote is sugar for denote a where denote is the function being defined. We call it the "dot notation".

@[reducible] def 
Ty.denote: Ty → Type
Ty.denote : 
Ty: Type
Ty → 
Type: Type 1
Type
  | 
nat: Ty
nat    => 
Nat: Type
Nat
  | 
fn: Ty → Ty → Ty
fn 
a: Ty
a 
b: Ty
b => 
a: Ty
a.
denote: Ty → Type
denote → 
b: Ty
b.
denote: Ty → Type
denote

With HOAS, each object language binding construct is represented with a function of the meta language. Here is what we get if we apply that idea within an inductive definition of term syntax. However a naive encondig in Lean fails to meet the strict positivity restrictions imposed by the Lean kernel. An alternate higher-order encoding is parametric HOAS, as introduced by Washburn and Weirich for Haskell and tweaked by Adam Chlipala for use in Coq. The key idea is to parameterize the declaration by a type family rep standing for a "representation of variables."

inductive 
Term': (Ty → Type) → Ty → Type
Term' (
rep: Ty → Type
rep : 
Ty: Type
Ty → 
Type: Type 1
Type) : 
Ty: Type
Ty → 
Type: Type 1
Type
  | 
var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty
var   : 
rep: Ty → Type
rep 
ty: Ty
ty → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
ty: Ty
ty
  | 
const: {rep : Ty → Type} → Nat → Term' rep Ty.nat
const : 
Nat: Type
Nat → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
.nat: Ty
.nat
  | 
plus: {rep : Ty → Type} → Term' rep Ty.nat → Term' rep Ty.nat → Term' rep Ty.nat
plus  : 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
.nat: Ty
.nat → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
.nat: Ty
.nat → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
.nat: Ty
.nat
  | 
lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (dom.fn ran)
lam   : (
rep: Ty → Type
rep 
dom: Ty
dom → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
ran: Ty
ran) → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep (
.fn: Ty → Ty → Ty
.fn 
dom: Ty
dom 
ran: Ty
ran)
  | 
app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (dom.fn ran) → Term' rep dom → Term' rep ran
app   : 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep (
.fn: Ty → Ty → Ty
.fn 
dom: Ty
dom 
ran: Ty
ran) → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
dom: Ty
dom → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
ran: Ty
ran
  | 
let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂
let   : 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
ty₁: Ty
ty₁ → (
rep: Ty → Type
rep 
ty₁: Ty
ty₁ → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
ty₂: Ty
ty₂) → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
ty₂: Ty
ty₂

Lean accepts this definition because our embedded functions now merely take variables as arguments, instead of arbitrary terms. One might wonder whether there is an easy loophole to exploit here, instantiating the parameter rep as term itself. However, to do that, we would need to choose a variable representation for this nested mention of term, and so on through an infinite descent into term arguments.

We write the final type of a closed term using polymorphic quantification over all possible choices of rep type family

open Ty (
nat: Ty
nat 
fn: Ty → Ty → Ty
fn)

namespace FirstTry

def 
Term: Ty → Type 1
Term (
ty: Ty
ty : 
Ty: Type
Ty) := (
rep: Ty → Type
rep : 
Ty: Type
Ty → 
Type: Type 1
Type) → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
ty: Ty
ty

In the next two example, note how each is written as a function over a rep choice, such that the specific choice has no impact on the structure of the term.

def 
add: Term (nat.fn (nat.fn nat))
add : 
Term: Ty → Type 1
Term (
fn: Ty → Ty → Ty
fn 
nat: Ty
nat (
fn: Ty → Ty → Ty
fn 
nat: Ty
nat 
nat: Ty
nat)) := fun 
_rep: Ty → Type
_rep =>
  
.lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (dom.fn ran)
.lam fun 
x: _rep nat
x => 
.lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (dom.fn ran)
.lam fun 
y: _rep nat
y => 
.plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat
.plus (
.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty
.var 
x: _rep nat
x) (
.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty
.var 
y: _rep nat
y)

def 
three_the_hard_way: Term nat
three_the_hard_way : 
Term: Ty → Type 1
Term 
nat: Ty
nat := fun 
rep: Ty → Type
rep =>
  
.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (dom.fn ran) → Term' rep dom → Term' rep ran
.app (
.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (dom.fn ran) → Term' rep dom → Term' rep ran
.app (
add: Term (nat.fn (nat.fn nat))
add 
rep: Ty → Type
rep) (
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const 
1: Nat
1)) (
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const 
2: Nat
2)

end FirstTry

The argument rep does not even appear in the function body for add. How can that be? By giving our terms expressive types, we allow Lean to infer many arguments for us. In fact, we do not even need to name the rep argument! By using Lean implicit arguments and lambdas, we can completely hide rep in these examples.

def 
Term: Ty → Type 1
Term (
ty: Ty
ty : 
Ty: Type
Ty) := {
rep: Ty → Type
rep : 
Ty: Type
Ty → 
Type: Type 1
Type} → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
ty: Ty
ty

def 
add: Term (nat.fn (nat.fn nat))
add : 
Term: Ty → Type 1
Term (
fn: Ty → Ty → Ty
fn 
nat: Ty
nat (
fn: Ty → Ty → Ty
fn 
nat: Ty
nat 
nat: Ty
nat)) :=
  
.lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (dom.fn ran)
.lam fun 
x: rep✝ nat
x => 
.lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (dom.fn ran)
.lam fun 
y: rep✝ nat
y => 
.plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat
.plus (
.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty
.var 
x: rep✝ nat
x) (
.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty
.var 
y: rep✝ nat
y)

def 
three_the_hard_way: Term nat
three_the_hard_way : 
Term: Ty → Type 1
Term 
nat: Ty
nat :=
  
.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (dom.fn ran) → Term' rep dom → Term' rep ran
.app (
.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (dom.fn ran) → Term' rep dom → Term' rep ran
.app 
add: Term (nat.fn (nat.fn nat))
add (
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const 
1: Nat
1)) (
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const 
2: Nat
2)

It may not be at all obvious that the PHOAS representation admits the crucial computable operations. The key to effective deconstruction of PHOAS terms is one principle: treat the rep parameter as an unconstrained choice of which data should be annotated on each variable. We will begin with a simple example, that of counting how many variable nodes appear in a PHOAS term. This operation requires no data annotated on variables, so we simply annotate variables with Unit values. Note that, when we go under binders in the cases for lam and let, we must provide the data value to annotate on the new variable we pass beneath. For our current choice of Unit data, we always pass ().

def 
countVars: {ty : Ty} → Term' (fun x => Unit) ty → Nat
countVars : 
Term': (Ty → Type) → Ty → Type
Term' (fun 
_: Ty
_ => 
Unit: Type
Unit) 
ty: Ty
ty → 
Nat: Type
Nat
  | 
.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty
.var _    => 
1: Nat
1
  | 
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const _  => 
0: Nat
0
  | 
.plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat
.plus 
a: Term' (fun x => Unit) nat
a 
b: Term' (fun x => Unit) nat
b => 
countVars: {ty : Ty} → Term' (fun x => Unit) ty → Nat
countVars 
a: Term' (fun x => Unit) nat
a + 
countVars: {ty : Ty} → Term' (fun x => Unit) ty → Nat
countVars 
b: Term' (fun x => Unit) nat
b
  | 
.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (dom.fn ran) → Term' rep dom → Term' rep ran
.app 
f: Term' (fun x => Unit) (dom✝.fn ty)
f 
a: Term' (fun x => Unit) dom✝
a  => 
countVars: {ty : Ty} → Term' (fun x => Unit) ty → Nat
countVars 
f: Term' (fun x => Unit) (dom✝.fn ty)
f + 
countVars: {ty : Ty} → Term' (fun x => Unit) ty → Nat
countVars 
a: Term' (fun x => Unit) dom✝
a
  | 
.lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (dom.fn ran)
.lam 
b: Unit → Term' (fun x => Unit) ran✝
b    => 
countVars: {ty : Ty} → Term' (fun x => Unit) ty → Nat
countVars (
b: Unit → Term' (fun x => Unit) ran✝
b 
(): Unit
())
  | 
.let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂
.let 
a: Term' (fun x => Unit) ty₁✝
a 
b: Unit → Term' (fun x => Unit) ty
b  => 
countVars: {ty : Ty} → Term' (fun x => Unit) ty → Nat
countVars 
a: Term' (fun x => Unit) ty₁✝
a + 
countVars: {ty : Ty} → Term' (fun x => Unit) ty → Nat
countVars (
b: Unit → Term' (fun x => Unit) ty
b 
(): Unit
())

We can now easily prove that add has two variables by using reflexivity

example: countVars add = 2
example : 
countVars: {ty : Ty} → Term' (fun x => Unit) ty → Nat
countVars 
add: Term (nat.fn (nat.fn nat))
add = 
2: Nat
2 :=
  
rfl: ∀ {α : Type} {a : α}, a = a
rfl

Here is another example, translating PHOAS terms into strings giving a first-order rendering. To implement this translation, the key insight is to tag variables with strings, giving their names. The function takes as an additional input i which is used to create variable names for binders. We also use the string interpolation available in Lean. For example, s!"x_{i}" is expanded to "x_" ++ toString i.

def 
pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → String
pretty (
e: Term' (fun x => String) ty
e : 
Term': (Ty → Type) → Ty → Type
Term' (fun 
_: Ty
_ => 
String: Type
String) 
ty: Ty
ty) (
i: optParam Nat 1
i : 
Nat: Type
Nat := 
1: Nat
1) : 
String: Type
String :=
  match 
e: Term' (fun x => String) ty
e with
  | 
.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty
.var 
s: String
s     => 
s: String
s
  | 
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const 
n: Nat
n   => 
toString: {α : Type} → [self : ToString α] → α → String
toString 
n: Nat
n
  | 
.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (dom.fn ran) → Term' rep dom → Term' rep ran
.app 
f: Term' (fun x => String) (dom✝.fn ty)
f 
a: Term' (fun x => String) dom✝
a   => s!"({
pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → String
pretty 
f: Term' (fun x => String) (dom✝.fn ty)
f 
i: optParam Nat 1
i} {
pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → String
pretty 
a: Term' (fun x => String) dom✝
a 
i: optParam Nat 1
i})"
  | 
.plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat
.plus 
a: Term' (fun x => String) nat
a 
b: Term' (fun x => String) nat
b  => s!"({
pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → String
pretty 
a: Term' (fun x => String) nat
a 
i: optParam Nat 1
i} + {
pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → String
pretty 
b: Term' (fun x => String) nat
b 
i: optParam Nat 1
i})"
  | 
.lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (dom.fn ran)
.lam 
f: String → Term' (fun x => String) ran✝
f     =>
    let 
x: String
x := s!"x_{
i: optParam Nat 1
i}"
    s!"(fun {
x: String
x} => {
pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → String
pretty (
f: String → Term' (fun x => String) ran✝
f 
x: String
x) (
i: optParam Nat 1
i+
1: Nat
1)})"
  | 
.let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂
.let 
a: Term' (fun x => String) ty₁✝
a 
b: String → Term' (fun x => String) ty
b  =>
    let 
x: String
x := s!"x_{
i: optParam Nat 1
i}"
    s!"(let {
x: String
x} := {
pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → String
pretty 
a: Term' (fun x => String) ty₁✝
a 
i: optParam Nat 1
i}; => {
pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → String
pretty (
b: String → Term' (fun x => String) ty
b 
x: String
x) (
i: optParam Nat 1
i+
1: Nat
1)}"

#eval
"(((fun x_1 => (fun x_2 => (x_1 + x_2))) 1) 2)"
 
pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → String
pretty 
three_the_hard_way: Term nat
three_the_hard_way

It is not necessary to convert to a different representation to support many common operations on terms. For instance, we can implement substitution of terms for variables. The key insight here is to tag variables with terms, so that, on encountering a variable, we can simply replace it by the term in its tag. We will call this function initially on a term with exactly one free variable, tagged with the appropriate substitute. During recursion, new variables are added, but they are only tagged with their own term equivalents. Note that this function squash is parameterized over a specific rep choice.

def 
squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep ty
squash : 
Term': (Ty → Type) → Ty → Type
Term' (
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep) 
ty: Ty
ty → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
ty: Ty
ty
 | 
.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty
.var 
e: Term' rep ty
e    => 
e: Term' rep ty
e
 | 
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const 
n: Nat
n  => 
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const 
n: Nat
n
 | 
.plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat
.plus 
a: Term' (Term' rep) nat
a 
b: Term' (Term' rep) nat
b => 
.plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat
.plus (
squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep ty
squash 
a: Term' (Term' rep) nat
a) (
squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep ty
squash 
b: Term' (Term' rep) nat
b)
 | 
.lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (dom.fn ran)
.lam 
f: Term' rep dom✝ → Term' (Term' rep) ran✝
f    => 
.lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (dom.fn ran)
.lam fun 
x: rep dom✝
x => 
squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep ty
squash (
f: Term' rep dom✝ → Term' (Term' rep) ran✝
f (
.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty
.var 
x: rep dom✝
x))
 | 
.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (dom.fn ran) → Term' rep dom → Term' rep ran
.app 
f: Term' (Term' rep) (dom✝.fn ty)
f 
a: Term' (Term' rep) dom✝
a  => 
.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (dom.fn ran) → Term' rep dom → Term' rep ran
.app (
squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep ty
squash 
f: Term' (Term' rep) (dom✝.fn ty)
f) (
squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep ty
squash 
a: Term' (Term' rep) dom✝
a)
 | 
.let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂
.let 
a: Term' (Term' rep) ty₁✝
a 
b: Term' rep ty₁✝ → Term' (Term' rep) ty
b  => 
.let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂
.let (
squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep ty
squash 
a: Term' (Term' rep) ty₁✝
a) fun 
x: rep ty₁✝
x => 
squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep ty
squash (
b: Term' rep ty₁✝ → Term' (Term' rep) ty
b (
.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty
.var 
x: rep ty₁✝
x))

To define the final substitution function over terms with single free variables, we define Term1, an analogue to Term that we defined before for closed terms.

def 
Term1: Ty → Ty → Type 1
Term1 (
ty1: Ty
ty1 
ty2: Ty
ty2 : 
Ty: Type
Ty) := {
rep: Ty → Type
rep : 
Ty: Type
Ty → 
Type: Type 1
Type} → 
rep: Ty → Type
rep 
ty1: Ty
ty1 → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
ty2: Ty
ty2

Substitution is defined by (1) instantiating a Term1 to tag variables with terms and (2) applying the result to a specific term to be substituted. Note how the parameter rep of squash is instantiated: the body of subst is itself a polymorphic quantification over rep, standing for a variable tag choice in the output term; and we use that input to compute a tag choice for the input term.

def 
subst: {ty1 ty2 : Ty} → Term1 ty1 ty2 → Term ty1 → Term ty2
subst (
e: Term1 ty1 ty2
e : 
Term1: Ty → Ty → Type 1
Term1 
ty1: Ty
ty1 
ty2: Ty
ty2) (
e': Term ty1
e' : 
Term: Ty → Type 1
Term 
ty1: Ty
ty1) : 
Term: Ty → Type 1
Term 
ty2: Ty
ty2 :=
  
squash: {rep : Ty → Type} → {ty : Ty} → Term' (Term' rep) ty → Term' rep ty
squash (
e: Term1 ty1 ty2
e 
e': Term ty1
e')

We can view Term1 as a term with hole. In the following example, (fun x => plus (var x) (const 5)) can be viewed as the term plus _ (const 5) where the hole _ is instantiated by subst with three_the_hard_way

#eval
"((((fun x_1 => (fun x_2 => (x_1 + x_2))) 1) 2) + 5)"
 
pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → String
pretty <| 
subst: {ty1 ty2 : Ty} → Term1 ty1 ty2 → Term ty1 → Term ty2
subst (fun 
x: rep✝ nat
x => 
.plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat
.plus (
.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty
.var 
x: rep✝ nat
x) (
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const 
5: Nat
5)) 
three_the_hard_way: Term nat
three_the_hard_way

One further development, which may seem surprising at first, is that we can also implement a usual term denotation function, when we tag variables with their denotations.

The attribute [simp] instructs Lean to always try to unfold denote applications when one applies the simp tactic. We also say this is a hint for the Lean term simplifier.

@[simp] def 
denote: {ty : Ty} → Term' Ty.denote ty → ty.denote
denote : 
Term': (Ty → Type) → Ty → Type
Term' 
Ty.denote: Ty → Type
Ty.denote 
ty: Ty
ty → 
ty: Ty
ty.
denote: Ty → Type
denote
  | 
.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty
.var 
x: ty.denote
x    => 
x: ty.denote
x
  | 
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const 
n: Nat
n  => 
n: Nat
n
  | 
.plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat
.plus 
a: Term' Ty.denote nat
a 
b: Term' Ty.denote nat
b => 
denote: {ty : Ty} → Term' Ty.denote ty → ty.denote
denote 
a: Term' Ty.denote nat
a + 
denote: {ty : Ty} → Term' Ty.denote ty → ty.denote
denote 
b: Term' Ty.denote nat
b
  | 
.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (dom.fn ran) → Term' rep dom → Term' rep ran
.app 
f: Term' Ty.denote (dom✝.fn ty)
f 
a: Term' Ty.denote dom✝
a  => 
denote: {ty : Ty} → Term' Ty.denote ty → ty.denote
denote 
f: Term' Ty.denote (dom✝.fn ty)
f (
denote: {ty : Ty} → Term' Ty.denote ty → ty.denote
denote 
a: Term' Ty.denote dom✝
a)
  | 
.lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (dom.fn ran)
.lam 
f: dom✝.denote → Term' Ty.denote ran✝
f    => fun 
x: dom✝.denote
x => 
denote: {ty : Ty} → Term' Ty.denote ty → ty.denote
denote (
f: dom✝.denote → Term' Ty.denote ran✝
f 
x: dom✝.denote
x)
  | 
.let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂
.let 
a: Term' Ty.denote ty₁✝
a 
b: ty₁✝.denote → Term' Ty.denote ty
b  => 
denote: {ty : Ty} → Term' Ty.denote ty → ty.denote
denote (
b: ty₁✝.denote → Term' Ty.denote ty
b (
denote: {ty : Ty} → Term' Ty.denote ty → ty.denote
denote 
a: Term' Ty.denote ty₁✝
a))

example: denote three_the_hard_way = 3
example : 
denote: {ty : Ty} → Term' Ty.denote ty → ty.denote
denote 
three_the_hard_way: Term nat
three_the_hard_way = 
3: nat.denote
3 :=
  
rfl: ∀ {α : Type} {a : α}, a = a
rfl

To summarize, the PHOAS representation has all the expressive power of more standard encodings (e.g., using de Bruijn indices), and a variety of translations are actually much more pleasant to implement than usual, thanks to the novel ability to tag variables with data.

We now define the constant folding optimization that traverses a term if replaces subterms such as plus (const m) (const n) with const (n+m).

@[simp] def 
constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep ty
constFold : 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
ty: Ty
ty → 
Term': (Ty → Type) → Ty → Type
Term' 
rep: Ty → Type
rep 
ty: Ty
ty
  | 
.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty
.var 
x: rep ty
x    => 
.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep ty
.var 
x: rep ty
x
  | 
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const 
n: Nat
n  => 
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const 
n: Nat
n
  | 
.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (dom.fn ran) → Term' rep dom → Term' rep ran
.app 
f: Term' rep (dom✝.fn ty)
f 
a: Term' rep dom✝
a  => 
.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (dom.fn ran) → Term' rep dom → Term' rep ran
.app (
constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep ty
constFold 
f: Term' rep (dom✝.fn ty)
f) (
constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep ty
constFold 
a: Term' rep dom✝
a)
  | 
.lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (dom.fn ran)
.lam 
f: rep dom✝ → Term' rep ran✝
f    => 
.lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (dom.fn ran)
.lam fun 
x: rep dom✝
x => 
constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep ty
constFold (
f: rep dom✝ → Term' rep ran✝
f 
x: rep dom✝
x)
  | 
.let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂
.let 
a: Term' rep ty₁✝
a 
b: rep ty₁✝ → Term' rep ty
b  => 
.let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂
.let (
constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep ty
constFold 
a: Term' rep ty₁✝
a) fun 
x: rep ty₁✝
x => 
constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep ty
constFold (
b: rep ty₁✝ → Term' rep ty
b 
x: rep ty₁✝
x)
  | 
.plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat
.plus 
a: Term' rep nat
a 
b: Term' rep nat
b =>
    match 
constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep ty
constFold 
a: Term' rep nat
a, 
constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep ty
constFold 
b: Term' rep nat
b with
    | 
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const 
n: Nat
n, 
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const 
m: Nat
m => 
.const: {rep : Ty → Type} → Nat → Term' rep nat
.const (
n: Nat
n+
m: Nat
m)
    | 
a': Term' rep nat
a',       
b': Term' rep nat
b'       => 
.plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat
.plus 
a': Term' rep nat
a' 
b': Term' rep nat
b'

The correctness of the constFold is proved using induction, case-analysis, and the term simplifier. We prove all cases but the one for plus using simp [*]. This tactic instructs the term simplifier to use hypotheses such as a = b as rewriting/simplications rules. We use the split to break the nested match expression in the plus case into two cases. The local variables iha and ihb are the induction hypotheses for a and b. The modifier ← in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in the "reverse direction. That is, given h : a = b, ← h instructs the term simplifier to rewrite b subterms to a.

theorem 
constFold_sound: ∀ {ty : Ty} (e : Term' Ty.denote ty), denote (constFold e) = denote e
constFold_sound (
e: Term' Ty.denote ty
e : 
Term': (Ty → Type) → Ty → Type
Term' 
Ty.denote: Ty → Type
Ty.denote 
ty: Ty
ty) : 
denote: {ty : Ty} → Term' Ty.denote ty → ty.denote
denote (
constFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep ty
constFold 
e: Term' Ty.denote ty
e) = 
denote: {ty : Ty} → Term' Ty.denote ty → ty.denote
denote 
e: Term' Ty.denote ty
e := by
Goals accomplished! 🐙
  induction 
e: Term' Ty.denote ty
e with
ty: Ty
e: Term' Ty.denote ty
denote (constFold e) = denote e simp [*]
Goals accomplished! 🐙
  | 
plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat
plus 
a: Term' Ty.denote nat
a 
b: Term' Ty.denote nat
b 
iha: denote (constFold a) = denote a
iha 
ihb: denote (constFold b) = denote b
ihb =>
ty: Ty
a, b: Term' Ty.denote nat
iha: denote (constFold a) = denote a
ihb: denote (constFold b) = denote b
plus
denote
    (match constFold a, constFold b with
    | Term'.const n, Term'.const m => Term'.const (n + m)
    | a', b' => a'.plus b') =
  denote a + denote b
    split
ty: Ty
a, b: Term' Ty.denote nat
iha: denote (constFold a) = denote a
ihb: denote (constFold b) = denote b
x✝¹, x✝: Term' Ty.denote nat
n✝, m✝: Nat
heq✝¹: constFold a = Term'.const n✝
heq✝: constFold b = Term'.const m✝
plus.h_1
denote (Term'.const (n✝ + m✝)) = denote a + denote b
ty: Ty
a, b: Term' Ty.denote nat
iha: denote (constFold a) = denote a
ihb: denote (constFold b) = denote b
x✝², x✝¹: Term' Ty.denote nat
x✝: ∀ (n m : Nat), constFold a = Term'.const n → constFold b = Term'.const m → False
plus.h_2
denote ((constFold a).plus (constFold b)) = denote a + denote b
    next 
he₁: constFold a = Term'.const n✝
he₁ 
he₂: constFold b = Term'.const m✝
he₂ =>
ty: Ty
a, b: Term' Ty.denote nat
iha: denote (constFold a) = denote a
ihb: denote (constFold b) = denote b
x✝¹, x✝: Term' Ty.denote nat
n✝, m✝: Nat
heq✝¹: constFold a = Term'.const n✝
heq✝: constFold b = Term'.const m✝
plus.h_1
denote (Term'.const (n✝ + m✝)) = denote a + denote b
ty: Ty
a, b: Term' Ty.denote nat
iha: denote (constFold a) = denote a
ihb: denote (constFold b) = denote b
x✝², x✝¹: Term' Ty.denote nat
x✝: ∀ (n m : Nat), constFold a = Term'.const n → constFold b = Term'.const m → False
plus.h_2
denote ((constFold a).plus (constFold b)) = denote a + denote b simp [← 
iha: denote (constFold a) = denote a
iha, ← 
ihb: denote (constFold b) = denote b
ihb, 
he₁: constFold a = Term'.const n✝
he₁, 
he₂: constFold b = Term'.const m✝
he₂]
Goals accomplished! 🐙
    next =>
ty: Ty
a, b: Term' Ty.denote nat
iha: denote (constFold a) = denote a
ihb: denote (constFold b) = denote b
x✝², x✝¹: Term' Ty.denote nat
x✝: ∀ (n m : Nat), constFold a = Term'.const n → constFold b = Term'.const m → False
plus.h_2
denote ((constFold a).plus (constFold b)) = denote a + denote b simp [
iha: denote (constFold a) = denote a
iha, 
ihb: denote (constFold b) = denote b
ihb]
Goals accomplished! 🐙