Separating two mutually recursive modules (was Specifying recursive modules?)

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

Hello,

In the same vein as:

  <code>
  let rec p_even odd x =
    if x = 1 then false
    else x = 0 || (odd (x - 1))

  let rec p_odd even x =
    if x = 0 then false
    else x = 1 || (even (x - 1))

  ...

  let rec even x = p_even odd x
  and odd x = p_odd even x
  </code>

where I define two mutually recursive functions but only combine them
later, I would like to separate two modules, named Boxes and
Validator, which are mutually recursive.

I've tried to imitate the above-mentionned transformation, but such
attempts haven't amounted to much because, (a) I am unable to write
recursive functors, i.e.: crazy stuff such as "module rec F :
functor(A : TA with type t = F(A).t) -> TF"; (b) not only are my main
modules mutually recursive, but one depends on itself as well.

The crux of my problem, is that I have "grammar" that *must* be broken
down into several modules: different "components" from this grammar
are handled (entirely) by separate modules, and no module should be
dependent on how each modules handles its task (of course). It is as
if I had:

  <code>
  module Bools(Main : M) : sig type t ... end =
  struct
    type t = True | False | Not of t | Equal of Main.t * Main.t
    ...
  end

  module Nats(Main : M) : sig type t ... end =
  struct
    type t = Zero | Succ of t
    ...
  end

  module Minilanguage =
    functor (BoolMod : ...) ->
    functor (NatMod : ...) ->
  struct
    type t = | Stuff of ...
             | Bool of BoolMod.t
             | Nat of NatMod.t
             ...
    ...
  end
  </code>

The problem is not in defining this language; it arises when I try to
write a "fold" function on the grammar, while maintaining these
conditions:

  - the individual 't' types are abstract (I don't want the details of
    the grammar to be accessible from "outside");

  - because the goal is modularization I *cannot* resort to some trick
    wherein I create a "parent" module which contains all types, and
    then have the other modules "inherit" from it;

  - the various solutions I've examined (for instance, making
    Boxes.B.t a parameterized type) have been unsatisfactory (for
    various reasons with which I don't want to burden this paper
    with---even more than it already is!);

  - the fold must, for instance allow the Bools module to provide a
    function that takes a Minilanguage.t tree value, and transforms it
    by prefixing every boolean with a Not, i.e.:

      Bool(Equal(Nat(Zero), Nat(Succ(Zero))))
      --> Bool(Not(Equal( .., .. )))


I have been unable to cleanly specify the code below (or something
equivalent) without resorting to Obj.magic. (In the example below,
"Boxes.B.t" as referenced by the Validator module would ideally simply
be "Boxes.t", and Validator would not "see" the submodules;)

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

  module rec Boxes : sig

    (* 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 Validator.t
    end

    module B : sig
      type t = private
    	     | Bnil
    	     | Bout of Boxes.A.t * t
    end

  end =
  struct

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

      val boolfold : ('a -> bool) -> ('a -> bool) -> Boxes.A.t -> bool
    end =
    struct
      type t = | Anil
               | Aout of Validator.t

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

  and Validator : sig

    (* This type has been simplified for explanatory purposes. *)
    (* IDEALLY, Boxes.B.t would simply be B.t. *)
    type t = Me of int | Node of t * t | B of Boxes.B.t

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

  end =
  struct

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


    (* This functions must allow me to do "fold-like" operations on
       objects 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>

This is a Gordian knot---of that I am fully aware.

I'd welcome any help/hint/moral support with arms wide open; at this
point I fear I've simply hit a (Berlin-sized) wall.

Jérémie