(* Emulation of the calculus lambda-sr-let Polymorphic delimited continuations Asai and Kameyama, APLAS 2007 http://logic.cs.tsukuba.ac.jp/~kam/paper/aplas07.pdf hereafter, AK07 Unlike the Haskell code described in http://www.haskell.org/pipermail/haskell/2007-December/020034.html the present code is an emulation of the lambda-sr-let rather than direct implementation. We show that shift/reset with multiple prompts can indeed emulate answer-type modifying shift/reset of lambda-sr-let. The multi-prompt shift/reset of OCaml (cupto) is already sufficiently polymorphic. Although the answer-type of cupto-derived shift/reset is fixed, the availability of several prompts and _overlapping_ control regions make up for that. Effectively, answer-type modification becomes possible. This emulation of the AK07 calculus is yet another proof that AK07 admit type inference algorithm. In all the tests below, all the types are inferred. *) (* Preliminaries *) (* Open the DelimCC library http://pobox.com/~oleg/ftp/Computation/Continuations.html#caml-shift Make sure OCaml top level is invoked as $ LD_LIBRARY_PATH=. ocamltopcc and the current directory contains the delimcc DLL (shared object). Or byte-compile the code. *) open Delimcc;; let shift p f = take_subcont p (fun sk () -> push_prompt p (fun () -> (f (fun c -> push_prompt p (fun () -> push_subcont sk (fun () -> c)))))) ;; (* val shift : 'a Delimcc.prompt -> (('b -> 'a) -> 'a) -> 'b = *) let abort p v = take_subcont p (fun sk () -> v);; (* val abort : 'a Delimcc.prompt -> 'a -> 'b = *) (* emulation of the answer-type-modifying shift Unlike the fixed-answer-type shift/reset, which have one prompt (corresponding to the fixed answer-type), shift2/reset2 have two prompts, for the two answer types (before and after the modification). *) let reset2 f = let p1 = new_prompt () in let p2 = new_prompt () in push_prompt p1 (fun () -> abort p2 (f (p1,p2)));; (* val reset2 : ('a Delimcc.prompt * 'b Delimcc.prompt -> 'b) -> 'a = *) let shift2 (p1,p2) f = shift p1 (fun k -> fun x -> push_prompt p2 (fun () -> f k x; failwith "omega"));; (* val shift2 : ('a -> 'b) Delimcc.prompt * 'b Delimcc.prompt -> (('c -> 'a -> 'b) -> 'a -> 'd) -> 'c = *) (* Example from Sec 2.1 of AK07 *) let rec append lst prompts = match lst with | [] -> shift2 prompts (fun k l -> k l) | a::rest -> a :: append rest prompts;; (* val append : 'a list -> ('a list -> 'b) Delimcc.prompt * 'b Delimcc.prompt -> 'a list = The type clearly indicates the modification of the answer-type from 'b to 'a list -> 'b Note that 'b remains polymorphic. *) let append123 = reset2 (append [1;2;3]);; (* val append123 : int list -> int list = *) let test1 = append123 [4;5;6];; (* val test1 : int list = [1; 2; 3; 4; 5; 6] *) (* Type-safe, first-class sprint: Sec 2.3 of AK07 *) let int x = string_of_int x;; let str (x:string) = x;; let fmt to_str prompts = shift2 prompts (fun k x -> k (to_str x));; (* *) let lit str (p1,p2) = shift p1 (fun k -> push_prompt p2 (fun () -> k str));; (* *) let test10 = reset2 (lit "Hello");; (* val test10 : string = "Hello" *) (* Combining two answer-type-modifying computations, chaining the modification of the answer-type. *) (* The following is right-associative. The associativity doesn't seem to matter though *) let (^^) e1 e2 = fun (pa,pg) -> let pb = new_prompt () in let v1 = e1 (pa,pb) in let v2 = e2 (pb,pg) in v1 ^ v2;; (* val ( ^^ ) : ('a * 'b Delimcc.prompt -> string) -> ('b Delimcc.prompt * 'c -> string) -> 'a * 'c -> string = Note the return type: chaining of the answer-type modifications. *) let sprintf p = reset2 p;; (* val sprintf : ('a Delimcc.prompt * 'b Delimcc.prompt -> 'b) -> 'a = *) (* It is instructive to see some types: # lit "xx";; - : '_a Delimcc.prompt * '_a Delimcc.prompt -> string = # fmt int;; - : (int -> '_a) Delimcc.prompt * '_a Delimcc.prompt -> string = # fmt str;; - : (string -> '_a) Delimcc.prompt * '_a Delimcc.prompt -> string = # fmt int ^^ lit "xx";; - : (int -> '_a) Delimcc.prompt * '_a Delimcc.prompt -> string = # lit "xx" ^^ fmt int;; - : (int -> '_a) Delimcc.prompt * '_a Delimcc.prompt -> string = # fmt int ^^ fmt str;; - : (int -> string -> '_a) Delimcc.prompt * '_a Delimcc.prompt -> string = Please see the discussion in the AK07 paper about the answer-types modifications. *) (* Tests *) let test2 = sprintf (lit "Hello " ^^ lit "world");; (* val test2 : string = "Hello world" *) let test2 = sprintf (fmt str ^^ lit "world");; (* val test2 : string -> string = *) let test2r = test2 "Hello ";; (* val test2r : string = "Hello world" *) let test2 = sprintf (lit "Hello" ^^ fmt str);; (* val test2 : string -> string = *) let test2r = test2 " world";; (* val test2r : string = "Hello world" *) let test2 = sprintf (lit "Hello" ^^ fmt int);; (* val test2 : int -> string = *) let test22 = test2 2;; (* val test22 : string = "Hello2" *) let test3 = sprintf (lit "The value of " ^^ fmt str ^^ lit " is " ^^ fmt int);; (* val test3 : string -> int -> string = *) let test3r = test3 "x" 1;; (* val test3r : string = "The value of x is 1" *) (* The following is the same as test3, only split into several parts. The aim is to demonstrate that sprintf and the format specification are first-class functions. This is not the case with Haskell's Printf (which isn't even type safe) or OCaml's printf (where the format specification has a weird typing and is not first class). *) let test3' = (* format specification can be built incrementally *) let format_spec1 = lit "The value of " ^^ fmt str ^^ lit " is " in let format_spec = format_spec1 ^^ fmt int in let applyit f x = f x in (* sprintf and format_spec are ordinary functions, can be passed as args *) let formatter = applyit sprintf format_spec in formatter "x" 1 ;; (* val test3' : string = "The value of x is 1" *)