From 8cf0b32869b476b734e235c57d8531ae9c20e101 Mon Sep 17 00:00:00 2001 From: Martin Odersky Date: Sat, 23 Dec 2017 14:33:10 +0100 Subject: [PATCH 1/5] Fixes to meta-programming doc --- .../reference/symmetric-meta-programming.md | 36 ++++++++++++------- 1 file changed, 23 insertions(+), 13 deletions(-) diff --git a/docs/docs/reference/symmetric-meta-programming.md b/docs/docs/reference/symmetric-meta-programming.md index c198a08c1fa5..125814d71557 100644 --- a/docs/docs/reference/symmetric-meta-programming.md +++ b/docs/docs/reference/symmetric-meta-programming.md @@ -32,7 +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: ${~expr.toString}") } If `e` is an expression, then `’(e)` or `’{e}` represent the typed @@ -491,14 +491,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 +532,16 @@ 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. +In fact, the initial example of assertions also uses a lifting conversion under the hood. +Recall the failure clause: + + throw new AssertionError(s"failed assertion: ${~expr.toString}") } + +Here, `expr.toString` yields `expr`'s representation in String form. That string +is lifted to an `Expr[String]` since the required type of a splice argument is an `Expr`. +The lifted result is then spliced in into the `AssertionError` argument, giving +back again the original string representation of `expr`. + ## Implementation ### Syntax changes @@ -603,9 +613,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 +645,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 +658,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 From e33bd4266591e186f65ccdd26f1a4708ab5500da Mon Sep 17 00:00:00 2001 From: Martin Odersky Date: Sat, 23 Dec 2017 14:33:53 +0100 Subject: [PATCH 2/5] A simplified calculus with a sketch of its meta theory. --- docs/docs/reference/simple-smp.md | 229 ++++++++++++++++++++++++++++++ 1 file changed, 229 insertions(+) create mode 100644 docs/docs/reference/simple-smp.md diff --git a/docs/docs/reference/simple-smp.md b/docs/docs/reference/simple-smp.md new file mode 100644 index 000000000000..069995674d75 --- /dev/null +++ b/docs/docs/reference/simple-smp.md @@ -0,0 +1,229 @@ +# Simple Symmetric Metaprogramming + +23.12.2017 + +This note presents a simplified variant of symmetric metaprogramming +which only treats dialgogues between two stages. We could have quotes +containing splices (which can contain quotes, which can contain +splices, and so on). Or we could start with a splice with embedded +quotes. The important restriction is that (1) a term contains toplevel +quotes or toplevel 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 + + + E1 ’ E2 |- t: T + ----------------- + E1 ~ E2 |- ’t: ’T + + + E1 ~ E2 |- 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 judgements. + +### 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 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`. + From 26682abdf7979e37444980b6cd175849f22d8ff5 Mon Sep 17 00:00:00 2001 From: Martin Odersky Date: Sat, 23 Dec 2017 17:46:19 +0100 Subject: [PATCH 3/5] Fix typos and add layout tag --- docs/docs/reference/simple-smp.md | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/docs/docs/reference/simple-smp.md b/docs/docs/reference/simple-smp.md index 069995674d75..177fa68fca59 100644 --- a/docs/docs/reference/simple-smp.md +++ b/docs/docs/reference/simple-smp.md @@ -1,13 +1,19 @@ -# Simple Symmetric Metaprogramming +--- +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 metaprogramming -which only treats dialgogues between two stages. We could have quotes -containing splices (which can contain quotes, which can contain -splices, and so on). Or we could start with a splice with embedded -quotes. The important restriction is that (1) a term contains toplevel -quotes or toplevel splices, but not both and (2) quotes cannot appear +This note presents a simplified variant of symmetric meta-programming +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. @@ -95,12 +101,12 @@ Typing judgments are of the form `E1 * E2 |- t: T` where `E1, E2` are environme E1 * E2 |- t1 t2: T - E1 ’ E2 |- t: T + E2 ’ E1 |- t: T ----------------- E1 ~ E2 |- ’t: ’T - E1 ~ E2 |- t: ’T + E2 ~ E1 |- t: ’T ---------------- E1 ’ E2 |- ~t: T @@ -109,7 +115,7 @@ Typing judgments are of the form `E1 * E2 |- t: T` where `E1, E2` are environme ## Soundness -The meta-theory typically requires mutual inductions over two judgements. +The meta-theory typically requires mutual inductions over two judgments. ### Progress Theorem @@ -122,7 +128,7 @@ 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 second I.H., we have one of: + 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. @@ -150,7 +156,7 @@ To prove (2): ### 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`. + 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 From 5f0d35e3bf93bc3c44c7ded89875b904c4b183da Mon Sep 17 00:00:00 2001 From: Martin Odersky Date: Sun, 24 Dec 2017 11:25:24 +0100 Subject: [PATCH 4/5] Fixes to the assertImpl example Make sure `assertImpl` prints the tested expression rather than its result. --- docs/docs/reference/symmetric-meta-programming.md | 14 +++++--------- tests/pos/quote-0.scala | 4 +++- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/docs/docs/reference/symmetric-meta-programming.md b/docs/docs/reference/symmetric-meta-programming.md index 125814d71557..be2d42ccadfa 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.toString}") } - + ’{ 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]` @@ -532,15 +531,12 @@ 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. -In fact, the initial example of assertions also uses a lifting conversion under the hood. -Recall the failure clause: +Using lifting, we can now give the missing definition of `showExpr` in the introductory example: - throw new AssertionError(s"failed assertion: ${~expr.toString}") } + def showExpr[T](expr: Expr[T]): Expr[String] = expr.toString -Here, `expr.toString` yields `expr`'s representation in String form. That string -is lifted to an `Expr[String]` since the required type of a splice argument is an `Expr`. -The lifted result is then spliced in into the `AssertionError` argument, giving -back again the original string representation of `expr`. +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 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)) From dea5715dd7f2ac218e9318ffe69582ecc491096c Mon Sep 17 00:00:00 2001 From: Martin Odersky Date: Sat, 13 Jan 2018 20:25:51 +0100 Subject: [PATCH 5/5] Add links Add links between symmetric-meta-programming and simple-smp. --- docs/docs/reference/simple-smp.md | 7 ++++--- docs/docs/reference/symmetric-meta-programming.md | 3 +++ 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/docs/docs/reference/simple-smp.md b/docs/docs/reference/simple-smp.md index 177fa68fca59..733810d4cd19 100644 --- a/docs/docs/reference/simple-smp.md +++ b/docs/docs/reference/simple-smp.md @@ -7,11 +7,12 @@ title: "The Meta-theory of Symmetric Meta-programming" 23.12.2017 -This note presents a simplified variant of symmetric meta-programming +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 +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 +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 diff --git a/docs/docs/reference/symmetric-meta-programming.md b/docs/docs/reference/symmetric-meta-programming.md index be2d42ccadfa..95141f1a0ce1 100644 --- a/docs/docs/reference/symmetric-meta-programming.md +++ b/docs/docs/reference/symmetric-meta-programming.md @@ -701,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