RE: first class modules (was: alternative module systems)

RE: first class modules (was: alternative module systems)

[Claudio Russo]

(This was a response to Xavier and Mosml hackers, but I've been asked to
forward it to the list).

> Hi Claudio,
> 
> > BTW, in Moscow ML, the "open" construct is integrated more naturally
> > as a special form of declaration, plus a side condition that
> > disallows an open declaration from appearing within the body of a
> > functor (for soundness reasons). This lets you open first-class
> > modules at top-level and within substructures, which can be more
> > convenient.
> 
> That sounds interesting.  I was thinking exactly along these lines.
> Do you have this written down somewhere?
> 
> Xavier

In Moscow there is no separate open expression, just a new form of
structure binding that let's you deconstruct a
first-class module (there is a similar form for functors):

<strbind> := ... | <strid> as <sigexp> = <exp>

This lets you write declarations like


structure Bar as S = if .. then .. else ...;

wherever an ordinary declaration can occur.

This is actually more general (and convenient) than the open construct
because it lets you open first-class modules  at top-level and within
structure bodies, not just within Core expressions. If functors are
always generative, this is ok, but it interacts badly  with applicative
functors (programs can go "wrong"). 
To avoid this, in Moscow we simply place a syntatic restriction on
functor bodies: 
"the body of any functor (whether applicative or generative) cannot
contain a structure level declaration of the 
 above form,  *unless* that declaration occurs within a dec in a Core
"let <dec> in <exp> end" expression"

In the examples below, the structure Ok is legal, the functor Wrong is
illegal but the functor Ok is legal.

signature S = sig type t val f:t end;
structure A = struct type t = int -> int val f x = x+1 end;
structure B = struct type t = bool  val f = true end;
structure Ok as S = if ... then [structure A as S] else  [structure B as
S] (* legal *)
functor Wrong(val b:bool) = 
struct structure C  as S =if b then [structure A as S] else  [structure
B as S]                            
end (* ilegal, because of "open" within immediate structure binding *)

functor Ok(val b:bool) = 
struct val c = let structure C as S = if b then [structure A as S] else
[structure B as S]
	                                in  ...
                                      end
end (* legal again, because "open" is within Core let. *)

I've got a formal revision of the SML definition,  if anyone is
interested, just ask.

The Mosml doc also describes the syntax in more detail (if I recall
correctly).
Of course, it's probably possible to come up with a more permissive
restriction, but I like this one because its simple.

Cheers,
Claudio




 

RE: first class modules (was: alternative module systems)

[Claudio Russo]

> > > a few month ago, Markus Mottl pointed to this mailing 
> list the work by
> > > Claudio Russo on first class modules. There were no 
> answer about plans to
> > > implement such a system for OCaml.
> > 
> > Well, it seems like Russo's first-class modules could be added with
> > relatively little effort, if there is a sufficient need for them.
> 
> Does this include the recursive modules aspect of Moscow ML 
> too? That's
> where I feel the shoe pinching. I realize that at least one 
> big name in
> the ML community dislikes the notion and admittedly my main 
> issue could be 
> resolved by a recursion between a type definition and a 
> module but it can
> also be fixed with recursive modules. The problems arise 
> fairly frequently.

The discussion is about first-class modules only, I think. Recursive
modules are
a completely separate issue. You can support either without the other.
Although Moscow supports recursive structures, their status is
"experimental", 
but I thought adding something simple was better than nothing at all. 
Recursive functors should be an easy generalisation of recursive
structures;
I didn't put them in because I couldn't find any nice examples (but I
didn't look very hard either).

> Do the implementors have any impressions as to whether the 
> Moscow ML approach or
> the "mixin module" approach discussed here will be used to 
> address this
> problem? 

Has the mixin module stuff been formalised enough for actual
implementation? 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). (BTW, the distribution has a minor bug but this
is fixed for the next release.)

Cheers,

Claudio
> -- Brian
> 
> 

Re: first class modules (was: alternative module systems)

[Brian Rogoff]

On Mon, 8 Jan 2001, Xavier Leroy wrote:
> > a few month ago, Markus Mottl pointed to this mailing list the work by
> > Claudio Russo on first class modules. There were no answer about plans to
> > implement such a system for OCaml.
> 
> Well, it seems like Russo's first-class modules could be added with
> relatively little effort, if there is a sufficient need for them.

Does this include the recursive modules aspect of Moscow ML too? That's
where I feel the shoe pinching. I realize that at least one big name in
the ML community dislikes the notion and admittedly my main issue could be 
resolved by a recursion between a type definition and a module but it can
also be fixed with recursive modules. The problems arise fairly frequently.

Do the implementors have any impressions as to whether the Moscow ML approach or
the "mixin module" approach discussed here will be used to address this
problem? 

-- Brian

RE: first class modules (was: alternative module systems)

[Claudio Russo]

Hi Frank,

This should do it...

signature S = sig type t; val x: t; val y: t -> int end;
functor F A:sig val b: bool end = struct 
  structure X as S = if A.b 
     then [structure struct type t = int; 
                      val x = 0; 
		          val y = fn x:t => x
                     end as S]
     else [structure struct type t = int -> int; 
                      val x = fn x:int => x;  
	                val y = fn f:t => f 1  
                     end as S]
end; (* X.t depends on the value of A.b *)
structure Y = F(struct val b = true end); 
structure Z = F(struct val b = false end); 
(* if functors are applicative then Y.X.t = Z.X.t *)
val z = Z.X.y (Y.X.x)  (* applies 0 to 1, a run-time error *)

Note that the definition of z  goes "wrong" if F is applicative (a la
O'Caml, and expressible in Mosml syntax by omitting the parenthesis
around A:sig ... end), 
but is ill-typed if F is generative (as in Standard ML). The program is
rejected by the (crude)
syntactic restriction that functor bodies can't eliminate first-class
modules, 
except within inner Core let expressions.

Section 7.4 of my thesis discusses this issue in detail. Xavier's paper
on applicative functors has a similar example. The example above appears
in my forthcoming Nordic Journal of Computation article.

Cheers,

Claudio

> -----Original Message-----
> From: Frank Atanassow [mailto:franka@cs.uu.nl]
> Sent: 09 January 2001 12:31
> To: Claudio Russo
> Subject: Re: first class modules (was: alternative module systems)
> 
> 
> Hello,
> 
> Claudio Russo wrote (on 08-01-01 07:11 -0800):
> > This is actually more general (and convenient) than the 
> open construct
> > because it lets you open first-class modules  at top-level 
> and within
> > structure bodies, not just within Core expressions. If functors are
> > always generative, this is ok, but it interacts badly  with 
> applicative
> > functors (programs can go "wrong"). 
> 
> I have seen you allude to this type soundness issue several 
> times now. Can you
> give an example of a bad program which violates your 
> condition?  (Or just
> point me to the place in your thesis or a paper where it is 
> elucidated.)
> 
> -- 
> Frank Atanassow, Information & Computing Sciences, Utrecht University
> Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
> Tel +31 (030) 253-3261 Fax +31 (030) 251-379
> 

RE: first class modules (was: alternative module systems)

[Claudio Russo]

 
> > For the record, your simplification based on identity of signature
> > identifiers
> > is probably ok in practice, but it does
> > rule out some examples that involve package types with free type
> > variables. 
> 
> Right. Would it break something to allow named module type with
> explicit arguments:
> 
> module type 'a ARRAY = sig
>    type array
>    val init: 'a -> array
>    val sub: array -> int -> 'a
>    val update : array -> int -> 'a -> array
> end
> 
> ?
> 
> Then the unification between < (a1,...,ap) S > and < (b1,...,bq) T >
> is solved by equating S = T (syntactically), p=q  and unifying
> a1=b1,...,ap=bp.


I think this would be fine, but you then also have to deal with the
meaning
of these parameterised signatures in other contexts, eg:

functor F(X: ('a -> int) S )= <modexp>;

and so on. Is this declaration illegal or should the functor F be
implicitly polymorphic in 'a?
This is not impossible to deal with, just needs some more work. I
suppose you could only allow
signature applications in core type expressions of the form < sigexp >,
but that seems a little hacky.

-c




> 
> -- 
>   Alain Frisch
> 
> 

RE: first class modules (was: alternative module systems)

[Claudio Russo]

Hi again,

> > a few month ago, Markus Mottl pointed to this mailing list 
> the work by
> > Claudio Russo on first class modules. There were no answer 
> about plans to
> > implement such a system for OCaml.
> 
> Well, it seems like Russo's first-class modules could be added with
> relatively little effort, if there is a sufficient need for them.
> (In OCaml and also in Luc Maranget's Hevea, I can see the need for
> conditionally selecting between several structures having the same
> signature; first-class modules give almost this but not quite.)

Why can't you do this with first-class modules?
In Moscow, you can write (note the somewhat different syntax designed to
co-exist with SML):

structure X as S = if toss_coin() then [structure Foo as S] else
[structure Bar as S];

It's a little redundant, but works.
If you want this to appear as a top-level or nested structure
declaration, then this does rely on 
integrating open with ordinary declarations,  but this is
straightforward.

> > As I see it, the main issue is the unification problem < S 
> > = < T >.
> 
> Right.  The last time we met, I asked Claudio about type inference
> issues for his scheme.  Basically, to "unify" <S> and <T>, you just
> check that the module types S and T are equivalent (using the same
> notion of equivalence that OCaml currently uses to for checking
> compatibility between manifest module type declarations, see 
> the predicate
> Includemod.check_modtype_equiv in the OCaml sources).
> 
> If <S> and <T> contain value components with non-generalized type
> variables, it is necessary to unify them along the way, and Claudio
> alluded to potential traps here.  However, I'm not even sure this can
> happen at all in OCaml since module types cannot contain n-g type vars
> and "pack" requires an explicit module type constraint.

This isn't quite true (unless you don't allow n-g vars in inferred
module types either).
Counter-example:

fun f x = [structure struct val y = x end as sig val y:int end];
> val f = fn : int -> [{val y : int}]

applying the constraint should affect the type of x (which will be a
free var until the 
signature is matched against).

FYI, in Moscow you can even write, 

fun f (x:'a) = [structure struct val y = x end as sig val y:'a end];
> val 'a f = fn : 'a -> [{val y : 'a}]

so that f is polymorphic.
> 
> > (as a side effect, we get the local "open ... in ...")
> 
> I'm not sure I follow you here.  Did you mean that "open" and "pack"
> subsume "let module ... in ..."?  This I agree with.

I think the best approach is the other way around, treating open as
another form of declaration.

Cheers,
Claudio
 
> - Xavier Leroy
> 

RE: first class modules (was: alternative module systems)

[Alain Frisch]

On Mon, 8 Jan 2001, Claudio Russo wrote:

> For the record, your simplification based on identity of signature
> identifiers
> is probably ok in practice, but it does
> rule out some examples that involve package types with free type
> variables. 

Right. Would it break something to allow named module type with
explicit arguments:

module type 'a ARRAY = sig
   type array
   val init: 'a -> array
   val sub: array -> int -> 'a
   val update : array -> int -> 'a -> array
end

?

Then the unification between < (a1,...,ap) S > and < (b1,...,bq) T >
is solved by equating S = T (syntactically), p=q  and unifying
a1=b1,...,ap=bp.


-- 
  Alain Frisch

RE: first class modules (was: alternative module systems)

[Claudio Russo]

Hi,

Thanks for doing the implementation!

For the record, your simplification based on identity of signature
identifiers
is probably ok in practice, but it does
rule out some examples that involve package types with free type
variables. 
For instance, you might want to define a Core type constructor 'a array,
whose definition mentions
the type parameter 'a within a package type:

type  'a = < sig
  type array
  val init: 'a -> array
  val sub: array -> int -> 'a
  val update : array -> int -> 'a -> array
end >

Forcing the expression within < > to be an identifier doesn't let you do
this (because 'a is free).

BTW, in Moscow ML, the "open" construct is integrated more naturally as
a special form of declaration, plus
a side condition that disallows an open declaration from appearing
within the body of a functor (for soundness reasons). This lets you open
first-class modules at top-level and within substructures, which can be
more convenient.

Cheers,
Claudio

PS. If you come up with some more nice examples, I'd love to see them.










Hello,

a few month ago, Markus Mottl pointed to this mailing list the work by
Claudio Russo on first class modules. There were no answer about plans
to
implement such a system for OCaml.

I also have the feeling that there should be no problem to implement
first
class "packaged" modules a la Russo for OCaml. The idea is to keep the
core and module langages distinct but provide bridges between them.
The type algebra is enriched with the syntax  < S >  where S is a module
type.

(pack (m:S))  is a core expression of core type < S > when m is a module
of module type S.

(open a1 as X : S in a2)  has the natural meaning; a1 must have type 
< S >, X is bound in a2 to the module packaged by a1.


As I see it, the main issue is the unification problem < S > = < T >. I
implemented as a quick and dirty hack such a system, where < S > and < T
> unify if and only if S and T represent syntactically the same path. It
is the simpliest solution, but it is general enough (by defining named
module types and putting some explicit coercions). It should be possible
to check that S and T are structurally compatible.


Here is the classical example of arrays of size 2^n:
========================================================================
module type ARRAY = sig
  type 'a array
  val init: 'a -> 'a array
  val sub: 'a array -> int -> 'a
  val update : 'a array -> int -> 'a -> 'a array
end

module ArrayZero = struct
  type 'a array = 'a
  let init x = x
  let sub a i = a
  let update a i x = x
end

module ArraySucc (A:ARRAY) = struct
  type 'a array = 'a A.array * 'a A.array
  let init x = 
    (A.init x, A.init x)
  let sub (l,r) i = 
    if i mod 2 = 0 then A.sub l (i/2) else A.sub r (i/2)
  let update (l,r) i x = 
    if i mod 2 = 0 then (A.update l (i/2) x, r) else (l, A.update r
(i/2)
x)
end

let rec array = function
  | 0 -> pack (ArrayZero:ARRAY)
  | n -> open array (n-1) as A : ARRAY in pack (ArraySucc(A):ARRAY)
========================================================================

The last definition yields as expected:
val array : int ->  < ARRAY > 

It couldn't be expressed without the extension.

Now:
======
let _ =
  open (array 2) as A:ARRAY in
  let a = A.init "hello" in
  let a = A.update a 1 " " in
  let a = A.update a 2 "world" in
  let a = A.update a 3 " !\n" in
  for i = 0 to 3 do print_string (A.sub a i) done
======
builds a module of "array of size 4=2^2" and use it.

Naturally, a type that makes reference to a module value can't escape
the scope where this module is visible:
======
# open (array 3) as A:ARRAY in A.init 5;;
This `let module' expression has type int A.array
In this type, the locally bound module name A escapes its scope
======
(in the first line of the error message, `let module' should read
`open...')


Everything seems to work as expected for higher order modules:
=====================================
module type S = sig type t  val x:t  val y:t  val print:t->unit end
module type T = sig type u  val a:u end
module type F = functor (X:S) -> T with type u = X.t

module TAKE_x(X:S): T with type u = X.t = struct type u = X.t let a =
X.x end
module TAKE_y(X:S): T with type u = X.t = struct type u = X.t let a =
X.y end

module A = struct type t = int let x = 1 and y = 2 and print = print_int
end
module B = struct type t = string let x= "A" and y = "B" and print =
print_string end

let take_x = pack (TAKE_x : F)
let take_y = pack (TAKE_y : F)

let apply f m =
  open f as TAKE : F in
  open m as X : S in
  let module Y = TAKE(X) in
  X.print Y.a

let _ =
  apply take_x (pack (A:S));
  apply take_y (pack (A:S)); print_newline ();
  apply take_x (pack (B:S));
  apply take_y (pack (B:S)); print_newline ();
=====================================

Interesting types are:
val take_x :  < F > 
val take_y :  < F > 
val apply :  < F >  ->  < S >  -> unit


and the execution gives of course:
12
AB

(as a side effect, we get the local "open ... in ...")


Almost everything is already there in OCaml to implement easily this
system. Basically, with trivial extensions of ast, typed ast and type
expressions, for the typing, this gives something like:
(typing/typecore.ml, function type_exp):
....
  | Pexp_pack m ->
      let modl = !type_module env m in
      let ty = newty (Tpackage modl.mod_type) in
      { exp_desc = Texp_pack(modl);
        exp_loc = sexp.pexp_loc;
        exp_type = ty;
        exp_env = env }

  | Pexp_unpack (e1, name, mty, sbody) ->
      let ty = newvar() in
      Ident.set_current_time ty.level;
      let mty = !transl_modtype env mty in
      let arg  = type_expect env e1 (newty (Tpackage mty)) in
      let (id, new_env) = Env.enter_module name mty env in
      Ctype.init_def(Ident.current_time());
      let body = type_exp new_env sbody in
      begin try
        Ctype.unify new_env body.exp_type ty
      with Unify _ ->
        raise(Error(sexp.pexp_loc, Scoping_let_module(name,
body.exp_type)))
      end;
      { exp_desc = Texp_unpack(arg, id, mty, body);
        exp_loc = sexp.pexp_loc;
        exp_type = ty;
        exp_env = env }


for the conversion to lambda-code:
(bytecomp/translcore.ml, function transl_exp)
...
  | Texp_pack modl ->
      !transl_module Tcoerce_none None modl
  | Texp_unpack  (arg,id,mty,body) ->
      Llet(Strict, id, transl_exp arg, transl_exp body)

and something very stupid in typing/ctype.ml for the unification:
    | (Tpackage  (Tmty_ident p1), Tpackage (Tmty_ident p2)) when
Path.same
p1 p2 ->
        update_level env t1.level t2;
        t1.desc <- Tlink t2

I may have overlooked some important consequences on the type safety
properties.

Is there any theoretical work about the integration of such a system to
the OCaml module system ?  Any plan to include it in a future release ?


-- 
  Alain Frisch

Re: first class modules (was: alternative module systems)

[Xavier Leroy]

> a few month ago, Markus Mottl pointed to this mailing list the work by
> Claudio Russo on first class modules. There were no answer about plans to
> implement such a system for OCaml.

Well, it seems like Russo's first-class modules could be added with
relatively little effort, if there is a sufficient need for them.
(In OCaml and also in Luc Maranget's Hevea, I can see the need for
conditionally selecting between several structures having the same
signature; first-class modules give almost this but not quite.)

> As I see it, the main issue is the unification problem < S > = < T >.

Right.  The last time we met, I asked Claudio about type inference
issues for his scheme.  Basically, to "unify" <S> and <T>, you just
check that the module types S and T are equivalent (using the same
notion of equivalence that OCaml currently uses to for checking
compatibility between manifest module type declarations, see the predicate
Includemod.check_modtype_equiv in the OCaml sources).

If <S> and <T> contain value components with non-generalized type
variables, it is necessary to unify them along the way, and Claudio
alluded to potential traps here.  However, I'm not even sure this can
happen at all in OCaml since module types cannot contain n-g type vars
and "pack" requires an explicit module type constraint.

> (as a side effect, we get the local "open ... in ...")

I'm not sure I follow you here.  Did you mean that "open" and "pack"
subsume "let module ... in ..."?  This I agree with.

- Xavier Leroy

Re: first class modules (was: alternative module systems)

[Markus Mottl]

On Sun, 07 Jan 2001, Alain Frisch wrote:
> Is there any theoretical work about the integration of such a system to
> the OCaml module system ?  Any plan to include it in a future release ?

I'd surely appreciate the availability of this new module system in OCaml!

Just as a quick reminder: Moscow ML implements Claudio Russo's module
system with all of its nice features (higher-order and recursive modules;
first-class modules). Here the link:

  http://www.dina.dk/~sestoft/mosml.html

- Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl

first class modules (was: alternative module systems)

[Alain Frisch]

Hello,

a few month ago, Markus Mottl pointed to this mailing list the work by
Claudio Russo on first class modules. There were no answer about plans to
implement such a system for OCaml.

I also have the feeling that there should be no problem to implement first
class "packaged" modules à la Russo for OCaml. The idea is to keep the
core and module langages distinct but provide bridges between them.
The type algebra is enriched with the syntax  < S >  where S is a module
type.

(pack (m:S))  is a core expression of core type < S > when m is a module
of module type S.

(open a1 as X : S in a2)  has the natural meaning; a1 must have type 
< S >, X is bound in a2 to the module packaged by a1.


As I see it, the main issue is the unification problem < S > = < T >. I
implemented as a quick and dirty hack such a system, where < S > and < T
> unify if and only if S and T represent syntactically the same path. It
is the simpliest solution, but it is general enough (by defining named
module types and putting some explicit coercions). It should be possible
to check that S and T are structurally compatible.


Here is the classical example of arrays of size 2^n:
========================================================================
module type ARRAY = sig
  type 'a array
  val init: 'a -> 'a array
  val sub: 'a array -> int -> 'a
  val update : 'a array -> int -> 'a -> 'a array
end

module ArrayZero = struct
  type 'a array = 'a
  let init x = x
  let sub a i = a
  let update a i x = x
end

module ArraySucc (A:ARRAY) = struct
  type 'a array = 'a A.array * 'a A.array
  let init x = 
    (A.init x, A.init x)
  let sub (l,r) i = 
    if i mod 2 = 0 then A.sub l (i/2) else A.sub r (i/2)
  let update (l,r) i x = 
    if i mod 2 = 0 then (A.update l (i/2) x, r) else (l, A.update r (i/2)
x)
end

let rec array = function
  | 0 -> pack (ArrayZero:ARRAY)
  | n -> open array (n-1) as A : ARRAY in pack (ArraySucc(A):ARRAY)
========================================================================

The last definition yields as expected:
val array : int ->  < ARRAY > 

It couldn't be expressed without the extension.

Now:
======
let _ =
  open (array 2) as A:ARRAY in
  let a = A.init "hello" in
  let a = A.update a 1 " " in
  let a = A.update a 2 "world" in
  let a = A.update a 3 " !\n" in
  for i = 0 to 3 do print_string (A.sub a i) done
======
builds a module of "array of size 4=2^2" and use it.

Naturally, a type that makes reference to a module value can't escape
the scope where this module is visible:
======
# open (array 3) as A:ARRAY in A.init 5;;
This `let module' expression has type int A.array
In this type, the locally bound module name A escapes its scope
======
(in the first line of the error message, `let module' should read `open...')


Everything seems to work as expected for higher order modules:
=====================================
module type S = sig type t  val x:t  val y:t  val print:t->unit end
module type T = sig type u  val a:u end
module type F = functor (X:S) -> T with type u = X.t

module TAKE_x(X:S): T with type u = X.t = struct type u = X.t let a = X.x end
module TAKE_y(X:S): T with type u = X.t = struct type u = X.t let a = X.y end

module A = struct type t = int let x = 1 and y = 2 and print = print_int  end
module B = struct type t = string let x= "A" and y = "B" and print = print_string end

let take_x = pack (TAKE_x : F)
let take_y = pack (TAKE_y : F)

let apply f m =
  open f as TAKE : F in
  open m as X : S in
  let module Y = TAKE(X) in
  X.print Y.a

let _ =
  apply take_x (pack (A:S));
  apply take_y (pack (A:S)); print_newline ();
  apply take_x (pack (B:S));
  apply take_y (pack (B:S)); print_newline ();
=====================================

Interesting types are:
val take_x :  < F > 
val take_y :  < F > 
val apply :  < F >  ->  < S >  -> unit


and the execution gives of course:
12
AB

(as a side effect, we get the local "open ... in ...")


Almost everything is already there in OCaml to implement easily this
system. Basically, with trivial extensions of ast, typed ast and type
expressions, for the typing, this gives something like:
(typing/typecore.ml, function type_exp):
....
  | Pexp_pack m ->
      let modl = !type_module env m in
      let ty = newty (Tpackage modl.mod_type) in
      { exp_desc = Texp_pack(modl);
        exp_loc = sexp.pexp_loc;
        exp_type = ty;
        exp_env = env }

  | Pexp_unpack (e1, name, mty, sbody) ->
      let ty = newvar() in
      Ident.set_current_time ty.level;
      let mty = !transl_modtype env mty in
      let arg  = type_expect env e1 (newty (Tpackage mty)) in
      let (id, new_env) = Env.enter_module name mty env in
      Ctype.init_def(Ident.current_time());
      let body = type_exp new_env sbody in
      begin try
        Ctype.unify new_env body.exp_type ty
      with Unify _ ->
        raise(Error(sexp.pexp_loc, Scoping_let_module(name, body.exp_type)))
      end;
      { exp_desc = Texp_unpack(arg, id, mty, body);
        exp_loc = sexp.pexp_loc;
        exp_type = ty;
        exp_env = env }


for the conversion to lambda-code:
(bytecomp/translcore.ml, function transl_exp)
...
  | Texp_pack modl ->
      !transl_module Tcoerce_none None modl
  | Texp_unpack  (arg,id,mty,body) ->
      Llet(Strict, id, transl_exp arg, transl_exp body)

and something very stupid in typing/ctype.ml for the unification:
    | (Tpackage  (Tmty_ident p1), Tpackage (Tmty_ident p2)) when Path.same
p1 p2 ->
        update_level env t1.level t2;
        t1.desc <- Tlink t2

I may have overlooked some important consequences on the type safety
properties.

Is there any theoretical work about the integration of such a system to
the OCaml module system ?  Any plan to include it in a future release ?


-- 
  Alain Frisch