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

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

[Claudio Russo]

> 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
 

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

[Alain Frisch]

On Wed, 10 Jan 2001, Claudio Russo wrote:

> Moscow's recursive modules have the advantage that they
> leverage many of the concepts already existing in the Definition. If I
> recall correctly, they require one new kind of semantic object, a simple
> generalisation of enrichment, and two new syntactic constructs with
> associated evaluation and typing rules. Current main drawbacks: heavy
> syntax requiring forward declarations,
>  no support for cross-compilation-unit recursion and recursion on module
> terms requires a dynamic check for each
> forward reference (this is because the implementation imposes no
> restriction on whether the recursion is safe or not, forcing a dynamic
> check for definedness).

Are there real examples using recursive modules with these restrictions ?

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

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.


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


About mixins: what is the proposed dynamic semantic ?  I guess the
evaluation of the mixins, which can have side effects or depend on the
environment, is done when then composition yields a fully defined
structure. But this operation involves a reordering of the definitions,
so it may be non trivial to predict the evaluation order of the different
fields. Is there a requirement for the ordering to be compatible when
possible with the order of definition for values/submodule in each mixin
of the composition ?


-- 
  Alain Frisch