8
$\begingroup$

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.

$\endgroup$
7
  • $\begingroup$ @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. $\endgroup$ Mar 30, 2022 at 17:53
  • $\begingroup$ 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. $\endgroup$ Mar 30, 2022 at 17:53
  • 2
    $\begingroup$ 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? $\endgroup$ Mar 30, 2022 at 21:14
  • 1
    $\begingroup$ @AndrejBauer indeed sometimes beauty has to take a backseat to getting things done. There's nothing really wrong with this approach. $\endgroup$ Mar 30, 2022 at 21:40
  • 2
    $\begingroup$ 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. $\endgroup$ Mar 31, 2022 at 7:44

1 Answer 1

5
$\begingroup$

As various commenters have said, you sometimes just need to bite the bullet. Good modularity, good naming conventions and other standard good software practices will help. If you need inspiration, I'd consult the sources for big projects in this space. In particular, I imagine that the CompCert project with ASTs for various intermediate languages (IRs) would be a good example in the Coq world. (To blow my own horn, the CakeML project has many of these as well, and for a functional language complete with typing relations and the like, but in HOL4 rather than Coq.)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.