Re: [Caml-list] Separating two mutually recursive modules

[Keiko Nakata <keiko@kurims.kyoto-u.ac.jp>]

Hello.

> I know of the "double vision" problem, and I am actually confused by
> the post which you reference. I think it discusses an old version of
> the typechecker, as the example which Xavier Leroy gives supposedly to
> illustrate the flaw now (3.10.2) properly type-checks:

Yes; I was forgetting the fix. Sorry for confusing you. 
But I believe the previous program I posted should type check, 
so I am not sure whether the fix is complete. 
Furthermore, I may suspect the problem there has something to do with 
OCaml's way of handling applicative functors; I am not sure though. 

For what it's worth, I managed to type check my previous attempt, 
which is attached below; the trick is to add the manifest type specification 
"type t = Boxes.T.t" to the signature of the module T. 
Unfortunately, I do not know exactly why this trick works. 

> XL also mentions a solution for this problem: resorting to variants,
> so Caml explicitly flags the type, thus preventing it from
> "forgetting" how a given type was defined.
> 
> I wonder if the specific problem which was solved by this hack still
> exists (and if it is in fact the problem that I'm encountering here).
> 
> Do you (or anybody else) have any idea (if I can /) how to adapt the
> "variant hack" to my problem ...

I have tried it by wrapping the type t of module T with variants,
but I could not make it type check. Maybe I did it wrongly. 

With best,
Keiko


--------------------------------

module type BOXES_PROVIDER =  sig  module T : sig type t end  end 

module type FVALIDATOR = functor(Boxes: BOXES_PROVIDER) ->
sig
  type t = Me of int | Node of t * t | B of Boxes.T.t
  val fold_on_B : (Boxes.T.t -> 'a) -> ('a -> 'a -> 'a) -> 'a -> t -> 'a
end

module BoxesProvider(FValidator : FVALIDATOR) : 
sig module Boxes : BOXES_PROVIDER end = struct
  module rec Validator : sig 
    type t
    val fold_on_B : (Boxes.T.t -> 'a) -> ('a -> 'a -> 'a) -> 'a -> t -> 'a end 
      = FValidator(Boxes) 
  and Boxes : sig module T: sig type t end end = struct
    module rec T : sig 
      type t = Boxes.T.t
      val o_f : ('a -> bool) -> ('a -> bool) -> t -> bool
    end = 
      struct 
	type t = T of B.t 
	let o_f p1 p2 = function T x -> B.o_f p1 p2 x
      end
    and A : sig
      type t = | Anil| Aout of Validator.t
      val o_f : ('a -> bool) -> ('a -> bool) -> t -> bool end = struct
	type t = | Anil | Aout of Validator.t
	let o_f p1 p2 =
          let rec aux = function
  	    | Anil    -> false
  	    | Aout tv -> 
  		Validator.fold_on_B (fun x -> T.o_f p1 p2 x) (||) false tv
          in
          aux
      end
    and B : sig
      type t =  Bnil | Bout of A.t * t
      val o_f : ('a -> bool) -> ('a -> bool) -> t -> bool  end =  struct
	type t =  Bnil | Bout of A.t * t
	let o_f p1 p2 =
          let rec aux = function
  	    | Bnil        -> false
  	    | Bout(a, tv) -> (A.o_f p1 p2 a) || (aux tv)
          in
          aux
      end
  end
end

module FValidator(Boxes: BOXES_PROVIDER) : sig 
  type t = Me of int | Node of t * t | B of Boxes.T.t
  val fold_on_B : (Boxes.T.t -> 'a) -> ('a -> 'a -> 'a) -> 'a -> t -> 'a
end =
  struct
    type t = Me of int | Node of t * t | B of Boxes.T.t
    let fold_on_B f combinator default =
      let rec aux = function
        | Node(b1, b2) -> combinator (aux b1) (aux b2)
        | B r          -> f r
        | _            -> default
      in
      aux
  end

module Boxes = BoxesProvider(FValidator)