Re: [Caml-list] Type visibility limitation in recursive modules

["\"Márk S. Zoltán\"" <zoltan.s.mark@dravanet.hu>]

Keiko Nakata wrote:
> Hello. 
>
> I have not thoroughly read your posts,
> but it looks like the double vision problem. 
>
> You may be interested in the following post to camllist:
>
> http://caml.inria.fr/pub/ml-archives/caml-list/2007/06/0d23465b5b04f72fedecdd3bbf2c9d72.en.html
>   
Thanks; somehow I haven't found that particular post when I was 
searching for precedents. Not having managed to understand the double 
vision problem, I still I happen to think it is not a good explanation 
in this case for many reasons. Even Xavier agrees in the above linked 
post that this is a bug of the current implementation, i.e. not a 
theoretical issue. If it was due to some sort of theoretical difficulty, 
variant types would fail at it too, but they don't. This is a plain bug 
- the way type equations are stored is a kludge, as it uses the 
type-manifest field which already plays an only distantly related role.
> By the way, I believe one can hack the OCaml type checker 
> to (mostly) avoid the problem by "strengthening" 
> the external signature of the recursively defined module 
> in the type environment. 
Something like this is actually done in the code - when typing the 
structs, the encountered type declarations are strengthened to point to 
themselves as seen from outside of the module. The problem is that this 
is only doable for variant and record types due to legacy design 
decisions in the actual implementation, namely that type abbreviations 
are represented in the current implementation in a way which does not 
allow storing the results of such strenghtening, and that the compiler 
silently passes over a type it cannot strenghten this way, probably in 
the hope of not causing hard-to-relate problems later. I really find it 
hard to emphasize enough that this cannot be a theoretical impossibility 
if it works for variant types.

Unless you are talking about some other kind of hack, in which case I'd 
be very grateful to hear more details.
> But this is not particularly beautiful 
> since a type constructor may escape its scope, 
> although the implementation is kept sound
>   
You mean like in http://caml.inria.fr/mantis/view.php?id=3993 ? The 
situation is caught by the compiler, fortunately, so I don't feel 
worried about it. I wonder, though, if there is any other way for this 
escape to happen except the '_a-style delayed typing, like ref [], which 
IMHO should be rejected as untypeable in the absence of explicit type 
annotations, not courteously typed to '_a list.
> I would be very happy if you could give me a practical example 
> which suffers from the double vision problem. 
>   
I could give you the skeleton of what I am trying to implement, which is a pattern matching & rewriting engine. I am not sure if it is a practical example of the double vision problem, since I don't know what it is.

module type NumbersS : sig ... end
module type AtomsS : sig ... end

module type ReprS : 
  sig
    module Numbers : NumbersS
    module Atoms : AtomsS
    module rec Terms : sig type t = <variant type def here, using Seq.t> ... end
    and Seq : sig type t ... end
  end

module RepresentationF =
  functor(N : NumbersS) ->
  functor(A : AtomsS) ->
  (struct
    module Numbers = N
    module Atoms = A
    module rec Terms : sig ...<as above> end =
      struct ...<stuff using Seq.t> ...end
    and Seq : sig type t ... end =
      struct type t = Terms.t list <or something awful like that>
      ...
    end
  end : ReprS with module Numbers = N and module Atoms = A)

module type RewriterS =
  sig
    module Numbers : NumbersS
    module Atoms : AtomsS
    module Representation : ReprS with module Atoms = Atoms and module Numbers = Numbers
    ...
  end

module RewriterF =
  functor(N : NumbersS) ->
  functor(A : AtomsS) ->
  functor(R : ReprS with module Atoms = A and module Numbers = N) ->
  (struct
    ...
  end : RewriterS with module Numbers = N and module Atoms = A and module Representation = R)

module MyNumbers : NumbersS = struct .. end

module rec MyAtoms : sig ... end <includes AtomsS and uses Driver.* stuff> =
  struct ... end
and MyRepresentation : ReprS with module Numbers = MyNumbers and module Atoms = MyAtoms
  = RepresentationF(MyNumbers)(MyAtoms)
and MyRewriter 
  : RewriterS with module Numbers = MyNumbers and module Atoms = MyAtoms and module Representation = MyRepresentation
  = RewriterF(MyNumbers)(MyAtoms)(MyRepresentation)
and Driver : sig ... end = struct ... <stuff making use of all other modules> ... end
 
Basically, I want to 
- separate the numeric part (plain OCaml numeric types vs. Bignum lib vs. ocamlgmp). 
- postpone decisions about the actual structure of atoms (this code will be reused in many projects, and in some of them atoms may contain complex structures making use of Representation.Terms.t and Representation.Seq.t)
- isolate the implementation details of Seq from Terms (Seq.t: list? array? map?) and make sure Terms does not make assumptions about the Seq.t type (the struct of Terms is a huge mess of legacy code)
- keep the pattern-matching and rewriting bytecode engine isolated from the representation details
- keep the actual driver separate from the rewriter too (the same Rewriter could be used with different drivers, e.g. one with memoizing, one without, one with memoizing open to explicit insertion of memoized cases; the driver might make use of builtins for certain kinds of terms, sport a typing system or not - and it would probably store lots of such information in the atoms, not in maps from atoms to information).

Of course there are other, non-rec ways to get there, but I don't want to just yet. Apart from arriving to a more straightforward code using module rec, this is a hobby project, so I can afford to wait for a solution.

Cheers

   Z-