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