Skip to content

Commit 08e6735

Browse files
oderskyodersky
authored
Merge pull request #3698 from dotty-staging/simple-smp
Fixes and extensions to symmetric meta programming docs
2 parents 1ab6027 + dea5715 commit 08e6735

File tree

3 files changed

+262
-15
lines changed

3 files changed

+262
-15
lines changed

‎docs/docs/reference/simple-smp.md

Lines changed: 236 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,236 @@
1+
---
2+
layout: doc-page
3+
title: "The Meta-theory of Symmetric Meta-programming"
4+
---
5+
6+
# The Meta-theory of Symmetric Meta-programming
7+
8+
23.12.2017
9+
10+
This note presents a simplified variant of
11+
[symmetric meta-programming](./symmetric-meta-programming.md)
12+
and sketches its soundness proof. The variant treats only dialogues
13+
between two stages. A program can have quotes which can contain
14+
splices (which can contain quotes, which can contain splices, and so
15+
on). Or the program could start with a splice with embedded
16+
quotes. The essential restriction is that (1) a term can contain top-level
17+
quotes or top-level splices, but not both, and (2) quotes cannot appear
18+
directly inside quotes and splices cannot appear directly inside
19+
splices. In other words, the universe is restricted to two phases
20+
only.
21+
22+
Under this restriction we can simplify the typing rules so that there are
23+
always exactly two environments instead of having a stack of environments.
24+
The variant presented here differs from the full calculus also in that we
25+
replace evaluation contexts with contextual typing rules. While this
26+
is more verbose, it makes it easier to set up the meta theory.
27+
28+
## Syntax
29+
30+
Terms t ::= x variable
31+
(x: T) => t lambda
32+
t t application
33+
’t quote
34+
~t splice
35+
36+
Simple terms u ::= x | (x: T) => u | u u
37+
38+
Values v ::= (x: T) => t lambda
39+
’u quoted value
40+
41+
Types T ::= A base type
42+
T -> T function type
43+
’T quoted type
44+
45+
## Operational semantics
46+
47+
### Evaluation
48+
49+
((x: T) => t) v --> [x := v]t
50+
51+
t1 --> t2
52+
---------------
53+
t1 t --> t2 t
54+
55+
t1 --> t2
56+
---------------
57+
v t1 --> v t2
58+
59+
t1 ==> t2
60+
-------------
61+
’t1 --> ’t2
62+
63+
64+
### Splicing
65+
66+
~’u ==> u
67+
68+
t1 ==> t2
69+
-------------------------------
70+
(x: T) => t1 ==> (x: T) => t2
71+
72+
t1 ==> t2
73+
---------------
74+
t1 t ==> t2 t
75+
76+
t1 ==> t2
77+
---------------
78+
u t1 ==> u t2
79+
80+
t1 --> t2
81+
-------------
82+
~t1 ==> ~t2
83+
84+
85+
## Typing Rules
86+
87+
Typing judgments are of the form `E1 * E2 |- t: T` where `E1, E2` are environments and
88+
`*` is one of `~` and `’`.
89+
90+
x: T in E2
91+
---------------
92+
E1 * E2 |- x: T
93+
94+
95+
E1 * E2, x: T1 |- t: T2
96+
--------------------------------
97+
E1 * E2 |- (x: T1) => t: T -> T2
98+
99+
100+
E1 * E2 |- t1: T2 -> T E1 * E2 |- t2: T2
101+
-------------------------------------------
102+
E1 * E2 |- t1 t2: T
103+
104+
105+
E2 ’ E1 |- t: T
106+
-----------------
107+
E1 ~ E2 |- ’t: ’T
108+
109+
110+
E2 ~ E1 |- t: ’T
111+
----------------
112+
E1 ’ E2 |- ~t: T
113+
114+
115+
(Curiously, this looks a bit like a Christmas tree).
116+
117+
## Soundness
118+
119+
The meta-theory typically requires mutual inductions over two judgments.
120+
121+
### Progress Theorem
122+
123+
1. If `E1 ~ |- t: T` then either `t = v` for some value `v` or `t --> t2` for some term `t2`.
124+
2. If ` ’ E2 |- t: T` then either `t = u` for some simple term `u` or `t ==> t2` for some term `t2`.
125+
126+
Proof by structural induction over terms.
127+
128+
To prove (1):
129+
130+
- the cases for variables, lambdas and applications are as in STL.
131+
- If `t = ’t2`, then by inversion we have ` ’ E1 |- t2: T2` for some type `T2`.
132+
By the second I.H., we have one of:
133+
- `t2 = u`, hence `’t2` is a value,
134+
- `t2 ==> t3`, hence `’t2 --> ’t3`.
135+
- The case `t = ~t2` is not typable.
136+
137+
To prove (2):
138+
139+
- If `t = x` then `t` is a simple term.
140+
- If `t = (x: T) => t2`, then either `t2` is a simple term, in which case `t` is as well.
141+
Or by the second I.H. `t2 ==> t3`, in which case `t ==> (x: T) => t3`.
142+
- If `t = t1 t2` then one of three cases applies:
143+
144+
- `t1` and `t2` are a simple term, then `t` is as well a simple term.
145+
- `t1` is not a simple term. Then by the second IH, `t1 ==> t12`, hence `t ==> t12 t2`.
146+
- `t1` is a simple term but `t2` is not. Then by the second IH. `t2 ==> t22`, hence `t ==> t1 t22`.
147+
148+
- The case `t = ’t2` is not typable.
149+
- If `t = ~t2` then by inversion we have `E2 ~ |- t2: ’T2`, for some some type `T2`.
150+
By the first I.H., we have one of
151+
152+
- `t2 = v`. Since `t2: ’T2`, we must have `v = ’u`, for some simple term `u`, hence `t = ~’u`.
153+
By quote-splice reduction, `t ==> u`.
154+
- `t2 --> t3`. Then by the context rule for `’t`, `t ==> ’t3`.
155+
156+
157+
### Substitution Lemma
158+
159+
1. If `E1 ~ E2 |- s: S` and `E1 ~ E2, x: S |- t: T` then `E1 ~ E2 |- [x := s]t: T`.
160+
2. If `E1 ~ E2 |- s: S` and `E2, x: S ’ E1 |- t: T` then `E2 ’ E1 |- [x := s]t: T`.
161+
162+
The proofs are by induction on typing derivations for `t`, analogous
163+
to the proof for STL (with (2) a bit simpler than (1) since we do not
164+
need to swap lambda bindings with the bound variable `x`). The
165+
arguments that link the two hypotheses are as follows.
166+
167+
To prove (1), let `t = ’t1`. Then `T = ’T1` for some type `T1` and the last typing rule is
168+
169+
E2, x: S ’ E1 |- t1: T1
170+
-------------------------
171+
E1 ~ E2, x: S |- ’t1: ’T1
172+
173+
By the second I.H. `E2 ’ E1 |- [x := s]t1: T1`. By typing, `E1 ~ E2 |- ’[x := s]t1: ’T1`.
174+
Since `[x := s]t = [x := s](’t1) = ’[x := s]t1` we get `[x := s]t: ’T1`.
175+
176+
To prove (2), let `t = ~t1`. Then the last typing rule is
177+
178+
E1 ~ E2, x: S |- t1: ’T
179+
-----------------------
180+
E2, x: S ’ E1 |- ~t1: T
181+
182+
By the first I.H., `E1 ~ E2 |- [x := s]t1: ’T`. By typing, `E2 ’ E1 |- ~[x := s]t1: T`.
183+
Since `[x := s]t = [x := s](~t1) = ~[x := s]t1` we get `[x := s]t: T`.
184+
185+
186+
### Preservation Theorem
187+
188+
1. If `E1 ~ E2 |- t1: T` and `t1 --> t2` then `E1 ~ E2 |- t2: T`.
189+
2. If `E1 ’ E2 |- t1: T` and `t1 ==> t2` then `E1 ’ E2 |- t2: T`.
190+
191+
The proof is by structural induction on evaluation derivations. The proof of (1) is analogous
192+
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:
193+
194+
- Assume the last rule was
195+
196+
t1 ==> t2
197+
-------------
198+
’t1 --> ’t2
199+
200+
By inversion of typing rules, we must have `T = ’T1` for some type `T1` such that `t1: T1`.
201+
By the second I.H., `t2: T1`, hence `’t2: `T1`.
202+
203+
204+
To prove (2):
205+
206+
- Assume the last rule was `~’u ==> u`. The typing proof of `~’u` must have the form
207+
208+
209+
E1 ’ E2 |- u: T
210+
-----------------
211+
E1 ~ E2 |- ’u: ’T
212+
-----------------
213+
E1 ’ E2 |- ~’u: T
214+
215+
Hence, `E1 ’ E2 |- u: T`.
216+
217+
- Assume the last rule was
218+
219+
t1 ==> t2
220+
-------------------------------
221+
(x: S) => t1 ==> (x: T) => t2
222+
223+
By typing inversion, `E1 ' E2, x: S |- t1: T1` for some type `T1` such that `T = S -> T1`.
224+
By the I.H, `t2: T1`. By the typing rule for lambdas the result follows.
225+
226+
- The context rules for applications are equally straightforward.
227+
228+
- Assume the last rule was
229+
230+
t1 ==> t2
231+
-------------
232+
~t1 ==> ~t2
233+
234+
By inversion of typing rules, we must have `t1: ’T`.
235+
By the first I.H., `t2: ’T`, hence `~t2: T`.
236+

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

Lines changed: 23 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,7 @@ prints it again in an error message if it evaluates to `false`.
3232
~ assertImpl(’(expr))
3333

3434
def assertImpl(expr: Expr[Boolean]) =
35-
’{ if !(~expr) then throw new AssertionError(s"failed assertion: ${~expr}") }
36-
35+
’{ if !(~expr) then throw new AssertionError(s"failed assertion: ${~showExpr(expr)}") }
3736

3837
If `e` is an expression, then `’(e)` or `’{e}` represent the typed
3938
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:
491490
The conversion says that values of types implementing the `Liftable`
492491
type class can be converted ("lifted") automatically to `Expr`
493492
values. Dotty comes with instance definitions of `Liftable` for
494-
several types including all underlying types of literals. For example,
495-
`Int` values can be converted to `Expr[Int]` values by wrapping the
496-
value in a `Literal` tree node. This makes use of the underlying tree
497-
representation in the compiler for efficiency. But the `Liftable`
498-
instances are nevertheless not "magic" in the sense that they could
499-
all be defined in a user program without knowing anything about the
500-
representation of `Expr` trees. For instance, here is a possible
501-
instance of `Liftable[Boolean]`:
493+
several types including `Boolean`, `String`, and all primitive number
494+
types. For example, `Int` values can be converted to `Expr[Int]`
495+
values by wrapping the value in a `Literal` tree node. This makes use
496+
of the underlying tree representation in the compiler for
497+
efficiency. But the `Liftable` instances are nevertheless not "magic"
498+
in the sense that they could all be defined in a user program without
499+
knowing anything about the representation of `Expr` trees. For
500+
instance, here is a possible instance of `Liftable[Boolean]`:
502501

503502
implicit def BooleanIsLiftable: Liftable[Boolean] = new {
504503
implicit def toExpr(b: Boolean) = if (b) ’(true) else ’(false)
@@ -532,6 +531,13 @@ In the end, `Liftable` resembles very much a serialization
532531
framework. Like the latter it can be derived systematically for all
533532
collections, case classes and enums.
534533

534+
Using lifting, we can now give the missing definition of `showExpr` in the introductory example:
535+
536+
def showExpr[T](expr: Expr[T]): Expr[String] = expr.toString
537+
538+
That is, the `showExpr` method converts its `Expr` argument to a string, and lifts
539+
the result back to an `Expr[String]` using the implicit `toExpr` conversion.
540+
535541
## Implementation
536542

537543
### Syntax changes
@@ -603,9 +609,9 @@ The syntax of terms, values, and types is given as follows:
603609
~t splice
604610

605611
Values v ::= (x: T) => t lambda
606-
’q pure quote
612+
’u quote
607613

608-
Quoted q ::= x | (x: T) => q | q q | ’t
614+
Simple terms u ::= x | (x: T) => u | u u | ’t
609615

610616
Types T ::= A base type
611617
T -> T function type
@@ -635,7 +641,7 @@ We define a small step reduction relation `-->` with the following rules:
635641

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

638-
~(’t) --> t
644+
~(’u) --> u
639645

640646
t1 --> t2
641647
-----------------
@@ -648,7 +654,7 @@ position of an evaluation context. Evaluation contexts `e` and
648654
splice evaluation context `e_s` are defined syntactically as follows:
649655

650656
Eval context e ::= [ ] | e t | v e | ’e_s[~e]
651-
Splice context e_s ::= [ ] | (x: T) => e_s | e_s t | q e_s
657+
Splice context e_s ::= [ ] | (x: T) => e_s | e_s t | u e_s
652658

653659
### Typing rules
654660

@@ -695,6 +701,9 @@ environments and terms.
695701
----------------
696702
Es |- ’t: expr T
697703

704+
The meta theory of a slightly simplified variant 2-stage variant of this calculus
705+
is studied [separatey](../simple-smp.md)
706+
698707
## Going Further
699708

700709
The meta-programming framework as presented and currently implemented is quite restrictive

‎tests/pos/quote-0.scala

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,9 @@ class Test {
99
~ assertImpl('(expr))
1010

1111
def assertImpl(expr: Expr[Boolean]) =
12-
'{ if !(~expr) then throw new AssertionError(s"failed assertion: ${~expr}") }
12+
'{ if !(~expr) then throw new AssertionError(s"failed assertion: ${~showExpr(expr)}") }
13+
14+
def showExpr[T](expr: Expr[T]): Expr[String] = expr.toString
1315

1416
inline def power(inline n: Int, x: Double) = ~powerCode(n, '(x))
1517

0 commit comments

Comments
 (0)