(* Meta-programming with delimited continuations *) (* let-insertion via shift *) (* The Gibonacci example *) (* $Id: fib.ml,v 1.1 2006/02/01 00:54:57 oleg Exp $ *) (* The following code relies on the delimcc library: http://okmij.org/ftp/continuations/implementations.html#caml-shift Please make sure dlldelimcc.so is in your LD_LIBRARY_PATH or in ld.conf-described paths. *) open Delimcc open Printf ;; (* The original Gibonacci *) let rec gib x y n = if n = 0 then x else if n = 1 then y else gib x y (n-1) + gib x y (n-2) ;; (* gib 1 1 5;; gives 8 *) (* Naively staged Gibonacci *) let rec gibgen x y n = if n = 0 then x else if n = 1 then y else .<.~(gibgen x y (n-1)) + .~(gibgen x y (n-2))>. ;; (* val gibgen : ('a, int) code -> ('a, int) code -> int -> ('a, int) code = *) let test_gibgen n = . .~(gibgen .. .. n)>.;; (* val test_gibgen : int -> ('a, int -> int -> int) code = *) let test_gibgen5 = test_gibgen 5;; (* val test_gibgen5 : ('a, int -> int -> int) code = . fun y_2 -> ((((y_2 + x_1) + y_2) + (y_2 + x_1)) + ((y_2 + x_1) + y_2))>. *) (* Gibonacci with open recursion *) let gib x y self n = if n = 0 then x else if n = 1 then y else self (n-1) + self (n-2) ;; (* the simple y combinator *) let rec y_simple f n = f (y_simple f) n ;; let test_s1 = y_simple (gib 1 1) 5;; (* 8 *) (* Now add memoization *) let rec lookup k = function [] -> None | ((k',v')::t) -> if k = k' then Some v' else lookup k t let ext s n v = (n,v) :: s let empty () = [] ;; (* as a warm-up, use assignments here. We don't use this combinator after the following example. But it is useful for comparison. *) let y_memo_m f n = let tableref = ref (empty ()) in let rec memo n = match (lookup n !tableref) with | None -> let v = f memo n in (tableref := ext !tableref n v; v) | Some v -> v in f memo n ;; let test_ma1 = y_memo_m (gib 1 1) 8;; let test_ma2 = y_memo_m (gib 1 1) 30;; (* 1346269, without memoization it would've taken a while...*) (* The same, but using delim continuations *) type ('k,'v,'r) memo_req = | Val of 'r | Lookup of 'k * ('v option->('k,'v,'r) memo_req) | Ext of ('k * 'v) * ('v -> ('k,'v,'r) memo_req) ;; let top thunk = let p = new_prompt () in let rec loop table = function | Val v -> v | Lookup (n,k) -> loop table (k (lookup n table)) | Ext ((n,v),k) -> loop (ext table n v) (k v) in loop (empty ()) (push_prompt p (fun () -> Val (thunk p))) ;; (* Memoizing combinator *) let y_memo p f n = let lookup n = shift p (fun f -> Lookup (n,f)) in let ext n v = shift p (fun f -> Ext ((n,v),f)) in let rec memo n = match (lookup n) with | None -> let v = f memo n in ext n v | Some v -> v in f memo n ;; let test_md1 = top(fun p -> y_memo p (gib 1 1) 8);; (* 34 *) let test_md2 = top(fun p -> y_memo p (gib 1 1) 10);; (* 89 *) (* Staging ... *) (* Note the dynamic arguments, x and y, are at the front, so that self has to deal with the static argument only. Somehow, we have to specify what is dynamic/static. Shifting argument may be considered as a primitive BTA. Far more sophisticated BTA can be designed (using abstract interpretation, for example). But not here. We want a simple example. *) let sgib x y self n = if n = 0 then x else if n = 1 then y else .<.~(self (n-1)) + .~(self (n-2))>. ;; let test_ss n = . .~(y_simple (sgib .. ..) n)>.;; (* exponential explosion is evident *) let test_ss1 = test_ss 5;; let test_ss1r = (.! test_ss1) 1 1;; (* 8 *) (* But the explosion also occurs if we use the memoizing combinator! *) let test_ssm n = . .~(y_memo_m (sgib .. ..) n)>.;; let test_ssm1 = test_ssm 5;; (* val test_ssm1 : ('a, int -> int -> int) code = . fun y_2 -> ((((y_2 + x_1) + y_2) + (y_2 + x_1)) + ((y_2 + x_1) + y_2))>. *) (* exponential explosion is evident; (y_2 + x_1) is repeated thrice *) (* Staging and memoization -- of the code! *) let stop thunk = let p = new_prompt () in let rec loop table = function | Val v -> v | Lookup (n,k) -> loop table (k (lookup n table)) | Ext ((n,v),k) -> ..) (k ..))>. in loop (empty ()) (push_prompt p (fun () -> Val (thunk p))) ;; (* Note: we are using the same y_memo, as in the unstaged case *) let test_smd n = . .~(stop(fun p -> y_memo p (sgib .. ..)n))>.;; let test_smd1 = test_smd 5;; let test_ss1r = (.! test_ss1) 1 1;; (* 8 *) (* Danger of mixing mutation and staging *) let extrusion = let r = ref .<1>. in . .~(r := ..; .<()>.)>.; !r;; (* val extrusion : ('a, int) code = .. The result is a code with an unbound variable y_1! If we try to run the expression, we get # .! extrusion;; Unbound value y_1 Exception: Trx.TypeCheckingError. We get a type checking error at run-time. *) (* We now re-implement top and y_memo without the data types, to bring the implementation closer to our formal calculus *) (* Functional memo table *) let empty_fn = fun key onfound onmissing -> onmissing key let ext_fn table n v = fun key onfound onmissing -> if key = n then onfound v else table key onfound onmissing ;; let top_fn thunk = let p = new_prompt () in (push_prompt p (fun () -> let v = thunk p in fun table -> v)) empty_fn ;; (* Memoizing combinator *) let y_memo_fn p f n = let lookup n = shift p (fun k -> fun table -> k (table n) table) in let ext n v = shift p (fun k -> fun table -> let table' = ext_fn table n v in k v table') in let rec memo n = (lookup n) (* found *) (fun v -> v) (* not found *) (fun n -> let v = f memo n in ext n v) in f memo n ;; let test_fn_md1 = top_fn(fun p -> y_memo_fn p (gib 1 1) 8);; (* 34 *) let test_fn_md2 = top_fn(fun p -> y_memo_fn p (gib 1 1) 20);; (* 10946 *) (* Staged memoizing combinator *) let y_memo_sfn p f n = let lookup n = shift p (fun k -> fun table -> k (table n) table) in let ext n v = shift p (fun k -> fun table -> .. in k .. table')>.) in let rec memo n = (lookup n) (* found *) (fun v -> v) (* not found *) (fun n -> let v = f memo n in ext n v) in f memo n ;; let test_fn_smd n = . .~(top_fn(fun p -> y_memo_sfn p (sgib .. ..)n))>.;; let test_fn_smd1 = test_fn_smd 8;; (* val test_fn_smd1 : ('a, int -> int -> int) code = . fun y_2 -> let t_3 = y_2 in let t_4 = x_1 in let t_5 = (t_3 + t_4) in let t_6 = (t_5 + t_3) in let t_7 = (t_6 + t_5) in let t_8 = (t_7 + t_6) in let t_9 = (t_8 + t_7) in let t_10 = (t_9 + t_8) in (t_10 + t_9)>. *) let test__fn_ss1r = (.! test_fn_smd1) 1 1;; (* 34 *) (* Alas, the functional memo table in the above code requires recursive types if our function types are annotated with the answer-types of control effects. For consistency with the code in circle-shift.elf, we re-write the staged fixpoint combinator as follows. *) (* For the sake of the closest correspondence with circle-shift.elf, we use pairs to emulate 'a option data type. In the rest of the code, we may consider 'a option as an abstract data type. *) module Maybe : sig type 'a maybe val nothing : 'a maybe val just : 'a -> 'a maybe val ifnothing : 'a maybe -> bool val fromjust : 'a maybe -> 'a end = struct type 'a maybe = bool * (unit -> 'a) let nothing = (true, fun () -> failwith "nothing") let just x = (false, fun () -> x) let ifnothing = fst let fromjust x = snd x () end;; open Maybe;; (* Memo table with Maybe *) type 'a memo_sig = int -> 'a maybe;; let empty_fn = fun key -> nothing let ext_fn table n v = fun key -> if key = n then just v else table key ;; let top_fn thunk = let p = new_prompt () in (push_prompt p (fun () -> let v = thunk p in fun table -> v)) empty_fn ;; (* Memoizing combinator *) let y_memo_fn p f = let lookup n = shift p (fun k -> fun table -> k (table n) table) in let ext n v = shift p (fun k -> fun table -> let table' = ext_fn table n v in k v table') in let rec memo n = let r = lookup n in (* do the lookup first *) if ifnothing r then let v = f memo n in ext n v else (* value found *) fromjust r in f memo ;; let test_fn_md1 = top_fn(fun p -> y_memo_fn p (gib 1 1) 8);; (* 34 *) let test_fn_md2 = top_fn(fun p -> y_memo_fn p (gib 1 1) 20);; (* 10946 *) (* Staged memoizing combinator *) let y_ms p f = let lookup n = shift p (fun k -> fun table -> k (table n) table) in let ext n v = shift p (fun k -> fun table -> .. in k .. table')>.) in let rec memo n = let r = lookup n in (* do the lookup first *) if ifnothing r then let v = f memo n in ext n v else (* value found *) fromjust r in f memo ;; let test_fn_smd n = . .~(top_fn(fun p -> y_ms p (sgib .. ..)n))>.;; let test_fn_smd1 = test_fn_smd 8;; (* val test_fn_smd1 : ('a, int -> int -> int) code = . fun y_2 -> let t_3 = y_2 in let t_4 = x_1 in let t_5 = (t_3 + t_4) in let t_6 = (t_5 + t_3) in let t_7 = (t_6 + t_5) in let t_8 = (t_7 + t_6) in let t_9 = (t_8 + t_7) in let t_10 = (t_9 + t_8) in (t_10 + t_9)>. *) let test__fn_ss1r = (.! test_fn_smd1) 1 1;; (* 34 *) (* Safety justification *) (* In MetaOCaml, we have to do this justification manually. We have to prove that the body of a future-stage lambda contains an escape, the escape code has no control effects. In short, no present-stage control effect could cross the future-stage binder. In circle-shift.elf, this restriction on the use of delimited control is built into the calculus. *) (* There are three future-stage binders in the above code: binders for x and y in test_fn_smd and the let-binder for t in ext n f, which is part of y_ms. Regarding the first two binders, for x and y. The body of the function fun x y -> ... in test_fn_smd does have an escape, which runs in the context of top_fn, which inserts push_prompt p. There is only one prompt used in the whole code. Therefore, one push_prompt p stops all control effects. The application of the 'table' to the result of the prompt expression is also pure (it may involve the invocation of the captured continuation k, see lookup and ext. The delimited continuation captured by shift is always a pure function however). The escape code in test_fn_smd is pure. The body of the let-expression in ext n v contains the invocation of ext_fn and of k. The examination of ext_fn shows it has no control effects. The function k is the continuation captured by shift, which adds reset around the invocation. Thus the expression k .. table' has no control effects. We thus have satisfied the safety requirements of using delimited continuations in code generators. *) (* And here what happens if the safety condition is not met. The following is a slight variation on test_fn_smd above. Suppose we wish to compute sgib not for .. and .. but for .. and .. To guard against possible duplication of the expression y+1, we bind it to a new variable z. In the following code, we cannot prove that the escape in the body of let-binding is pure. In fact, it is certainly not, as y_ms has an effect. *) let test_fn_smd_bad = . .~(top_fn(fun p -> .. ..) 2)>.))>.;; (* And the result is disastrous: we can see that variable z_4 is being used *before* it is bound.*) (* val test_fn_smd_bad : ('a, int -> int -> int) code = . fun y_3 -> let t_5 = x_2 in let t_6 = z_4 in let z_4 = (y_3 + 1) in (t_6 + t_5)>. *) (* Attempting to run this expression gives # .! test_fn_smd_bad;; Unbound value z_4 Exception: Trx.TypeCheckingError. *) (* Purity and answer-type polymorphism (Sec 4.1 of the paper) The issue arises regardless of delimited control or monadic/CPS style. Here we demonstrate the issue for a simple state-passing memoizing fixpoint combinator. *) (* Here is the state-passing version of y_memo_m: *) (* val y_memo_m_statepass : ((('a * 'b) list -> 'a -> ('a * 'b) list * 'b) -> ('a * 'b) list -> 'a -> ('a * 'b) list * 'b) -> ('a * 'b) list -> 'a -> ('a * 'b) list * 'b = *) let rec y_memo_m_statepass f = f (fun s x -> match (lookup x s) with Some r -> (s,r) | None -> let (s1, r1) = (y_memo_m_statepass f s x) in (ext s1 x r1, r1)) ;; (* And an example of its use *) let gib_statepass x y self s n = if n = 0 then (s,x) else if n = 1 then (s,y) else let (s1,r1) = self s (n-1) in let (s2,r2) = self s1 (n-2) in (s2,r1+r2) ;; let 1346269 = snd (y_memo_m_statepass (gib_statepass 1 1) (empty ()) 30);; (* 1346269, without memoization it would've taken a while...*) (* We now try to write it without using the option data type, using the representation of 'a option as (bool * unit -> 'a) *) (* val y_memo_m_statepass1 : ((('a -> bool * (unit -> 'b)) -> 'a -> ('a -> bool * (unit -> 'b)) * 'b) -> ('a -> bool * (unit -> 'b)) -> 'a -> ('a -> bool * (unit -> 'b)) * 'b) -> ('a -> bool * (unit -> 'b)) -> 'a -> ('a -> bool * (unit -> 'b)) * 'b = That is, the memo table has the type ('a -> bool * (unit -> 'b)) *) let y_memo_m_statepass1 f = let empty n = (false, fun () -> failwith "empty") in let lookup k s = s k in let ext s n v = fun k -> if k = n then (true, fun () -> v) else s k in let ifjust x = fst x in let fromjust x = snd x () in let rec loop f = f (fun s x -> let lr = lookup x s in if ifjust lr then let r = fromjust lr in (s,r) else let (s1, r1) = (loop f s x) in (ext s1 x r1, r1)) in loop f ;; (* Suppose we write the projection function in the state-passing style as well. So, the memo-table has the type That is, the memo table has the type ('a -> bool * (unit -> 's -> ('s,'b))) Alas, it does not type: 's in the type above gets unified with the state of the whole computation, which contains the memo table itself. So, we get the failure of the occurrence check (alas, OCaml doesn't report these errors clearly. It is hard to see the failure of the occurrence check; as an example, try (fun x -> x x) and see what the error message says. let y_memo_m_statepass2 f = let empty n = (false, fun () s -> failwith "empty") in let lookup k s = s k in let ext s n v = fun k -> if k = n then (true, fun () s -> (s,v)) else s k in let ifjust x = fst x in let fromjust x = snd x () in let rec loop f = f (fun s x -> let lr = lookup x s in if ifjust lr then let (s',r) = fromjust lr s in (s',r) else let (s1, r1) = (loop f s x) in (ext s1 x r1, r1)) in loop f ;; *) (* We need to add reset, to indicate that fromjust is really pure *) let y_memo_m_statepass3 f = let empty n = (false, fun () s -> failwith "empty") in let reset m = fun s -> (s,snd (m empty)) in let lookup k s = s k in let ext s n v = fun k -> if k = n then (true, fun () s -> (s,v)) else s k in let ifjust x = fst x in let fromjust x = snd x () in let rec loop f = f (fun s x -> let lr = lookup x s in if ifjust lr then let (s',r) = reset (fromjust lr) s in (s',r) else let (s1, r1) = (loop f s x) in (ext s1 x r1, r1)) in loop f ;; let 1346269 = let empty n = (false, fun () s -> failwith "empty") in snd (y_memo_m_statepass3 (gib_statepass 1 1) empty 30);;