程序代写代做代考 scheme Last time: staging basics

generate_loop (fun e →.< .~e ^ "\n" >.)
⇝
.< fun e → for i = 0 to 10 do print (e ^ "\n") (* repeated work! *) done >.

What we need: A way to insert let bindings at outer levels

.< fun e → let c = e ^ "\n" in for i = 0 to 10 do print c done >.

16/ 41

let insertion: a simple implementation

let insertion as an effect

effect GenLet : ’a code → ’a code

let genlet v = perform (GenLet v)

Handling let insertion

let let_locus : (unit → ’a code) → ’a code =
fun f → match f () with
| x → x
| effect (GenLet e) k →
.< let x = .~e in .~(continue k .< x >.)>.

17/ 41

let insertion in action

Example

let_locus

(fun () →
.< w + .~(genlet .< y + z >.) >.)

Captured continuation

.< w + .~( - ) >.

let generation

| effect (GenLet e) k →
.< let x = .~e in .~(continue k .< x >.)>.

Result

.< let x = y + z in w + x >.

18/ 41

Where to insert let?

Sometimes there are several possible insertion points for let

For example, consider the following program:

.< fun y → y + .~(genlet e) >.

We could insert let beneath the binding for y

.< fun y → let x = .~e in y + x >.

Or above:

.< let x = .~e in fun y → y + x >.

We typically want the highest point where e is well-scoped.

19/ 41

let insertion at the outermost valid point
Is e well-scoped at this point in the program?

let is_well_scoped e =

try ignore .< (.~e; ()) >.; true
with _ → false

genlet defaults to insertion-in-place

let genlet v =

try perform (GenLet v)

with Unhandled → v

let_locus searches the stack for the highest suitable handler

let let_locus body =

try body ()

with effect (GenLet e) k when is_well_scoped e →
match perform (GenLet e) with

| v → continue k v
| exception Unhandled →
.< let x = .~e in .~(continue k .< x >.)>.

20/ 41

let rec insertion

Question: how can we generate (mutually) recursive functions?

let rec evenp x = x = 0 || oddp (x – 1)

and oddp x = not (evenp x)

Difficulty: constructing binding groups of unknown size

Observation: n-ary operators are difficult to abstract!

21/ 41

Recursion via references (Landin’s knot)

let evenp = ref (fun _ → assert false)
let oddp = ref (fun _ → assert false)

evenp := fun x → x = 0 || !oddp (pred x)
oddp := fun x → not (!evenp x)

What if evenp and oddp generated in different parts of the code?

Plan: use let-insertion to interleave bindings and assignments.

22/ 41

let rec insertion with references

letrec via genlet

val letrec : ((’a → ’b) code → (’a → ’b) code) →
(’a → ’b) code

let letrec k =

let r = genlet (.< ref (fun _ → assert false) >.) in
let _ = genlet (.<.~r := .~(k .< ! .~r >.) >.) in
.< ! .~r >.

letrec in action

let fib = let_locus @@ fun () →
letrec (fun f →

.< fun x → if x = 0 then 1 else x * .~f (x - 1) >.)
⇝
..

23/ 41

Staging generic programming

24/ 41

Generic programming recap

Type equality

val eqty : {A:TYPEABLE} → {B:TYPEABLE} →
(A.t, B.t) eq option

Generic shallow traversals

type ’u genericQ = {D:DATA} → D.t → ’u
val gmapQ : ’u genericQ → ’u list genericQ

Generic recursive schemes

let rec gshow {D:DATA} (v : D.t) =

“(“^ constructor_ v ^ concat ” ” (gmapQ gshow v) ^ “)”

gshow in action

gshow [1;2;3] ⇝ “(1 :: (2 :: (3 :: ([]))))”

25/ 41

Generic programming vs hand-written code

Generic show

let rec gshow {D:DATA} (v : D.t) =

“(“^ constructor_ v ^ concat ” ” (gmapQ gshow v) ^ “)”

Hand-written show

let rec show_list: (’a→ string)→’a list→ string =
fun f l →

match l with

| [] → “[]”
| h::t → “(“^ f h ^” :: “^ show_list f t ^”)”

Performance difference: an order of magnitude

Plan: turn gshow into a code generator

26/ 41

Generic programming vs hand-written code

Generic show

let rec gshow {D:DATA} (v : D.t) =

“(“^ constructor_ v ^ concat ” ” (gmapQ gshow v) ^ “)”

Hand-written show

let rec show_list: (’a→ string)→’a list→ string =
fun f l →

match l with

| [] → “[]”
| h::t → “(“^ f h ^” :: “^ show_list f t ^”)”

Performance difference: an order of magnitude

Plan: turn gshow into a code generator

26/ 41

Generic programming vs hand-written code

Generic show

let rec gshow {D:DATA} (v : D.t) =

“(“^ constructor_ v ^ concat ” ” (gmapQ gshow v) ^ “)”

Hand-written show

let rec show_list: (’a→ string)→’a list→ string =
fun f l →

match l with

| [] → “[]”
| h::t → “(“^ f h ^” :: “^ show_list f t ^”)”

Performance difference: an order of magnitude

Plan: turn gshow into a code generator

26/ 41

Generic programming: binding-time analysis

gshow {Data_list{Data_int }} [1; 2; 3]

Type representations are static Values are dynamic.

We’ve used type representations to traverse values.

Now we’ll use type representations to generate code.

Goal: generate code that contains no Typeable or Data values.

27/ 41

Generic programming, staged

Type equality (unchanged)

val eqty : {A:TYPEABLE} → {B:TYPEABLE} →
(A.t, B.t) eq option

Generic shallow traversals

type ’u genericQ = {D:DATA} → D.t code → ’u code
val gmapQ : ’u genericQ → ’u list genericQ

Generic recursive schemes

let gshow = gfixQ_ (fun self {D:DATA} v →
.< "("^ .~(constructor_ v) ^ concat " " .~(gmapQ_ self v) ^")" >.)

gshow in action

instantiate gshow ⇝ .< let rec show = ... >.

28/ 41

Staging gmapQ

The type of staged gmapQ

type ’u genericQ = {D:DATA} → D.t code → ’u code
val gmapQ : ’u genericQ → ’u list genericQ

Implementing staged gmapQ

implicit module rec DATA_list {A:DATA}

: DATA with type t = A.t list =

struct

let gmapQ q l =

.< match .~l with | [] → [] | h :: t → [.~(q .< h >.); .~(q .< t >.)] >.

(* . . . *)
end

29/ 41

Fixpoint operators

Problem: we can’t overload / redefine let rec

let rec gshow {D:DATA} (v : D.t) =

“(“^ constructor_ v

^ concat ” ” (gmapQ gshow v) ^ “)”

Solution: rewrite gshow using a fixpoint combinator

let rec gfixQ :

(u genericQ → u genericQ) → u genericQ =
fun f {D:DATA} x → f {D} (gfixQ f) x

let gshow = gfixQ (fun self {D:DATA} v →
“(“^ constructor_ v

^ concat ” ” (gmapQ self v) ^ “)”)

New problem: stage gfixQ

30/ 41

gfixQ: cyclic static structures

type tree =

Empty : tree

| Branch : branch → tree
and branch = tree * int * tree

tree

tree

branch

int

31/ 41

gfixQ: cyclic static structures

tree

tree

branch

int

32/ 41

gfixQ: cyclic static structures

tree

tree

branch

int

gshow tree

gshow branch

gshow tree

. . .

gshow intgshow tree

. . .

32/ 41

Background: memoization

Recursive functions can be inefficient

let rec fib = function

0 → 0
| 1 → 1
| n → fib (n – 1) + fib (n – 2)

33/ 41

Background: memoization

Recursive functions can be inefficient

let rec fib = function

0 → 0
| 1 → 1
| n → fib (n – 1) + fib (n – 2)

fib 4

33/ 41

Background: memoization

Recursive functions can be inefficient

let rec fib = function

0 → 0
| 1 → 1
| n → fib (n – 1) + fib (n – 2)

fib 4

fib 2fib 3

33/ 41

Background: memoization

Recursive functions can be inefficient

let rec fib = function

0 → 0
| 1 → 1
| n → fib (n – 1) + fib (n – 2)

fib 4

fib 2

fib 0fib 1

fib 3

fib 1fib 2

33/ 41

Background: memoization

Recursive functions can be inefficient

let rec fib = function

0 → 0
| 1 → 1
| n → fib (n – 1) + fib (n – 2)

fib 4

fib 2

fib 0fib 1

fib 3

fib 1fib 2

fib 0fib 1

33/ 41

Background: memoization
Recursive functions can be inefficient — use memoization

val memoize : ((’a → ’b) → (’a → ’b)) → ’a → ’b

let memoize f n =

let table = ref [] in

let rec f’ n =

try List.assoc n !table

with Not_found →
let r = f f’ n in

table := (n, r) :: !table;

r

in f’ n

let open_fib fib = function

0 → 0
| 1 → 1
| n → fib (n – 1) + fib (n – 2)

let fib = memoize open_fib

34/ 41

Background: memoization

Recursive functions can be inefficient — use memoization

let open_fib fib = function

0 → 0
| 1 → 1
| n → fib (n – 1) + fib (n – 2)

let fib = memoize open_fib

fib 4

fib 3

fib 2

fib 0fib 1

35/ 41

Memoizing generic functions

A lookup table for heterogeneous code values

type _ t =

Nil : ’a t

| Cons : {T.TYPEABLE} * (T.t → ’a) code * ’a t → ’a t

val new_map : unit → ’a t ref

val add :

{T:TYPEABLE} → (T.t → ’a) code → ’a t ref → unit

val lookup :

{T:TYPEABLE} → ’a t → (T.t → ’a) code option

36/ 41

A staged generic fixpoint operator

let gfixQ (f : ’v genericQ → ’v genericQ) =
let tbl = empty () in

let rec result {D: DATA} x =

match lookup !tbl with

| Some g →.< .~g .~x >.
| None → let g = letrec

(fun self →
add tbl self;

.< fun y → .~(f result ..) >.)
in .< .~g .~x >.

in result

37/ 41

Staged gshow

gshow, staged

let gshow = gfixQ_ (fun self {D:DATA} v →
.< "("^ .~(constructor_ v) ^ concat " " .~(gmapQ_ self v) ^")" >.)

38/ 41

Generated code for gshow

let show_list = ref (fun _ → assert false) in
let show_int = ref (fun _ → assert false) in
let _ = show_int :=

fun i →
“(“^ string_of_int i ^ String.concat ” ” [] ^”)” in

let _ = show_list :=

(fun t →
“(“^(( match t with [] → “[]”

| _ :: __ → “::”) ^
(( concat ” ”

(match t with

| [] → []
| h :: t → [! show_int h;

!show_list t])) ^”)”))) in

!show_list

39/ 41

Staging generic programming: summary

Bad news: the generated code is pretty poor

Better news: the performance is fairly good!

typically 10× the speed of generic code;
typically 0.5-1× the speed of handwritten code

Best news: the staging can be improved

with better let / let rec insertion
with partially-static data
with match insertion
with match elimination
. . . and many other such techniques

until it is as fast as handwritten code (& sometimes faster!)

40/ 41

Next time: super-advanced functional programming

data Vec (A : Set) : N → Set

41/ 41