Last time: effects
effect E : t
1/ 38
This time: staging
.< e >.
2/ 38
Review: abstraction
Lambda abstraction
λx : A.M
ΛA :: K .M
λA :: K .B
First-class ∀ and ∃
type t = { f: ’a. . . . }
type t = E : ’a s → t
Modular abstraction
module F(X : T) = . . .
let f {X:T} = . . .
Abstraction of type equalities
a ≡ b
Interfaces to computation
m >>= k f ⊗ p
effect E:t
Abstraction over data shape
val show :
{D:DATA} → ’a → string
3/ 38
The cost of ignorance
Fewer opportunities for optimization
let both_eq1 : int * int → int * int → bool =
fun (x1 , y1) (x2 , y2) →
x1 = x2 && y1 = y2
let both_eq2 : (int → int → bool) →
int * int → int * int → bool =
fun eq (x1, y1) (x2, y2) →
eq x1 x2 && eq y1 y2
both_eq2 (fun x y → x = y)
type eq = { eq: ’a. ’a → ’a → bool }
let both_eq {eq} (x1, y1) (x2, y2) =
eq x1 x2 && eq y1 y2
4/ 38
The cost of ignorance
Interpretative overhead
let print_int_pair (x,y) =
print_char ’(’;
print_int x;
print_char ’,’;
print_int y;
print_char ’)’
let print_int_pair2 (x,y) =
Printf.sprintf “(%d,%d)” x y
let print_int_pair3 (x,y) =
print_string (gshow (pair int int) (x, y))
5/ 38
Abstraction wants to be free
let pow2 x = x * x (* x2 *)
let pow3 x = x * x * x (* x3 *)
let pow5 x = x * x * x * x * x (* x5 *)
let rec pow x n = (* xn *)
if n = 0 then 1
else x * pow x (n – 1)
val pow : int → int → int
6/ 38
Power, staged
let rec pow x n =
if n = 0 then .< 1 >.
else .<.~x * .~(pow x (n - 1)) >.
7/ 38
Power, staged
let rec pow x n =
if n = 0 then .< 1 >.
else .<.~x * .~(pow x (n - 1)) >.
val pow : int code → int → int code
8/ 38
Power, staged
let rec pow x n =
if n = 0 then .< 1 >.
else .<.~x * .~(pow x (n - 1)) >.
val pow : int code → int → int code
let pow_code n = .< fun x → .~(pow .
9/ 38
Power, staged
let rec pow x n =
if n = 0 then .< 1 >.
else .<.~x * .~(pow x (n - 1)) >.
val pow : int code → int → int code
let pow_code n = .< fun x → .~(pow .
val pow_code : int → (int → int) code
10/ 38
Power, staged
let rec pow x n =
if n = 0 then .< 1 >.
else .<.~x * .~(pow x (n - 1)) >.
val pow : int code → int → int code
let pow_code n = .< fun x → .~(pow .
val pow_code : int → (int → int) code
# pow_code 3;;
.
11/ 38
Power, staged
let rec pow x n =
if n = 0 then .< 1 >.
else .<.~x * .~(pow x (n - 1)) >.
val pow : int code → int → int code
let pow_code n = .< fun x → .~(pow .
val pow_code : int → (int → int) code
# pow_code 3;;
.
# let pow3 ’ = !. (pow_code 3);;
val pow3 ’ : int → int =
12/ 38
Power, staged
let rec pow x n =
if n = 0 then .< 1 >.
else .<.~x * .~(pow x (n - 1)) >.
val pow : int code → int → int code
let pow_code n = .< fun x → .~(pow .
val pow_code : int → (int → int) code
# pow_code 3;;
.
# let pow3 ’ = !. (pow_code 3);;
val pow3 ’ : int → int =
# pow3 ’ 4;;
– : int = 64
13/ 38
MetaOCaml basics
14/ 38
Quoting
let x = “w” in
let y = “x” in
print_string (x ^ y)
let x = “w” in
let y = x in
print_string (x ^ y)
let x = “w” in
let y = x in
print_string (“x ^ y”)
let x = “w” in
let y = x in
print_string (“x” ^ y)
Quoting prevents evaluation.
15/ 38
Quoting code
MetaOCaml: multi-stage programming with code quoting.
Stages: current (available now) and delayed (available later).
(Also double-delayed, triple-delayed, etc.)
Brackets
.
Escaping (within brackets)
.~e
Running code
!. e
Cross-stage persistence
.
Goal: generate a specialized program with better performance
16/ 38
Quoting and escaping: some examples
.<3 >.
.<1 + 2 >.
.<[1; 2; 3] >.
.
.
.<(.~f) 3 >.
.<.~(f 3)>.
.
17/ 38
Quoting: typing
Γ ⊢n e : τ
Γ ⊢n+ e : τ
T-bracket
Γ ⊢n .
Γ ⊢n e : τ code T-escape
Γ ⊢n+ .~e : τ
Γ+ ⊢n e : τ code
T-run
Γ ⊢n !. e : τ
Γ(x) = τ (n−m)
T-var
Γ ⊢n : τ
18/ 38
Quoting: open code
Open code (supports symbolic computation)
let pow_code n = .< fun x → .~(pow .
Cross-stage persistence
let print_int_pair (x,y) =
Printf.printf “(%d,%d)” x y
let pairs = .< [(3, 4); (5, 6)] >.
.< List.iter print_int_pair .~pairs >.
19/ 38
Quoting: scoping
Scoping is lexical, just as in OCaml.
.< fun x → .~( let x = 3 in .
let x = 3 in .< fun x → .~( .
MetaOCaml renames variables to avoid clashes:
.< let x = 3 in
.~(let y = .
.< fun x → .~y + x >.) >.
20/ 38
Quoting: scoping
Scoping is lexical, just as in OCaml.
.< fun x → .~( let x = 3 in .
let x = 3 in .< fun x → .~( .
MetaOCaml renames variables to avoid clashes:
# .< let x = 3 in
.~(let y = .
.< fun x → .~y + x >.) >.;;
– : (int → int) code =
.
21/ 38
Learning from mistakes
22/ 38
Error: quoting nonsense
.< 1 + "two" >.
23/ 38
Error: quoting nonsense
# .< 1 + "two" >.;;
Characters 7-12:
.< 1 + "two" >.;;
^^^^^
Error: This expression has type string but an
expression was expected of type int
24/ 38
Error: looking into the future
.< fun x → .~( x ) >.
25/ 38
Error: looking into the future
# .< fun x → .~( x ) >.;;
Characters 14-19:
.< fun x → .~( x ) >.;;
^^^^^
Error: A variable that was bound within brackets is
used outside brackets
for example: .
Hint: enclose the variable in brackets ,
as in: .
26/ 38
Error: escape from nowhere
let x = .< 3 >. in .~x
27/ 38
Error: escape from nowhere
# let x = .< 3 >. in .~x;;
Characters 22-23:
let x = .< 3 >. in .~x;;
^
Error: An escape may appear only within brackets
28/ 38
Error: running open code
.< fun x → .~(!. .
29/ 38
Error: running open code
# .< fun x → .~(!. .
Exception:
Failure
“The code built at Characters 7-8:\n
.< fun x → .~(!. .< x >. ) >.;;\n
^\n
is not closed: identifier x_2 bound at
Characters 7-8:\n
.< fun x → .~(!. .< x >. ) >.;;\n
^\n
is free”.
30/ 38
Learning by doing
31/ 38
The staging process, idealized
1. Write the program as usual:
val program : t_sta → t_dyn → t
2. Add staging annotations:
val staged_program : t_sta → t_dyn code → t code
3. Compile using back:
val back: (’a code → ’b code) → (’a → ’b) code
val code_generator : t_sta → (t_dyn → t)
4. Construct static inputs:
val s : t_sta
5. Apply code generator to static inputs:
val specialized_code : (t_dyn → t) code
6. Run specialized code to build a specialized function:
val specialized_function : t_dyn → t
32/ 38
The staging process, idealized
1. Write the program as usual:
val program : t_sta → t_dyn → t
2. Add staging annotations:
val staged_program : t_sta → t_dyn code → t code
3. Compile using back:
val back: (’a code → ’b code) → (’a → ’b) code
val code_generator : t_sta → (t_dyn → t)
4. Construct static inputs:
val s : t_sta
5. Apply code generator to static inputs:
val specialized_code : (t_dyn → t) code
6. Run specialized code to build a specialized function:
val specialized_function : t_dyn → t
32/ 38
The staging process, idealized
1. Write the program as usual:
val program : t_sta → t_dyn → t
2. Add staging annotations:
val staged_program : t_sta → t_dyn code → t code
3. Compile using back:
val back: (’a code → ’b code) → (’a → ’b) code
val code_generator : t_sta → (t_dyn → t)
4. Construct static inputs:
val s : t_sta
5. Apply code generator to static inputs:
val specialized_code : (t_dyn → t) code
6. Run specialized code to build a specialized function:
val specialized_function : t_dyn → t
32/ 38
The staging process, idealized
1. Write the program as usual:
val program : t_sta → t_dyn → t
2. Add staging annotations:
val staged_program : t_sta → t_dyn code → t code
3. Compile using back:
val back: (’a code → ’b code) → (’a → ’b) code
val code_generator : t_sta → (t_dyn → t)
4. Construct static inputs:
val s : t_sta
5. Apply code generator to static inputs:
val specialized_code : (t_dyn → t) code
6. Run specialized code to build a specialized function:
val specialized_function : t_dyn → t
32/ 38
The staging process, idealized
1. Write the program as usual:
val program : t_sta → t_dyn → t
2. Add staging annotations:
val staged_program : t_sta → t_dyn code → t code
3. Compile using back:
val back: (’a code → ’b code) → (’a → ’b) code
val code_generator : t_sta → (t_dyn → t)
4. Construct static inputs:
val s : t_sta
5. Apply code generator to static inputs:
val specialized_code : (t_dyn → t) code
6. Run specialized code to build a specialized function:
val specialized_function : t_dyn → t
32/ 38
The staging process, idealized
1. Write the program as usual:
val program : t_sta → t_dyn → t
2. Add staging annotations:
val staged_program : t_sta → t_dyn code → t code
3. Compile using back:
val back: (’a code → ’b code) → (’a → ’b) code
val code_generator : t_sta → (t_dyn → t)
4. Construct static inputs:
val s : t_sta
5. Apply code generator to static inputs:
val specialized_code : (t_dyn → t) code
6. Run specialized code to build a specialized function:
val specialized_function : t_dyn → t
32/ 38
Inner product
let dot
: int → float array → float array → float
= fun n l r →
let rec loop i =
if i = n then 0.
else l.(i) *. r.(i)
+. loop (i + 1)
in loop 0
33/ 38
Inner product, loop unrolling
let dot ’
: int → float array code → float array code → float code
= fun n l r →
let rec loop i =
if i = n then .< 0. >.
else .< ((.~l).(i) *. (.~r).(i))
+. .~(loop (i + 1)) >.
in loop 0
34/ 38
Inner product, loop unrolling
# .< fun l r → .~(dot ’ 3 .
– : (float array → float array → float) code =
.< fun l r →
(l.(0) *. r.(0)) +.
((l.(1) *. r.(1)) +. ((l.(2) *. r.(2)) +. 0.))>.
35/ 38
Inner product, eliding no-ops
let dot ’’
: float array → float array code → float code =
fun l r →
let n = Array.length l in
let rec loop i =
if i = n then .< 0. >.
else match l.(i) with
0.0 → loop (i + 1)
| 1.0 → .<(.~r).(i) +. .~(loop (i + 1)) >.
| x → .<(x *. (.~r).(i)) +. .~(loop (i + 1)) >.
in loop 0
36/ 38
Inner product, eliding no-ops
# .< fun r → .~(dot ’’ [| 1.0; 0.0; 3.5 |] .
– : (float array → float) code =
.< fun r → r.(0) +. ((3.5 *. r.(2)) +. 0.)>.
37/ 38
Next: partially-static data; staged generic programming
type ’u genericQ = {D:DATA} → D.t code → ’u code
38/ 38