Re: [Caml-list] type aliases and recursive modules

["Andreas Rossberg" <AndreasRossberg@web.de>]

"Josh Berdine" <berdine@dcs.qmul.ac.uk>:
> #
> module rec A : sig
>  type t = It of ASet.t
>  val compare : t -> t -> int
>  val get : t -> ASet.t
> end = struct
>  type t = It of ASet.t
>  let compare = compare
>  let get = function It(x) -> x
> end
>
> and ASet : sig
>  type t
>  val get_its_elements : t -> A.t list
> end = struct
>  module C = Set.Make(A)
>  type t = C.t
>  let get_its_elements x = C.elements (A.get (C.choose x))
> end
>
>                                      Characters 350-370:
>    let get_its_elements x = C.elements (A.get (C.choose x))
>                                        ^^^^^^^^^^^^^^^^^^^^
> This expression has type ASet.t but is here used with type
>  C.t = Set.Make(A).t

You are suffering from the "double vision" problem. This arises when you 
have a recursive module with an abstract type and attempt to cross the 
abstraction boundary recursively. The type system does not make the abstract 
type recursively transparent. Here is a simpler example:

# module rec A : sig type t val f : t -> t end =
  struct type t = int let f (x : t) = A.f x end;;
This expression has type t = int but is here used with type A.t

You cannot do that in current Ocaml. The only way to avoid this problem is 
by making the type t transparent in the ascribed signature.

This problem actually is not straightforward to address on the 
type-theoretic level, and one of the reasons why recursive modules are 
pretty much an open research topic.

Hope this helps,
- Andreas