Fixes and extensions to symmetric meta programming docs

docs/docs/reference/simple-smp.md

@@ -0,0 +1,236 @@
+---
+layout: doc-page
+title: "The Meta-theory of Symmetric Meta-programming"
+---
+
+# The Meta-theory of Symmetric Meta-programming
+
+23.12.2017
+
+This note presents a simplified variant of
+[symmetric meta-programming](./symmetric-meta-programming.md)
+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
+
+ 1. If `E1 ~  |- t: T` then either `t = v` for some value `v` or `t --> t2` for some term `t2`.
+ 2. 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 STL.
+ - If `t = ’t2`, then by inversion we have ` ’ E1 |- t2: T2` for some type `T2`.
+   By the second 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 IH, `t1 ==> t12`, hence `t ==> t12 t2`.
+   - `t1` is a simple term but `t2` is not. Then by the second IH. `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 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
+
+ 1. If `E1 ~ E2 |- s: S` and `E1 ~ E2, x: S |- t: T` then `E1 ~ E2 |- [x := s]t: T`.
+ 2. 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
+
+ 1. If `E1 ~ E2 |- t1: T` and `t1 --> t2` then `E1 ~ E2 |- t2: T`.
+ 2. 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`.
+

docs/docs/reference/symmetric-meta-programming.md

@@ -32,8 +32,7 @@ prints it again in an error message if it evaluates to `false`.
       ~ assertImpl(’(expr))
 
     def assertImpl(expr: Expr[Boolean]) =
-      ’{ if !(~expr) then throw new AssertionError(s"failed assertion: ${~expr}") }
-
+      ’{ if !(~expr) then throw new AssertionError(s"failed assertion: ${~showExpr(expr)}") }
 
 If `e` is an expression, then `’(e)` or `’{e}` represent the typed
 abstract syntax tree representing `e`. If `T` is a type, then `’[T]`
@@ -491,14 +490,14 @@ is defined in the companion object of class `Expr` as follows:
 The conversion says that values of types implementing the `Liftable`
 type class can be converted ("lifted") automatically to `Expr`
 values. Dotty comes with instance definitions of `Liftable` for
-several types including all underlying types of literals. For example,
-`Int` values can be converted to `Expr[Int]` values by wrapping the
-value in a `Literal` tree node. This makes use of the underlying tree
-representation in the compiler for efficiency. But the `Liftable`
-instances are nevertheless not "magic" in the sense that they could
-all be defined in a user program without knowing anything about the
-representation of `Expr` trees. For instance, here is a possible
-instance of `Liftable[Boolean]`:
+several types including `Boolean`, `String`, and all primitive number
+types. For example, `Int` values can be converted to `Expr[Int]`
+values by wrapping the value in a `Literal` tree node. This makes use
+of the underlying tree representation in the compiler for
+efficiency. But the `Liftable` instances are nevertheless not "magic"
+in the sense that they could all be defined in a user program without
+knowing anything about the representation of `Expr` trees. For
+instance, here is a possible instance of `Liftable[Boolean]`:
 
     implicit def BooleanIsLiftable: Liftable[Boolean] = new {
       implicit def toExpr(b: Boolean) = if (b) ’(true) else ’(false)
@@ -532,6 +531,13 @@ In the end, `Liftable` resembles very much a serialization
 framework. Like the latter it can be derived systematically for all
 collections, case classes and enums.
 
+Using lifting, we can now give the missing definition of `showExpr` in the introductory example:
+
+    def showExpr[T](expr: Expr[T]): Expr[String] = expr.toString
+
+That is, the `showExpr` method converts its `Expr` argument to a string, and lifts
+the result back to an `Expr[String]` using the implicit `toExpr` conversion.
+
 ## Implementation
 
 ### Syntax changes
@@ -603,9 +609,9 @@ The syntax of terms, values, and types is given as follows:
                           ~t                splice
 
     Values        v  ::=  (x: T) => t       lambda
-                          ’q                pure quote
+                          ’u                quote
 
-    Quoted        q  ::=  x  |  (x: T) => q  |  q q  |  ’t
+    Simple terms  u  ::=  x  |  (x: T) => u  |  u u  |  ’t
 
     Types         T  ::=  A                 base type
                           T -> T            function type
@@ -635,7 +641,7 @@ We define a small step reduction relation `-->` with the following rules:
 
                 ((x: T) => t) v  -->  [x := v]t
 
-                          ~(’t)  -->  t
+                          ~(’u)  -->  u
 
                              t1  -->  t2
                           -----------------
@@ -648,7 +654,7 @@ position of an evaluation context.  Evaluation contexts `e` and
 splice evaluation context `e_s` are defined syntactically as follows:
 
     Eval context    e    ::=  [ ]  |  e t  |  v e  |  ’e_s[~e]
-    Splice context  e_s  ::=  [ ]  |  (x: T) => e_s  |  e_s t  |  q e_s
+    Splice context  e_s  ::=  [ ]  |  (x: T) => e_s  |  e_s t  |  u e_s
 
 ### Typing rules
 
@@ -695,6 +701,9 @@ environments and terms.
                            ----------------
                            Es |- ’t: expr T
 
+The meta theory of a slightly simplified variant 2-stage variant of this calculus
+is studied [separatey](../simple-smp.md)
+
 ## Going Further
 
 The meta-programming framework as presented and currently implemented is quite restrictive

tests/pos/quote-0.scala

@@ -9,7 +9,9 @@ class Test {
       ~ assertImpl('(expr))
 
     def assertImpl(expr: Expr[Boolean]) =
-      '{ if !(~expr) then throw new AssertionError(s"failed assertion: ${~expr}") }
+      '{ if !(~expr) then throw new AssertionError(s"failed assertion: ${~showExpr(expr)}") }
+
+    def showExpr[T](expr: Expr[T]): Expr[String] = expr.toString
 
     inline def power(inline n: Int, x: Double) = ~powerCode(n, '(x))