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

["Jérémie Lumbroso" <jeremie.lumbroso@etu.upmc.fr>]

Hello,

Thank you for your attempts ...

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:

module rec M : sig type t val f : t -> t end =
struct
   type t = int
   let f (x : M.t) = x
end

http://caml.inria.fr/pub/ml-archives/caml-list/2007/06/0d23465b5b04f72fedecdd3bbf2c9d72.en.html

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


And for the record, here is the latest (failed) rewrite of my modules.
I basically just did the same thing for the umpteenth time (abstract
all recursive/external references with local types, and then use
"with" conditions to try to coerce these).

I have however identified very clearly what is missing. The problem is
that recursivity is not fully supported with functors: if it were then
it would be possible to "reference" the arguments before they are
bound. Currently, I have:

module rec BMk : functor(Boxes : BOXES) ->
  functor (Validator : VALIDATOR with type bbt = Boxes.B.t) ->

What I would need is:

module rec BMk : functor(Boxes : BOXES with type vt = Validator.t and
type bat = Boxes.A.t) ->
  functor (Validator : VALIDATOR with type bbt = Boxes.B.t) ->

However, of course, Caml tells me that "Validator" is unbound. I
suspect this is what you've tried to do yourself (a wrapper module
which defines all "argument" modules as a recursive set of modules,
which can then be mutually recursively referenced). Am I wrong?

All the best,
Jérémie

  <code:"code_min_mutrec4.ml">
  (****************)
  (* MODULE Boxes *)
  (****************)

  module type BOXES =
  sig
    type vt  (* Validator.t *)
    type bat (* Boxes.A.t *)

    (* NOTE: I which modules A and B where only accessible by Boxes itself,
       but not by Validator. (And have something such as type t = B.t) *)

    module A : sig
      (* This type was simplified for explanatory purposes. *)
      type t = private
               | Anil
               | Aout of vt
    end

    module B : sig
      type t = private
               | Bnil
               | Bout of bat * t
    end

  end

  module type VALIDATOR =
  sig

    type bbt (* Boxes.B.t *)

    (* This type has been simplified for explanatory purposes. *)
    type t = Me of int | Node of t * t | B of bbt

    val fold_on_B : (bbt -> 'a) -> ('a -> 'a -> 'a) -> 'a -> t -> 'a

  end


  module rec BMk : functor(Boxes : BOXES) ->
    functor (Validator : VALIDATOR with type bbt = Boxes.B.t) ->
      BOXES with type vt = Validator.t
            and type bat = Boxes.A.t =
    functor (Boxes : BOXES) ->
      functor (Validator : VALIDATOR with type bbt = Boxes.B.t) ->
  struct

    type vt = Validator.t
    type bat = Boxes.A.t

    module rec A : sig
      type t = | Anil
               | Aout of vt

      val boolfold : ('a -> bool) -> ('a -> bool) -> bat -> bool
    end =
    struct
      type t = | Anil
               | Aout of vt

      let boolfold p1 p2 =
        let rec aux = function
          | Boxes.A.Anil    -> false
          | Boxes.A.Aout elt ->
              Validator.fold_on_B (fun x -> B.boolfold p1 p2 x) (||) false elt
        in
        aux
    end

    and B : sig
      type t = | Bnil
               | Bout of A.t * t

      val boolfold : ('a -> bool) -> ('a -> bool) -> Boxes.B.t -> bool

    end =
    struct
      type t = | Bnil
               | Bout of A.t * t

      let boolfold p1 p2 =
        let rec aux = function
          | Boxes.B.Bnil        -> false
          | Boxes.B.Bout(a, elt) -> (A.boolfold p1 p2 a) || (aux elt)
        in
        aux
    end

  end

  (********************)
  (* MODULE Validator *)
  (********************)

  module rec VMk :
    ( functor(Validator : VALIDATOR) ->
        functor (Boxes : BOXES with type vt = Validator.t) ->
          VALIDATOR with type bbt = Boxes.B.t ) =
    functor(Validator : VALIDATOR) -> functor (Boxes : BOXES) ->
  struct

    type bbt = Boxes.B.t
    type t = Me of int | Node of t * t | B of bbt


    (* This functions must allow me to do "fold-like" operations on object
    of type t, specifically targetting nodes of type B of Boxes.B.t *)

    let fold_on_B f combinator default =
      let rec aux = function
        (* Recursive calls down the tree. *)
        | Node(b1, b2) -> combinator (aux b1) (aux b2)

        (* Leaves which must be processed. *)
        | B r             -> f r

        (* Leaves which must be ignored, and return the default value. *)
        | _               -> default
      in
      aux

  end
  </code>