(* 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);;