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

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

[Jérémie Lumbroso]

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

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

[Keiko Nakata]

Hello,


> 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;)

Can I look at the code which does not type check without Obj.magic?
Ideally something like if I comment out Obj.magic then I get a type error,
and if I comment it in then the code type checks, 
so that I can identify the point of the issue?
(In the context of this simplified example of Boxes & Validator)

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

But B is not in the scope, isn't it?

With best,
Keiko

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

[Jérémie Lumbroso]

Hello,

> Can I look at the code which does not type check without Obj.magic?
> Ideally something like if I comment out Obj.magic then I get a type
> error, and if I comment it in then the code type checks, so that I can
> identify the point of the issue? (In the context of this simplified
> example of Boxes & Validator)

Yes, and thank you for taking an interest! I do have a warning though:
this code is not correct, in the sense that, it doesn't type and it
*shouldn't* type (because while in this case Validator.Boxes.t *is*
equivalent to B.t, there is nothing but my "good will" that guarantees in
the specs of the modules that this is so).

Attempts to make this correct (for the type checker) with "with type"
conditions have failed.

The mutually recursive version I posted in the previous message is an
"evolution" from this (and that mutually recursive version, contrarily to
this one is "correct").

  <code:"code_min_with_objmagic.ml">
  module type BOXES_PROVIDER =
  sig
    type t
  end

  module type VALIDATOR =
  sig
    module Boxes : BOXES_PROVIDER

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

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


  module BoxesProvider(Validator : VALIDATOR) : BOXES_PROVIDER =
  struct

    module rec 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

      (* There is no equality between Validator.Boxes.t and B.t, i.e.:
         failing to see this is not a problem with the typechecker.
         To get the type error, replace with "let crosstype x = x". *)

      let crosstype (x : Validator.Boxes.t) =
        ((Obj.magic x) : B.t)

      let o_f p1 p2 =
        let rec aux = function
  	| Anil    -> false
  	| Aout tv ->
  	    Validator.fold_on_B (fun x -> B.o_f p1 p2 (crosstype 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

    type t = B.t

  end


  module rec Validator : VALIDATOR (* with type Boxes.t =
Validator.Boxes.t ?? *) =
  struct

    module Boxes = BoxesProvider(Validator)

    type t = Me of int | Node of t * t | B of Boxes.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
  </code>

> >   (********************)
> >   (* 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 =
>
> But B is not in the scope, isn't it?

Indeed. What I meant to say is, "IDEALLY, Boxes.B.t would simply be
Boxes.t" (and Validator would not need to know about submodules A and/or
B).

Please, of course, don't hesitate to ask for any other details you might
need (and don't hesitate to tell me if this Obj.magic code is not what you
needed!).

All the best,
Jérémie

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

[Keiko Nakata]

Hello.

I could not solve your problem, but I report my attempt encountering
a known limitation of the type checker, which may be of some help to you.

The following program raises a type error:
"This expression has type Boxes.T.t but is here used with type B.t"
when typing the second branch of A.o_f.
It must be possible and sound to equate Boxes.T.t and B.t there,
but the type checker is not aware of it;
T's signature manifests the equality to A, but not to Validator. 

This problem is known as the double vision problem;
related discussions are found, for instance:
http://caml.inria.fr/pub/ml-archives/caml-list/2007/06/9d75407428bc2c403b99359bec646af2.en.html

As a consequence, I do not know how I can make your program type check
without revealing the sub-module B.  

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) : BOXES_PROVIDER = 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 = B.t end = struct type t = B.t 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 -> B.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

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

[Jérémie Lumbroso]

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>

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

[Keiko Nakata]

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)