Browse thread
Separating two mutually recursive modules (was Specifying recursive modules?)
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ 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