Type visibility limitation in recursive modules

Type visibility limitation in recursive modules

["Márk S. Zoltán"]

Behold the following code snippet:

module rec Aleph :
    sig
        type t = Tag of Beth.t
    end =
    struct
        type t = Tag of Beth.t
    end
and Beth :
    sig
        type t
        val scandalous : Aleph.t
    end =
    struct
        type t = Aleph.t list
        let scandalous = Aleph.Tag((* HERE BE DRAGONS *) [])
    end

The compiler complains that the empty list after HERE BE DRAGONS has 
type 'a list but it is used with type Beth.t. I'd expect the compiler to 
discover that those types can be unified via 'a == Aleph.t, since as far 
as I can tell, all necessary facts are visible at that point. Replacing 
"Beth : sig type t ..." with "Beth : sig type t = Aleph.t list ..." does 
away with the error, but I would very much like to keep Beth.t an opaque 
type. Is this an intended behavior? And if it is intended, is there a 
way to tell the compiler what I really want it to do?

Thanks in advance for any help.

    Z-

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

[Peng Zang]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

I do not know if this is the intended behavior.  It may very well be.  
However, it appears we can easily work around this by simply abstracting the 
type later.  Eg.

module rec Aleph :
    sig
        type t = Tag of Beth.t
    end =
    struct
        type t = Tag of Beth.t
    end
and Beth :
    sig
        type t = Aleph.t list
        val scandalous : Aleph.t
    end =
    struct
        type t = Aleph.t list
        let scandalous = Aleph.Tag((* HERE BE DRAGONS *) [])
    end

module Beth = (Beth:sig type t val scandalous : Aleph.t end)


# Beth.scandalous;;
- - : Aleph.t = Aleph.Tag []
# Aleph.Tag [];;
- - : Aleph.t = Aleph.Tag []
# (Aleph.Tag []) = Beth.scandalous;;
- - : bool = true

Happy Holidays,

Peng



On Sunday 23 December 2007 09:24:55 am Márk S. Zoltán wrote:
> Behold the following code snippet:
>
> module rec Aleph :
>     sig
>         type t = Tag of Beth.t
>     end =
>     struct
>         type t = Tag of Beth.t
>     end
> and Beth :
>     sig
>         type t
>         val scandalous : Aleph.t
>     end =
>     struct
>         type t = Aleph.t list
>         let scandalous = Aleph.Tag((* HERE BE DRAGONS *) [])
>     end
>
> The compiler complains that the empty list after HERE BE DRAGONS has
> type 'a list but it is used with type Beth.t. I'd expect the compiler to
> discover that those types can be unified via 'a == Aleph.t, since as far
> as I can tell, all necessary facts are visible at that point. Replacing
> "Beth : sig type t ..." with "Beth : sig type t = Aleph.t list ..." does
> away with the error, but I would very much like to keep Beth.t an opaque
> type. Is this an intended behavior? And if it is intended, is there a
> way to tell the compiler what I really want it to do?
>
> Thanks in advance for any help.
>
>     Z-
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs


-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.7 (GNU/Linux)

iD8DBQFHbpj4fIRcEFL/JewRAiRrAJ9lkWenFBHkG2IwRTuRDVN92JCRPQCgjjZV
INwvriBZ/NF25J3ApX8lKn8=
=UpHJ
-----END PGP SIGNATURE-----

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

["Márk S. Zoltán"]

Peng Zang wrote:
> I do not know if this is the intended behavior.  It may very well be.  
> However, it appears we can easily work around this by simply abstracting the 
> type later.  Eg.
>
> module rec Aleph :
>     sig
>         type t = Tag of Beth.t
>     end =
>     struct
>         type t = Tag of Beth.t
>     end
> and Beth :
>     sig
>         type t = Aleph.t list
>         val scandalous : Aleph.t
>     end =
>     struct
>         type t = Aleph.t list
>         let scandalous = Aleph.Tag((* HERE BE DRAGONS *) [])
>     end
>
> module Beth = (Beth:sig type t val scandalous : Aleph.t end)
>
>
> # Beth.scandalous;;
> - - : Aleph.t = Aleph.Tag []
> # Aleph.Tag [];;
> - - : Aleph.t = Aleph.Tag []
> # (Aleph.Tag []) = Beth.scandalous;;
> - - : bool = true
>
> Happy Holidays,
>
> Peng
>
>   
Agreed, this does work for the code on the outside, but I wanted to hide 
the actual gory details of Beth.t from the implementation of Aleph too. 
The real-life Aleph contains a huge mess of inherited code (inherited 
from myself, but I wrote it years ago), plus some serious potential for 
quasi-macaronic growth. I wanted to make sure that none of that code 
makes assumptions about Beth.t, because the choice of Beth.t could 
easily have serious performance implications, and I would like to 
isolate the rest of the code from the impact of Beth.t turning overnight 
into an Aleph.t array or worse. That can only be done if the 
implementation of Beth is the only place where the details of Beth.t are 
known.

This is not exactly a showstopper issue for me, though. The reason I 
posted it was that (1) I suspect this is a bug (more likely a design 
bug, not an implementation one), and I like finding bugs, or (2) this is 
a pointer into something I really should understand about modules, and 
with any help I will understand it soon, as more replies come in.

Happy Holidays,

      Z-

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

["Márk S. Zoltán"]

Márk S. Zoltán wrote:
> Behold the following code snippet:
>
> module rec Aleph :
>    sig
>        type t = Tag of Beth.t
>    end =
>    struct
>        type t = Tag of Beth.t
>    end
> and Beth :
>    sig
>        type t
>        val scandalous : Aleph.t
>    end =
>    struct
>        type t = Aleph.t list
>        let scandalous = Aleph.Tag((* HERE BE DRAGONS *) [])
>    end
>
> The compiler complains that the empty list after HERE BE DRAGONS has 
> type 'a list but it is used with type Beth.t. I'd expect the compiler 
> to discover that those types can be unified via 'a == Aleph.t, since 
> as far as I can tell, all necessary facts are visible at that point. 
> Replacing "Beth : sig type t ..." with "Beth : sig type t = Aleph.t 
> list ..." does away with the error, but I would very much like to keep 
> Beth.t an opaque type. Is this an intended behavior? And if it is 
> intended, is there a way to tell the compiler what I really want it to 
> do?
>
> Thanks in advance for any help.
>
>    Z-
The plot thickens. The following code provokes an error message stating 
explicitly that type t in Beth is not the same as Beth.t:
----------------------
module rec Aleph :
    sig
        type t = Tag of Beth.t
    end =
    struct
        type t = Tag of Beth.t
    end
and Beth :
    sig
        type t   
        val a_beth_t_value : t
        val scandalous : Aleph.t
    end =
    struct
        type t = Aleph.t list
        let a_beth_t_value = ([] : t)
          let scandalous = Aleph.Tag(a_beth_t_value)
    end
----------------------
$ ocamlc -i Anomaly.ml
File "Anomaly.ml", line 18, characters 33-49:
This expression has type t = Aleph.t list but is here used with type Beth.t
---------------------

The error message references the mention of a_beth_value in the let 
scandalous ... line. The ([] : t) construct in the previous line was 
necessary to trigger the 'This expression has type t = Aleph.t list ...' 
message, since a bare [] only triggers "This expression has type Aleph.t 
list but ...", without an indication that it knows that type t is 
Aleph.t list.

However, reexporting a_beth_t_value from Aleph satisfies the compiler:
--------------------
module rec Aleph :
    sig
        type t = Tag of Beth.t
        val a_reexported_beth_t_value : Beth.t
    end =
    struct
        type t = Tag of Beth.t
        let a_reexported_beth_t_value = Beth.a_beth_t_value
    end
and Beth :
    sig
        type t
        val a_beth_t_value : t
        val scandalous : Aleph.t
    end =
    struct
        type t = Aleph.t list
        let a_beth_t_value = []
          let scandalous = Aleph.Tag(Aleph.a_reexported_beth_t_value)
    end
--------------------
$ ocamlc -i Anomaly.ml
module rec Aleph :
  sig type t = Tag of Beth.t val a_reexported_beth_t_value : Beth.t end
and Beth : sig type t val a_beth_t_value : t val scandalous : Aleph.t end
--------------------

So far it sounds like the compiler acknowledges there is a type Beth.t 
and identifies it with type t in the sig of Beth, but fails to make the 
connection between this type and the Aleph.t list type expression inside 
the struct of Beth. But even that is only true if the type expression in 
question uses a built-in list; if I replace it with an algebraic type 
implementing my own list, even the original example starts working.

-------------------
module rec Aleph :
    sig
        type t = Tag of Beth.t
    end =
    struct
        type t = Tag of Beth.t
    end
and Beth :
    sig
        type t   
        val scandalous : Aleph.t
    end =
    struct
        type t = Cons of Aleph.t * t | Nil
          let scandalous = Aleph.Tag(Nil)
    end
-----------------
$ ocamlc -i Anomaly.ml
module rec Aleph : sig type t = Tag of Beth.t end
and Beth : sig type t val scandalous : Aleph.t end
-----------------

This is a bug, isn't it?

Cheers

    Z-

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

["Márk S. Zoltán"]

The problem only impacts types declared via parametrized type 
constructors. To wit:

This does not work:
----------------------------------------
module rec Aleph : sig type t = Tag of Beth.t end =
   struct type t = Tag of Beth.t end
and Beth : sig type t val v : Aleph.t end =
   struct type t = Aleph.t list let v = Aleph.Tag([]) end

This does:
----------------------------------------
module rec Aleph : sig type t = Tag of Beth.t end =
   struct type t = Tag of Beth.t end
and Beth : sig type t val v : Aleph.t end =
   struct type t = Nil | Cons of Aleph.t * t let v = Aleph.Tag(Nil) end

And this does not:
----------------------------------------
type 'a mylist = Nil | Cons of 'a * 'a mylist
module rec Aleph : sig type t = Tag of Beth.t end =
   struct type t = Tag of Beth.t end
and Beth : sig type t val v : Aleph.t end =
   struct type t = Aleph.t mylist let v = Aleph.Tag(Nil) end

I have spent a few (dozen) hours debugging the compiler, and came to the 
conclusion that the reason for this bug is that "strenghtening" does not 
take place for Tconstr's. Tconstr types use their type_manifest fields 
to hold a description of the type, while Tvariant types set it to None. 
When the typing process of recursive modules reaches the strenghtening 
phase, it dutifully avoids updating Tconstr's because their 
type_manifest matches Some _, not None. As a result, Tconstr type 
implementations cannot be hidden inside a recursive module.

This issue has other interesting variations, e.g. this works:
-----------------------------------------------
module type AT = sig type t val v : t end
module type S = sig module Aleph : AT end
module Make = functor(A : AT) ->
    (struct module Aleph = A end : S with module Aleph = A)
module rec Al : AT =
    struct type t = string let v = "v" end
and Ex : S with module Aleph = Al = Make(Al)

This doesn't:
-----------------------------------------------
module type AT = sig type t val v : t end
module type S = sig module Aleph : AT end
module Make = functor(A : AT) ->
    (struct module Aleph = A end : S with module Aleph = A)
module rec Al : sig type t val v : t end (* NB: AT!!! *) =
    struct type t = string let v = "v" end
and Ex : S with module Aleph = Al = Make(Al)
-----------------------------------------------------
File "Anomaly.ml", line 34, characters 9-33:
In this `with' constraint, the new definition of Aleph
does not match its original definition in the constrained signature:
Modules do not match: sig type t = Al.t end is not included in AT
The field `v' is required but not provided
----------------------------------------------------

Cheers

   Z-

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

[Keiko Nakata]

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

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. But this is not particularly beautiful 
since a type constructor may escape its scope, 
although the implementation is kept sound. 

I would be very happy if you could give me a practical example 
which suffers from the double vision problem. 

A happy new year!
Keiko

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

["Márk S. Zoltán"]

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-

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

[Keiko Nakata]

> Unless you are talking about some other kind of hack, in which case I'd 
> be very grateful to hear more details.

Probably I was talking about something else.
(Please bear in mind that I've got this way of understanding the type checker 
via hacking the implementation; so it is likely that my understanding 
is incorrect.)

Let me consider:

module rec M : sig type t val x: t end = struct type t = int let x = M.x end

The type checker type checks the body of M, 
i.e., struct type t = int let x = M.x end, while the type environment records
M's signature as "sig type t val x: t end". But in fact one could perhaps 
enrich the signature to "sig type t = t val x: t end", 
where the right-hand side of the abbreviation t = t is the type t 
in the structure, not in the signature. 
As you may know, the type checker can distinguish the two types named t, 
since they internally carry different identities.
Since the type environments used to type check the body of M 
and the rest of the program are distinct, there is no possibility that 
type abstraction can be broken. 

This is not beautiful, since the type t in the right side of "t = t" 
escapes from its scope. 

I should note that this is not my original idea :-)

Thank you for the program. I will take it back home and look at it 
during the coming new year holidays.

Best,
Keiko