(* General recursive types via delimited continuations 
   See ../Computation/Continuations.html#delimcc-rectype
   for explanations.
 $Id: delimcc-rectype.ml,v 1.1 2007/12/08 01:13:27 oleg Exp oleg $
*)

(* The following is a term `representation' of a general recursive type
   mu X. (X->int->int)
 Note that in the body of mu, X occurs in the negative (contra-variant)
 position. That makes it a general recursive type.
*)
module type RecType = sig
 type t     (* an abstract type *)
 val wrap   : (t->int->int) -> t
 val unwrap : t -> (t->int->int)
end;;
(* provided that (unwrap . wrap) is the identity *)


(* A sample term using the emulated recursive type *)
module XX(T:RecType) = struct
  let u (x:T.t) : int->int = T.unwrap x x
  let fact (x:T.t) n = if n <= 1 then 1 else n * u x (n-1)
  let x = T.wrap fact
  let result = u x 5
end;;

(* There is certainly one implementation of the RecType signature, using
   iso-recursive types
*)
module R1 : RecType = struct
  type t = T of (t -> int -> int)
  let wrap x = T x
  let unwrap (T x) = x
end;;

let module Foo = XX(R1) in Foo.result;;
(* - : int = 120 *)

(* The question becomes if there is another implementation of the
   signature RecType, which does not use any recursive types. 
   It seems there is:
*)

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))))))


module R2 : RecType = struct
  type t = unit->unit
  let p = new_prompt ()
  let omega () = failwith "omega" (* or any other divergent term *)
  let wrap t () = shift p (fun sk -> t); omega ()
  let unwrap t = push_prompt p (fun () -> t (); omega ())
end;;

let module Bar = XX(R2) in Bar.result;;
(* - : int = 120 *)