(*                   All the different ways to get 
 *            the _fully polymorphic_ fixpoint in OCaml 
 *
 * This code has been inspired and influenced by Omega implementations
 *   http://www.lri.fr/~signoles/prog/misc/lambda.ml.html
 *   by Julien SIGNOLES.
 * 
 * This code fixes one bug in SIGNOLES' code, and develops
 * the fixpoint operator with full polymorphism. Our approach is 
 * based explicitly on self-application.
 * We also add more implementations: recursive modules, and the 
 * fixpoint inherent in objects.
 *
 * $Id: fixpoints.ml,v 1.3 2005/11/22 06:26:05 oleg Exp oleg $
 *)

(* The desired signature we are implementing (in quite a few ways) here
*)
module type FIX = sig
  val fix : (('a -> 'b) -> ('a -> 'b)) -> ('a -> 'b)
end

(* A simple test of FIX *)
module Fact(F : FIX) = struct
  let fact_nr self n = if n = 0 then 1 else n * (self (n-1))
  let fact n = F.fix fact_nr n
  let fact5 = fact 5
end

(*------------------------------------------------------------------------*)

(* The native implementation, via built-in let rec *)
module FixNative : FIX = struct
  let rec fix f n = f (fix f) n
end

let test = let module F = Fact(FixNative) in F.fact5
;;

(* The following is essentially the same, but cuter *)
module FixModule : FIX = struct
  module rec M : FIX = struct
    let fix f n = f (M.fix f) n
  end
  include M
end

let test = let module F = Fact(FixModule) in F.fact5
;;

(*------------------------------------------------------------------------*)

(* Implementing Fix via iso-recursive types 
 *
 * The standard formula for the applicative fixpoint combinator
 *    fix f === (fun g -> g g)(fun x n -> f (x x) n)
 * obviously does not type.
 * Indeed, the type of 'g' must be both t->a->b and t, i.e., must be
 * recursive. We can emulate this (equi-) recursive type with an 
 * iso-recursive one.
*)

(* Iso-recursive algebraic data type. 
 * Following SIGNOLES, we rely on an iso-recursive datatype ('a,'b) t
 * with the injection function Wrap :   (('a,'b) t -> ('a->'b)) -> ('a,'b) t
 * and  the projection function unwrap: ('a,'b) t -> (('a,'b) t -> ('a->'b))
 *)
module FixData : FIX = struct
  type ('a,'b) t = Wrap of (('a,'b) t -> ('a->'b))
  let unwrap (Wrap x) = x
  let fix f = ((fun g -> g (Wrap g)) (fun x n -> f (unwrap x x) n))
end

let test = let module F = Fact(FixData) in F.fact5
;;


(* A different take. Instead of wrapping/unwrapping, we attempt to
 * define a function auto'apply such that 
 *  auto'apply g applies g to itself, in some way that makes the
 * typechecker happy.
 * The following implementation uses the recursive datatype, the same
 * as above.
 *)
module FixData2 : FIX = struct
  type ('a,'b) t = Wrap of (('a,'b) t -> ('a->'b))
  let auto'apply ((Wrap x) as g) = x g
  let fix f = auto'apply (Wrap (fun x n -> f (auto'apply x) n))
end

let test = let module F = Fact(FixData2) in F.fact5
;;


(* essentially the same as above *)
module FixRecord : FIX = struct
  type ('a,'b) t = { unwrap : ('a,'b) t -> ('a->'b) }
  let auto'apply g = g.unwrap g
  let fix f = auto'apply {unwrap = (fun x n -> f (auto'apply x) n)}
end

let test = let module F = Fact(FixRecord) in F.fact5
;;

(* Also essentially the same as above: an object is a kind of record.
   See however below for FixObjectS: objects have an implicit
   fixpoint already.
*)
module FixObjectR : FIX = struct
  class ['a,'b] t y = 
    object method unwrap (x: ('a,'b) t) (n:'a) : 'b = y x n end
  let auto'apply g = g#unwrap g
  let fix f = auto'apply (new t (fun x n -> f (auto'apply x) n))
end

let test = let module F = Fact(FixObjectR) in F.fact5
;;

(* essentially the same as above. Polymorphic variants don't
   need an explicit type declaration.
   They still can have (iso-) recursive type 
*)
module FixPVar : FIX = struct
  let auto'apply ((`Unwrap f) as g) = f g
  let fix f = auto'apply (`Unwrap (fun x n -> f (auto'apply x) n))
end

let test = let module F = Fact(FixPVar) in F.fact5
;;

(* Here the value to auto'apply is implicit -- passed via an environment
   (continuation) rather than given as an explicit argument to auto'apply.
   Delimited continuations do have recursive types.
   See FixReference for the canonical form of using references for
   implementing fixpoints.
 *)
module FixReferenceA : FIX = struct
  let fix f = 
    let wrap = ref (fun _ -> failwith "undefined") in
    let auto'apply () = !wrap in
    auto'apply (wrap := (fun n -> f (auto'apply ()) n))
end

let test = let module F = Fact(FixReferenceA) in F.fact5
;;

(*------------------------------------------------------------------------*)
(* Equi-recursive types *)

module FixMagic: FIX = struct
  let auto'apply g = Obj.magic g g
  let fix f = auto'apply (fun x n -> f (auto'apply x) n)
end

let test = let module F = Fact(FixMagic) in F.fact5
;;

(* True equi-recursive types. Need -rectypes flag to the Ocaml *)
(*
module FixERec: FIX = struct
  let auto'apply g = g g
  let fix f = auto'apply (fun x n -> f (auto'apply x) n)
end

let test = let module F = Fact(FixERec) in F.fact5
;;
*)


(*------------------------------------------------------------------------*)

(* Mutation: mutation is implicitly a delimited continuation, which
   has a recursive type
*)

module FixReference : FIX = struct
  let fix f n = 
    let cell = ref (fun _ -> failwith "undefined") in
    begin cell := f (fun n -> !cell n); !cell n end
end

let test = let module F = Fact(FixReference) in F.fact5
;;

(* Exceptions are also continuations with recursive types.
   We needed to declare the record rfe below to get the polymorphism
   right.
*)
module FixException : FIX = struct
  type rfe = {lu : 'a 'b . (('a -> 'b) -> ('a -> 'b)) -> 
                            ((unit -> 'b) -> 'a -> 'b)}
  exception FE of rfe
  let u f g = f (fun n -> try g () with FE {lu = u'} -> u' f g n)
  let fix f = u f (fun () -> raise (FE {lu = u}))
end


let test = let module F = Fact(FixException) in F.fact5
;;

(* Objects already have fixpoints in them *)
module FixObjectS : FIX = struct
  class fixc = 
    object (self) 
      method fix' : 'a 'b. (('a->'b)->('a ->'b)) -> ('a->'b) = 
	fun f n -> f (self#fix' f) n end
  let fix f = (new fixc)#fix' f
end

let test = let module F = Fact(FixObjectS) in F.fact5
;;