(* Examples of the staged code and its translation This file contains the complete code for all the examples in the paper Closing the Stage: From staged code to typed closures. Yukiyoshi Kameyama, Oleg Kiselyov, and Chung-chieh Shan This file also includes extra examples. The source language is MetaOCaml. The target language is supposed to be System F. We try to emulate it in plain OCaml, using first-class (record) polymorphism where needed. $Id$ *) (* ---------------------------------------------------------------------- *) (* The power example, Sec 2 *) let square x = x * x let rec power : int -> ('a,int) code -> ('a,int) code = fun n -> fun x -> if n = 0 then .<1>. else if n mod 2 = 0 then .< (*csp*)square .~(power (n/2) x)>. else .<.~x * .~(power (n-1) x)>. ;; let power7 : int -> int = .! . .~(Printf.printf "power\n"; power 7 ..)>.;; (* "power" printed once *) let res = (power7 2, power7 3);; (* nothing is printed... val res : int * int = (128, 2187) *) (* Naive non-solution, Sec 2.1 *) let rec npower n x = if n = 0 then (fun () -> 1) else if n mod 2 = 0 then (fun () -> square ((npower (n/2) x) ())) else (fun () -> x () * ((npower (n-1) x) ())) let npower7 = (* int -> int *) (fun () -> fun x -> (Printf.printf "power\n"; npower 7 (fun () -> x)) ()) ();; (* Nothing is printed when npower7 is computed *) let res = (npower7 2, npower7 3);; (* power power val res : int * int = (128, 2187) *) (* Environment-passing translation, Sec 2.2 *) (* We use the lists of polymorphic unions as extensible polymorphic records to model env *) let rec tpower : int -> ('pi->int) -> ('pi->int) = fun n -> fun x -> if n = 0 then (fun env -> 1) else if n mod 2 = 0 then let v = tpower (n/2) x in fun env -> square (v env) else let v1 = x in let v2 = tpower (n-1) x in fun env -> v1 env * v2 env ;; let rec lkupX env = match env with (`X x::_) -> x | (_::rest) -> lkupX rest;; let tpower7 : int -> int = let v = Printf.printf "power\n"; tpower 7 (fun env -> lkupX env) in (fun env -> fun x -> v (`X x::env)) [];; (* "power" printed once *) let res = (tpower7 2, tpower7 3);; (* nothing is printed... val res : int * int = (128, 2187) *) (* ---------------------------------------------------------------------- *) (* The ef example. *) (* The source code *) let ef = fun z -> . .~z + x>.;; let ef1 = . .~(ef ..)>.;; (* val ef1 : ('a, int -> int -> int) code = . fun x_2 -> (y_1 + x_2)>. *) let ef1run = (.! ef1) 2 3;; (* 5 *) let ef2 = . fun y -> .~(ef ..)>.;; (* val ef2 : ('a, int -> int -> int -> int) code = . fun y_2 -> fun x_3 -> ((x_1 * y_2) + x_3)>. *) let ef2run = (.! ef2) 2 3 4;; (* 10 *) (* The translation *) let tef = fun (z:'pi->int) -> fun (r:'pi) -> fun x -> let coerce (r,x) = r in z (coerce (r,x)) + x ;; let tef1 = let es1 = tef (fun y -> y) in (* instantiating 'pi to int *) fun () -> fun y -> es1 y;; let tef1run = tef1 () 2 3;; (* 5 *) let tef2 = let es2 = tef (fun (x,y) -> x*y) in (* instantiating 'pi to int*int *) fun () -> fun x -> fun y -> es2 (x,y);; let tef2run = tef2 () 2 3 4;; (* 10 *) (* ---------------------------------------------------------------------- *) (* The eta example. *) let etatest = let eta f = . .~(f ..)>. in (.! .< fun y -> .~(eta (fun z -> .< .~z + y >.)) >.) 2 3, (.! .< fun y -> fun w -> .~(eta (fun z -> .< .~z + y*w >.)) >.) 2 3 4, (.! .< fun x u -> .~(eta (fun z -> . .~z + u*x*y >.)) >.) 2 3 4 5 ;; (* 5,10,34 *) (* To translate the third example, we keep the result of eta polymorphic. It could be either int> or int->int>. The paper considers only the first case. *) type ('w,'pi) funf = {f : 'pi1. (('pi* 'pi1)->int) -> (('pi * 'pi1)->'w)};; let teta f = let es = f.f (fun (r,x)->x) in (* instantiating pi1 to int *) fun (r:'pi) -> fun x -> es (r,x) ;; let teta1 = let f1 = {f = fun z -> fun (y,r1) -> z (y,r1) + y} in let es1 = teta f1 in fun () -> fun y -> es1 y in teta1 () 2 3;; (* 5 *) let teta2 = let f2' = fun z -> fun (y,w,r1) -> z ((y,w),r1) + y*w in let f2 = {f = fun z -> fun ((y,w),r1) -> f2' z (y,w,r1)} in (* coercion *) let es2 = teta f2 in fun () -> fun y -> fun w -> es2 (y,w) in teta2 () 2 3 4;; (* 10 *) let teta3 = let f3' = fun z -> fun (x,u,r1) -> fun y -> z ((x,u),r1) + u*x*y in let f3 : (int->int,int*int) funf = {f = fun z -> fun ((x,u),r1) -> f3' z (x,u,r1)} in (* coercion*) let es3 = teta f3 in fun () -> fun x -> fun u -> es3 (x,u) in teta3 () 2 3 4 5;; (* 34 *) (* ---------------------------------------------------------------------- *) (* A few more interesting, complex examples *) let ex5 = let sub x y = Printf.printf "sub\n"; .<.~x - .~y>. in . fun y -> .~(sub .. (sub .<1>. ..))>.;; (* sub sub val ex5 : ('a, int -> int -> int) code = . fun y_2 -> (x_1 - (1 - y_2))>. *) let ex5r = (.! ex5) 3 2;; (* 4 *) (* Translation *) (* sub had a type -> -> whose translation, according to the rules of Sec 5, is forall pi. (pi -> int) -> (forall pi1. ((pi,pi1) -> int) -> ((pi,pi1) -> int)) *) let tex5 = let sub : ('pi->int) -> (('pi*'pi1)->int) -> (('pi*'pi1)->int) = fun x -> fun y -> Printf.printf "sub\n"; fun (r,r1) -> x r - y (r,r1) in let es = (* the typing env contains the bindings x and y. The function sub has an (alpha)-closed type and so it doesn't count We need to coerce from the above type for sub to the env (int*int). We instantiate both pi and pi1 to (int*int), and have to do some packing/unpacking *) let coercef f = fun (x:(int*int)->int) -> fun (y:(int*int)->int) -> f x (fun (r,r1) -> y r1) and coercer v r = v (r,r) in (coercer ((coercef sub) (fun (x,y) -> x) (coercer ((coercef sub) (fun (x,y) -> 1) (fun (x,y) -> y))))) in fun () -> fun x -> fun y -> es (x,y) ;; (* sub sub val tex5 : unit -> int -> int -> int = *) let tex5r = tex5 () 3 2;; (* 4 *) let ex51 = let rapp x f = Printf.printf "rapp\n"; .<.~f .~x>. in . .~(rapp .. . .~(rapp .. . z*y>.)>.)>.;; (* rapp rapp val ex51 : ('a, int -> int) code = . ((fun y_2 -> ((fun z_3 -> (z_3 * y_2)) (x_1 + y_2))) (x_1 + 1))>. *) let ex51r = (.! ex51) 2;; (* 15 *) let ex6 = .. in print_string "here"; .<.~x + .~x>.)>.;; (* hereval ex6 : ('a, int) code = .. *) let ex70 = . let () = print_string "here" in ..) ..)>.;; (* hereval ex70 : ('a, int) code = .. *) (* ---------------------------------------------------------------------- *) (* Cross-stage presistence *) (* This example includes persistence of a code value, which we specifically exclude in the paper. *) let cspe = . .~(let u = .. in (.! . .<.~u>.>.) ()) >.;; (* val cspe : ('a, 'b -> 'b) code = . x_1>. *) (* This CSP example does fit our restriction *) let rec scspe x = .<(fun y -> x) (scspe 1)>.;; (* val scspe : int -> ('a, int) code = # scspe 10;; - : ('a, int) code = .<((fun y_1 -> 10) (((* cross-stage persistent value (as id: scspe) *)) 1))>. # .! (scspe 10);; - : int = 10 *) let rec tcspe x = fun () -> (fun y -> x) (tcspe 1);; (* val tcspe : int -> unit -> int = # (tcspe 10) ();; - : int = 10 *) (* or, more involved example *) (* but it fails... let rec f x = .<(fun y -> x) (f (.! (f 3)))>.;; *) (* ---------------------------------------------------------------------- *) (* The example with recursion. * This example suggests that we need polymorphic recursion in order to * translate staging into System F. * * [ccshan 2007-10-10] *) let rec funnysum : int -> ('a,int) code -> ('a,int) code = fun n -> fun x -> match n with | 0 -> x | _ -> ..)>. ;; let funnysum5 = . .~(funnysum 5 ..)>.;; (* . let y_2 = 42 in let y_3 = 42 in let y_4 = 42 in let y_5 = 42 in let y_6 = 42 in (y_6 + (y_5 + (y_4 + (y_3 + (y_2 + x_1)))))>. *) let funnysum5r = (.! funnysum5) 1000;; (* val funnysum5r : int = 1210 *) (* Translation. We use records with first-class polymorphism to model first-class polymorphic functions, and hence, polymorphic recursion. *) type cct = {ccf : 'pi. ('pi->int) -> ('pi->int) };; let rec tfunnysum : int -> cct = fun n -> {ccf = fun x -> match n with | 0 -> x | _ -> let es = (tfunnysum (n-1)).ccf (* instantiate to ('pi,int) *) (fun (r,y) -> y + x r) in fun r -> let y = 42 in es (r,y)} ;; let tfunnysum5 = let es = (tfunnysum 5).ccf (* instantiate to int *) (fun x -> x) in fun () -> fun x -> es x;; let tfunnysum5r = tfunnysum5 () 1000;; (* val tfunnysum5r : int = 1210 *) (* The following is less idiomatic OCaml but it better matches the System F translation (with the form fix f x : tau) *) type fsumt = {fsumf : 'pi. (int*('pi->int)) -> ('pi->int) };; let rec ttfunnysum : fsumt = {fsumf = fun (n,x) -> match n with | 0 -> x | _ -> let es = ttfunnysum.fsumf (* instantiate to ('pi,int) *) (n-1,(fun (r,y) -> y + x r)) in fun r -> let y = 42 in es (r,y)} ;; let ttfunnysum5 = let es = ttfunnysum.fsumf (* instantiate to int *) (5,(fun x -> x)) in fun () -> fun x -> es x;; let ttfunnysum5r = ttfunnysum5 () 1000;; (* val ttfunnysum5r : int = 1210 *) (* ---------------------------------------------------------------------- *) (* Scope extrusion via mutable state *) let extr = let x = ref .<1>. in let _ = . .~(x := ..; .<()>.)>. in !x;; (* val extr : ('a, int) code = .. # .! extr ;; Unbound value v_1 Exception: Trx.TypeCheckingError. *) (* an attempted translation of this example *) (* It does not typecheck! let textr = let x = ref (fun () -> 1) in let es = x := (fun v -> v); fun v -> () in let _ = fun () -> fun v -> es v in !x;; *)