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

[Alain Frisch <alain.frisch@lexifi.com>]

On 01/19/2011 01:33 PM, 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.

As Jacques mentioned, OCaml 3.13 will allow a lighter syntax, with a lot 
less explicit type annotations. Hopefully, this will make it less 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.

Indeed.

> 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.

One could indeed declare that (module A) and (module B) are equal
as soon as A and B refer to equal module types (that is, two module 
types subtype of each other without any coercion). I don't think there 
is any deep obstacle in doing that. One would need to be a little bit 
careful with mutually recursive types and module types (introduced with 
a recursive module).  As for the implementation strategy, I'm a little 
bit concerned of having a low-level module in the type-checker (Ctype), 
in charge of things like type equality check or unification, calling a 
function in a higher-level module (Includemod), but I don't see 
immediately any concrete problem in doing that.

What would be much more difficult is to declare that general package 
type (with constraints, like (module A with type t1 = T1)) are equal if 
the module types obtained by "applying the constraints" are equal. 
Indeed, the type T1 above can contain type variables, and a constraint 
"with type t1 = T1" is then not supported by the module system (there is 
no module type with free type variables).


There is a branch fstclassmod_parametrized in the SVN which allows more 
kinds of constraints; in particular, it allows constraints on 
parametrized types (module A with type 'a t1 = T1). See e.g.

http://caml.inria.fr/mantis/view.php?id=5078

This extension does not seem very useful to me in practice (because 
there is no polymorphism on type constructors in OCaml). Moreover, it 
isn't trivially combined with Jacques' work mentioned above. So it's 
probably not going to be integrated upstream.


Feel free to open entries in the bug tracker with specific examples of 
things you'd like to do but which are not possible or difficult with the 
current design.  My initial work on first-class modules was driven by 
our internal use at LexiFi (for which the nominal aspect has never been 
a problem) and also by the constraint of keeping the patch small enough 
(to increase the odds of being accepted upstream).



Alain