RE: first class, recursive, mixin modules (was: RE: first class modules)

["Claudio Russo" <crusso@microsoft.com>]

> Are there real examples using recursive modules with these 
> restrictions ?

Well, it depends on what do you mean by real...
They are useful, together with first-class modules, for doing object
encodings (albeit rather heavy ones). 
You get polymorphic recursion for free (but at the cost of the dynamic
check, which could be optimized away in this case), but there are
simpler mechanisms for this.
Chris Okasaki's elegant bootstrapped heap implementation requires them
(+ other features)
 (see the mosml distribution).
They are probably useful for things like CORBA to ML bindings that use
the ML modules language to capture
the structure of the mutually recursive IDL interfaces. 
An then there's the example of the Ocaml modules/core typechecker that
you mention.


> You can always define everything outside the structures (or 
> in the first
> one), then copy the types and values in the structures. Of course, you
> loose the modularity of definitions, but with recursive modules as in
> MosML, you loose the static typing for the module language (Bind
> exceptions) and also the modularity (different source files;
> separate compilation). 

I'm not sure what you meant by losing static typing. It's just that
typing for
recursive modules now gives you a weaker property --- either the
recursive expression evaluates or
raises the exception Bind. It never  seg faults. I think it would be
possible to refine the type system
to detect unsafe recursion and avoid dynamic checks for safe recursion,
but this is alot more work and may well
interact with other features of the type system. Note that it is already
possible to use a syntactic criterion to avoid some dynamic checks
(something like those under functions that don't get called in the
recursive module), as an optimisation. And of course, you can always
still use the reference tying trick of Ocala.

> If you accept runtime checks, the solution adopted
> in the OCaml compiler to break the circle of dependencies between
> the Core and Module type checkers (forward declaration with a 
> reference
> updated when the definition is available) has the advantage 
> of retaining
> separate compilation.

But this only works for mutually recursive functions that span module
boundaries, not datatype definitions.
You'll note in the caml sources that the abstract syntax tree and typed
abstract syntax tree for module
are defined in a single datatype definition, not separately. Although
it's possible to separate them out
using type parameters, this is pretty inconvenient in practice. 

> Back to first class packaged modules: a very useful feature 
> for runtime
> configuration of applications would be the possibility to load the
> packages from the disk/network (that is, dynamic loading; the
> signature of trusted packages can be checked as in the 
> Dynlink module).

This shouldn't be too difficult. I have an example of using that used
Moscow ML's Dynlib library to construct
an ADT to a C shared library, if it exists, and default ADT otherwise.
This is similar to what you want, except for
loading a C library.
 
Cheers, 
Claudio