Re: [Caml-list] Limitations of first-class modules

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2011/01/19, at 21:33, Lauri Alanko wrote:

> When first-class modules were announced for OCaml 3.12, I cheered them
> as a sorely needed extension, and I have now begun to make heavy use
> of them. I certainly prefer them over objects, even if I do find the
> syntax of first-class modules a bit awkward. I would much prefer to
> see a completely unified object-module system a la Scala, but I guess
> such drastic changes are beyond the scope of OCaml's development
> nowadays.
> 
> Anyway, I'm now beginning to stumble into the limitations of the
> extension, and I'm a bit curious about their rationale.
> 
> In a type (module S), S must be a path to a named module type, and if
> A and B are two different paths, (module A) and (module B) are
> distinct even if A and B are transparent definitions for exactly the
> same module types. This nominalism is quite surprising since one is
> used to transparent definitions being just shorthands for signatures
> that are compared structurally. In particular, this means that it is
> no longer harmless to include a signature definition to compose a
> convenience module from several submodules:
> 
> module A = struct 
>  module type S = sig end
>  type t = (module S)
>  module M : S = struct end
>  let v = (module M : S)
> end
> 
> module B = struct
>  include A
> end
> 
> # module X : A.S = B.M;;
> module X : A.S
> 
> # let x : A.t = B.v;;
> Error: This expression has type (module B.S)
>       but an expression was expected of type A.t = (module A.S)

I think there are two reasons for this limitation:
* avoiding having to run a full module type comparison during unification
  (potentially costly)
* in case the first-class module has type variables in its parameters,
   the original algorithm for module type comparison cannot be applied directly

I'm not sure the first reason matters that much.
The second one is more problematic, but clearly does not apply to your case.
So it should at least be possible to check module type equality structurally for
parameter-less first-class module types.

Note that if you use the trunk version (3.13), you need less annotations, so
you could write:
   let x : A.t = (module (val B.v))
A bit verbose, but no extra type annotations.

> Also, the limitations of package type constraints were also somewhat
> surprising.

The main goal of package type constraints is to allow connecting
types in the signature with type variables in the context.
Since type variables cannot have higher-order kinds in ocaml,
allowing to specify parameterized types in with constraints would
not make sense from that point of view.
It may still be useful, but there may be difficulties in connection with
the new implicit pack/unpack mecanism.

Jacques Garrigue