(* General recursive types via exceptions
   (which are restricted form of delimited continuations)
 $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 120 = let module Foo = XX(R1) in Foo.result;;

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

module R2 : RecType = struct
  type t = unit->unit
  exception E of (t -> int -> int)
  let wrap t () = raise (E t)
  let unwrap t  = try t (); raise (E (fun _ x -> x)) with E x -> x
end;;

let 120 = let module Bar = XX(R2) in Bar.result;;