Version française
Home     About     Download     Resources     Contact us    
Browse thread
Separating two mutually recursive modules (was Specifying recursive modules?)
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Keiko Nakata <keiko@k...>
Subject: Re: [Caml-list] Separating two mutually recursive modules
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