程序代写代做代考 ocaml Last time: effects

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 .. n) >.

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 .. n) >.

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 .. n) >.

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 .. n) >.

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 .. n) >.

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 .. : τ code

Γ ⊢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 .. n) >.

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 = .. in

.< 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 = .. in

.< 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: . .~( foo x) >.

Hint: enclose the variable in brackets ,

as in: . .~(foo ..) >.;;

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