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
.
defpretty (pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringe :e: Term' (fun x => String) tyTerm' (funTerm': (Ty → Type) → Ty → Type_ =>_: TyString)String: Typety) (ty: Tyi :i: optParam Nat 1Nat :=Nat: Type1) :1: NatString := matchString: Typee with |e: Term' (fun x => String) ty.var.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep tys =>s: Strings |s: String.const.const: {rep : Ty → Type} → Nat → Term' rep natn =>n: NattoStringtoString: {α : Type} → [self : ToString α] → α → Stringn |n: Nat.app.app: {rep : Ty → Type} → {dom ran : Ty} → Term' rep (dom.fn ran) → Term' rep dom → Term' rep ranff: Term' (fun x => String) (dom✝.fn ty)a => s!"({a: Term' (fun x => String) dom✝prettypretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringff: Term' (fun x => String) (dom✝.fn ty)i} {i: optParam Nat 1prettypretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringaa: Term' (fun x => String) dom✝i})" |i: optParam Nat 1.plus.plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nataa: Term' (fun x => String) natb => s!"({b: Term' (fun x => String) natprettypretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringaa: Term' (fun x => String) nati} + {i: optParam Nat 1prettypretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringbb: Term' (fun x => String) nati})" |i: optParam Nat 1.lam.lam: {rep : Ty → Type} → {dom ran : Ty} → (rep dom → Term' rep ran) → Term' rep (dom.fn ran)f => letf: String → Term' (fun x => String) ran✝x := s!"x_{x: Stringi}" s!"(fun {i: optParam Nat 1x} => {x: Stringpretty (pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringff: String → Term' (fun x => String) ran✝x) (x: Stringi+i: optParam Nat 11)})" |1: Nat.let.let: {rep : Ty → Type} → {ty₁ ty₂ : Ty} → Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂aa: Term' (fun x => String) ty₁✝b => letb: String → Term' (fun x => String) tyx := s!"x_{x: Stringi}" s!"(let {i: optParam Nat 1x} := {x: Stringprettypretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringaa: Term' (fun x => String) ty₁✝i}; => {i: optParam Nat 1pretty (pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringbb: String → Term' (fun x => String) tyx) (x: Stringi+i: optParam Nat 11)}"1: Natprettypretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringthree_the_hard_waythree_the_hard_way: Term nat
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
pretty <|pretty: {ty : Ty} → Term' (fun x => String) ty → optParam Nat 1 → Stringsubst (funsubst: {ty1 ty2 : Ty} → Term1 ty1 ty2 → Term ty1 → Term ty2x =>x: rep✝ nat.plus (.plus: {rep : Ty → Type} → Term' rep nat → Term' rep nat → Term' rep nat.var.var: {rep : Ty → Type} → {ty : Ty} → rep ty → Term' rep tyx) (x: rep✝ nat.const.const: {rep : Ty → Type} → Nat → Term' rep nat5))5: Natthree_the_hard_waythree_the_hard_way: Term nat
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/simplifications 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
.
theoremconstFold_sound (constFold_sound: ∀ {ty : Ty} (e : Term' Ty.denote ty), denote (constFold e) = denote ee :e: Term' Ty.denote tyTerm'Term': (Ty → Type) → Ty → TypeTy.denoteTy.denote: Ty → Typety) :ty: Tydenote (denote: {ty : Ty} → Term' Ty.denote ty → ty.denoteconstFoldconstFold: {rep : Ty → Type} → {ty : Ty} → Term' rep ty → Term' rep tye) =e: Term' Ty.denote tydenotedenote: {ty : Ty} → Term' Ty.denote ty → ty.denotee :=e: Term' Ty.denote tyGoals accomplished! 🐙ty: Ty
e: Term' Ty.denote tydenote (constFold e) = denote eGoals accomplished! 🐙ty: Ty
a, b: Term' Ty.denote nat
iha: denote (constFold a) = denote a
ihb: denote (constFold b) = denote b
plusdenote (match constFold a, constFold b with | Term'.const n, Term'.const m => Term'.const (n + m) | a', b' => a'.plus b') = denote a + denote bty: 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_1denote (Term'.const (n✝ + m✝)) = denote a + denote bty: 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 → Falsedenote ((constFold a).plus (constFold b)) = denote a + denote bty: 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_1denote (Term'.const (n✝ + m✝)) = denote a + denote bty: 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 → Falsedenote ((constFold a).plus (constFold b)) = denote a + denote bGoals accomplished! 🐙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_2denote ((constFold a).plus (constFold b)) = denote a + denote bGoals accomplished! 🐙