# How to deal with the proliferation of encodings of ASTs?

When working with type theory and ASTs one often ends up with a large amount of different encodings. It's very similar to the same problem in compiler design but more annoying because it's dependently typed as well.

I will use the simply typed lambda calculus as an example.

A user facing language

Inductive type :=
| tvar (A: string)
| fn (t1 t2: type).

Inductive term :=
| var (x: string)
| lam (x: string) (t: type) (e: term)
| app (e0 e1: term).

Inductive judge: list (string * type) -> term -> type -> Prop :=
| j_var {G x t}: find x G = Some t -> G |- var x in t
| j_lam {G x t1 t2 e}:
(x, t) :: G |- e in t2 ->
G |- lam x t1 e in fn t1 t2
| j_app {G t1 t2 e1 e2}:
G |- e1 in fn t1 t2 ->
G |- e2 in t1 ->
G |- app e1 e2 in t2
where "G |- e 'in' t" :[ (judge G e t).


A "decorated" format

Inductive term: list (string * type) -> type -> Set :=
| var {G t} (x: string): find x G = Some t -> term G t
| lam {G t2} (x: string) t1 (e: term ((x, t1) :: G) t2): term G (fn t1 t2)
| app {G t1 t2}: term G (fn t1 t2) -> term G t1 -> term G t2


Canonical forms (typing judgements omitted)

Inductive intro :=
| lam (x: string) (M: intro)
| neu (R: elim)
with elim :=
| var (x: string)
| app (R: elim) (M: intro).


Debruijn levels (judgements omitted)

Inductive term :=
| var (n: nat)
| lam (t: type) (e: term)
| app (e1 e2: term).


Parametric higher order abstract syntax

Inductive term V :=
| var (x: V)
| lam (t: type) (e: V -> term V)
| app (e1 e2: term V).


And various annoying combinations of all of these.

I'm not really sure how to grapple with all these different encodings.

• @GuyCoder Not really enough detail but to be sure Prolog is fun. IIRC there's a Lambda Prolog tactic language for Coq but I have no experience with it. I found Makam was great for prototyping stuff but was not formal and was pretty research quality. Mar 30, 2022 at 17:53
• I don't think that homoiconicity does anything to help here --- not least because homoiconicity appears not to be a well-defined concept at all. Mar 30, 2022 at 17:53
• I deal with the issue by accepting it. When things are done the right way, these types serve a purpose. So what is the problem, other than some humans being slightly annoyed? Mar 30, 2022 at 21:14
• @AndrejBauer indeed sometimes beauty has to take a backseat to getting things done. There's nothing really wrong with this approach. Mar 30, 2022 at 21:40
• This also happens in ordinary informal/paper-based stuff too, if you are being careful enough. My approach to mitigating the damage has been to simply decrease the number of representations used (by changing the way I prove things)! This has led to superior and more abstract proofs of the results in question. For instance, there are only two representations needed to prove normalization for MLTT --- but conventional proofs tend to involve closer to 4-6 representations. But it is true that sometimes you must bite the bullet. Mar 31, 2022 at 7:44