The Meta-theory of Symmetric Metaprogramming

This note presents a simplified variant of principled metaprogramming and sketches its soundness proof. The variant treats only dialogues between two stages. A program can have quotes which can contain splices (which can contain quotes, which can contain splices, and so on). Or the program could start with a splice with embedded quotes. The essential restriction is that (1) a term can contain top-level quotes or top-level splices, but not both, and (2) quotes cannot appear directly inside quotes and splices cannot appear directly inside splices. In other words, the universe is restricted to two phases only.

Under this restriction we can simplify the typing rules so that there are always exactly two environments instead of having a stack of environments. The variant presented here differs from the full calculus also in that we replace evaluation contexts with contextual typing rules. While this is more verbose, it makes it easier to set up the meta theory.

Syntax

Terms         t  ::=  x                 variable
                      (x: T) => t       lambda
                      t t               application
                      ’t                quote
                      ~t                splice

Simple terms  u  ::=  x  |  (x: T) => u  |  u u

Values        v  ::=  (x: T) => t       lambda
                      ’u                quoted value

Types         T  ::=  A                 base type
                      T -> T            function type
                      ’T                quoted type

Operational semantics

Evaluation

            ((x: T) => t) v  -->  [x := v]t

                         t1  -->  t2
                       ---------------
                       t1 t  -->  t2 t

                         t1  -->  t2
                       ---------------
                       v t1  -->  v t2

                         t1  ==>  t2
                        -------------
                        ’t1  -->  ’t2

Splicing

                        ~’u  ==>  u

                         t1  ==>  t2
               -------------------------------
               (x: T) => t1  ==>  (x: T) => t2

                         t1  ==>  t2
                       ---------------
                       t1 t  ==>  t2 t

                         t1  ==>  t2
                       ---------------
                       u t1  ==>  u t2

                         t1  -->  t2
                        -------------
                        ~t1  ==>  ~t2

Typing Rules

Typing judgments are of the form E1 * E2 |- t: T where E1, E2 are environments and * is one of ~ and ’.

                          x: T in E2
                       ---------------
                       E1 * E2 |- x: T


                   E1 * E2, x: T1 |- t: T2
               --------------------------------
               E1 * E2 |- (x: T1) => t: T -> T2


         E1 * E2 |- t1: T2 -> T    E1 * E2 |- t2: T2
         -------------------------------------------
                     E1 * E2 |- t1 t2: T


                       E2 ’ E1 |- t: T
                      -----------------
                      E1 ~ E2 |- ’t: ’T


                       E2 ~ E1 |- t: ’T
                       ----------------
                       E1 ’ E2 |- ~t: T

(Curiously, this looks a bit like a Christmas tree).

Soundness

The meta-theory typically requires mutual inductions over two judgments.

Progress Theorem

If E1 ~ |- t: T then either t = v for some value v or t --> t2 for some term t2.
If ’ E2 |- t: T then either t = u for some simple term u or t ==> t2 for some term t2.

Proof by structural induction over terms.

To prove (1):

the cases for variables, lambdas and applications are as in STLC.
If t = ’t2, then by inversion we have ’ E1 |- t2: T2 for some type T2. By the second induction hypothesis (I.H.), we have one of:
- t2 = u, hence ’t2 is a value,
- t2 ==> t3, hence ’t2 --> ’t3.
The case t = ~t2 is not typable.

To prove (2):

If t = x then t is a simple term.
If t = (x: T) => t2, then either t2 is a simple term, in which case t is as well. Or by the second I.H. t2 ==> t3, in which case t ==> (x: T) => t3.
If t = t1 t2 then one of three cases applies:
- t1 and t2 are a simple term, then t is as well a simple term.
- t1 is not a simple term. Then by the second I.H., t1 ==> t12, hence t ==> t12 t2.
- t1 is a simple term but t2 is not. Then by the second I.H. t2 ==> t22, hence t ==> t1 t22.
The case t = ’t2 is not typable.
If t = ~t2 then by inversion we have E2 ~ |- t2: ’T2, for some type T2. By the first I.H., we have one of
- t2 = v. Since t2: ’T2, we must have v = ’u, for some simple term u, hence t = ~’u. By quote-splice reduction, t ==> u.
- t2 --> t3. Then by the context rule for ’t, t ==> ’t3.

Substitution Lemma

If E1 ~ E2 |- s: S and E1 ~ E2, x: S |- t: T then E1 ~ E2 |- [x := s]t: T.
If E1 ~ E2 |- s: S and E2, x: S ’ E1 |- t: T then E2 ’ E1 |- [x := s]t: T.

The proofs are by induction on typing derivations for t, analogous to the proof for STL (with (2) a bit simpler than (1) since we do not need to swap lambda bindings with the bound variable x). The arguments that link the two hypotheses are as follows.

To prove (1), let t = ’t1. Then T = ’T1 for some type T1 and the last typing rule is

                    E2, x: S ’ E1 |- t1: T1
                   -------------------------
                   E1 ~ E2, x: S |- ’t1: ’T1

By the second I.H. E2 ’ E1 |- [x := s]t1: T1. By typing, E1 ~ E2 |- ’[x := s]t1: ’T1. Since [x := s]t = [x := s](’t1) = ’[x := s]t1 we get [x := s]t: ’T1.

To prove (2), let t = ~t1. Then the last typing rule is

                    E1 ~ E2, x: S |- t1: ’T
                    -----------------------
                    E2, x: S ’ E1 |- ~t1: T

By the first I.H., E1 ~ E2 |- [x := s]t1: ’T. By typing, E2 ’ E1 |- ~[x := s]t1: T. Since [x := s]t = [x := s](~t1) = ~[x := s]t1 we get [x := s]t: T.

Preservation Theorem

If E1 ~ E2 |- t1: T and t1 --> t2 then E1 ~ E2 |- t2: T.
If E1 ’ E2 |- t1: T and t1 ==> t2 then E1 ’ E2 |- t2: T.

The proof is by structural induction on evaluation derivations. The proof of (1) is analogous to the proof for STL, using the substitution lemma for the beta reduction case, with the addition of reduction of quoted terms, which goes as follows:

Assume the last rule was
```
                    t1  ==>  t2
                   -------------
                   ’t1  -->  ’t2
```
By inversion of typing rules, we must have T = ’T1 for some type T1 such that t1: T1. By the second I.H., t2: T1, hence ’t2:T1`.

To prove (2):

Assume the last rule was ~’u ==> u. The typing proof of ~’u must have the form

                  E1 ’ E2 |- u: T
                 -----------------
                 E1 ~ E2 |- ’u: ’T
                 -----------------
                 E1 ’ E2 |- ~’u: T

Hence, E1 ’ E2 |- u: T.

Assume the last rule was
```
                      t1  ==>  t2
            -------------------------------
            (x: S) => t1  ==>  (x: T) => t2
```
By typing inversion, E1 ' E2, x: S |- t1: T1 for some type T1 such that T = S -> T1. By the I.H, t2: T1. By the typing rule for lambdas the result follows.
The context rules for applications are equally straightforward.

Assume the last rule was

                      t1  ==>  t2
                     -------------
                     ~t1  ==>  ~t2

By inversion of typing rules, we must have t1: ’T. By the first I.H., t2: ’T, hence ~t2: T.