diff --git a/docs/docs/reference/simple-smp.md b/docs/docs/reference/simple-smp.md new file mode 100644 index 000000000000..733810d4cd19 --- /dev/null +++ b/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`. + diff --git a/docs/docs/reference/symmetric-meta-programming.md b/docs/docs/reference/symmetric-meta-programming.md index c198a08c1fa5..95141f1a0ce1 100644 --- a/docs/docs/reference/symmetric-meta-programming.md +++ b/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 diff --git a/tests/pos/quote-0.scala b/tests/pos/quote-0.scala index 8372c6414cde..e080af70620f 100644 --- a/tests/pos/quote-0.scala +++ b/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))