Renaming structures during inclusions?

Renaming structures during inclusions?

[Markus Mottl]

Hi,

I have run into a problem using the "include"-keyword for including
module definitions in other modules. E.g.:

----------------------------------------------
module M1 = struct
  type t
  module Std = struct end
end

module M2 = struct
  type t
  module Std = struct end
end

module M = struct
  include M1
  include M2
end
----------------------------------------------

The above is not possible, because the names for type t in M1 and M2,
and the module names for module Std clash. Though it would not lead to
any kind of unsoundness to allow this, it would make referring to
shadowed types or modules impossible, both for the user and also for
the compiler in error messages.

The only solution that seems to make sense and does not impose
excessive work on the user is, IMHO, to provide for a facility to
rename types and modules, e.g. maybe something like:

----------------------------------------------
module M = struct
  include M1
    with type t as m1_t
    with module Std as M1Std

  include M2
    with type t as m2_t
    with module Std as M2Std

  module Std = struct
    include M1Std
    include M2Std
  end
end
----------------------------------------------

In the above example I also added a new Std-module that includes the
contents of the two old ones.

The only current way to get something similar right now is to
explicitly create new bindings for all entities in the modules to be
included, which may be an enormous amount of work depending on their
size.

What do the developers think? Would it be a good idea to add a
renaming facility to the language (it wouldn't even require any new
keywords)?

Best regards,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

Re: [Caml-list] Renaming structures during inclusions?

[Christophe TROESTLER]

On Wed, 11 May 2005, Markus Mottl <markus.mottl@gmail.com> wrote:
> 
> The above is not possible, because the names for type t in M1 and M2,
> and the module names for module Std clash.

Wouldn't it be better to have a compiler switch (say "-w T/t", off by
default) to overide that behavior (new definitions override old ones
as with [open])?  Of course that makes it impossible to write M1
signature without aliasing [t] and [Std] but IMHO that's fine.  This
way, no new syntax needs to be introduced (and one is not forced to
alias modules one does not care about -- e.g. utilities).

module M = struct
  include M1
  type m1_t = M1.t
  module M1Std = M1.Std

  include M2
  type m2_t = M2.t
  module M2Std = M2.Std

  module Std = struct
    include M1.Std
    include M2.Std
  end
end

My 2¢,
ChriS

Re: [Caml-list] Renaming structures during inclusions?

[Andreas Rossberg]

Christophe TROESTLER wrote:
> 
> Wouldn't it be better to have a compiler switch (say "-w T/t", off by
> default) to overide that behavior (new definitions override old ones
> as with [open])?  Of course that makes it impossible to write M1
> signature without aliasing [t] and [Std] but IMHO that's fine.

Note that OCaml's type system fundamentally relies on the fact that type 
names cannot be shadowed in structures.

> This
> way, no new syntax needs to be introduced (and one is not forced to
> alias modules one does not care about -- e.g. utilities).
> 
> module M = struct
>   include M1
>   type m1_t = M1.t
>   module M1Std = M1.Std
> 
>   include M2
>   type m2_t = M2.t
>   module M2Std = M2.Std
> 
>   module Std = struct
>     include M1.Std
>     include M2.Std
>   end
> end

While your proposal probably could be made to work in this particular 
case - the compiler had to figure out that it can break the dependency 
on the first t by reordering m1_t relative to the fields from M1 in the 
derived signature and substituting m1_t for t in these fields, likewise 
for the other elements - it is *far* from obvious if and how this can be 
inferred in general, particularly when your modules go higher-order.

I believe it would require something akin to join and meet operations on 
signatures, but it is known that these don't exist for some very similar 
systems (signatures for higher-order modules don't form a lattice).

Cheers,

   - Andreas

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

Let's get rid of those possible thingies!  -- TB

Re: [Caml-list] Renaming structures during inclusions?

[Markus Mottl]

On 5/11/05, Andreas Rossberg <rossberg@ps.uni-sb.de> wrote:
> Note that OCaml's type system fundamentally relies on the fact that type
> names cannot be shadowed in structures.

Hm, I don't see why this should be so, can you elaborate? I don't know
the compiler internals about type inference, this seems like a
question of how types are identified internally. I make the reasonable
guess that it is not by names (strings) but some kind of integer id or
similar. So "type t type t" could internally still be kept apart,
though producing error messages is a problem (would require printing
of extra tags), and the user could not refer to the shadowed type
anymore. That's why I wouldn't want the compiler to accept this code,
which is the current behaviour anyway.

> While your proposal probably could be made to work in this particular
> case - the compiler had to figure out that it can break the dependency
> on the first t by reordering m1_t relative to the fields from M1 in the
> derived signature and substituting m1_t for t in these fields, likewise
> for the other elements - it is *far* from obvious if and how this can be
> inferred in general, particularly when your modules go higher-order.

Maybe I don't see the problem, but since I feel confident that I can
always solve this problem manually in a fairly mechanized and
straightforward way, I'd be surprised if this couldn't be done by the
compiler. Isn't it just a normal alpha conversion problem? The only
thing that needs to be guaranteed by the compiler is that there is no
name capture, but that, too, isn't difficult to do.

Regards,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

Re: [Caml-list] Renaming structures during inclusions?

[Christophe TROESTLER]

On Wed, 11 May 2005, Andreas Rossberg <rossberg@ps.uni-sb.de> wrote:
> 
> Note that OCaml's type system fundamentally relies on the fact that
> type names cannot be shadowed in structures.

Yes, you are correct -- I was thinking of checking the sig against a
given one, not to generate it.

> the compiler had to figure out that it can break the dependency on
> the first t by reordering m1_t relative to the fields from M1 in the
> derived signature and substituting m1_t for t in these fields, [...]
> it is *far* from obvious if and how this can be inferred in general,
> particularly when your modules go higher-order.
> 
> I believe it would require something akin to join and meet operations on 
> signatures, but it is known that these don't exist for some very similar 
> systems (signatures for higher-order modules don't form a lattice).

The substitution in itself is nothing difficult, isn't it.  Or is it
because you need to "backtrack" to change the inferred sigs?  Is the
problem when to do it?  Do you have examples?  I do not immediately
see why a rule like "duplicate types/modules are forbidden in a sig
unless one of them is explicitely renamed" would be difficult to check[1].

On the other hand, one may also argue that Markus proposal is cleaner.

Regards,
ChriS


[1] E.g. -- the simpler -- when the shadowing occurs (this is already
detected), an alternative name for the type must be available.

Re: [Caml-list] Renaming structures during inclusions?

[Jacques Garrigue]

Well, somebody already worked out a real solution to this problem, at
least at the signature level:
   http://www.eecs.harvard.edu/~nr/pubs/els-abstract.html

The point is that once you have solved the signature level problem,
you can solve the module level problem: you just have to duplicate your
binding under a new name, and hide the old one with a signature
where the type is renamed. You could have syntactic sugar for that,
but the semantics is clear.

So my take on this problem is that the above proposal, or something
equivalent, should be included in the language.

Jacques Garrigue

From: Markus Mottl <markus.mottl@gmail.com>

> I have run into a problem using the "include"-keyword for including
> module definitions in other modules. E.g.:
> 
> ----------------------------------------------
> module M1 = struct
>   type t
>   module Std = struct end
> end
> 
> module M2 = struct
>   type t
>   module Std = struct end
> end
> 
> module M = struct
>   include M1
>   include M2
> end
> ----------------------------------------------
> 
> The above is not possible, because the names for type t in M1 and M2,
> and the module names for module Std clash. Though it would not lead to
> any kind of unsoundness to allow this, it would make referring to
> shadowed types or modules impossible, both for the user and also for
> the compiler in error messages.
> 
> The only solution that seems to make sense and does not impose
> excessive work on the user is, IMHO, to provide for a facility to
> rename types and modules, e.g. maybe something like:
> 
> ----------------------------------------------
> module M = struct
>   include M1
>     with type t as m1_t
>     with module Std as M1Std
> 
>   include M2
>     with type t as m2_t
>     with module Std as M2Std
> 
>   module Std = struct
>     include M1Std
>     include M2Std
>   end
> end
> ----------------------------------------------
> 
> In the above example I also added a new Std-module that includes the
> contents of the two old ones.
> 
> The only current way to get something similar right now is to
> explicitly create new bindings for all entities in the modules to be
> included, which may be an enormous amount of work depending on their
> size.
> 
> What do the developers think? Would it be a good idea to add a
> renaming facility to the language (it wouldn't even require any new
> keywords)?
> 
> Best regards,
> Markus
> 
> -- 
> Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

Re: [Caml-list] Renaming structures during inclusions?

[Andreas Rossberg]

Markus Mottl wrote:
 >
 >> Note that OCaml's type system fundamentally relies on the fact that
 >> type names cannot be shadowed in structures.
 >
 > Hm, I don't see why this should be so, can you elaborate? I don't know
 > the compiler internals about type inference, this seems like a
 > question of how types are identified internally. I make the reasonable
 > guess that it is not by names (strings) but some kind of integer id or
 > similar.

It's by paths like A.B.C, in which only A is an alpha-convertible 
identifier, the rest are labels. Now consider:

   module X =
   struct
     type t = C
     let x = C
     type t = int
   end

How would you express the type of X.x? There is no label that allows 
projecting the shadowed t.

Sure there are ways to solve this (SML allows the above, for example), 
but most likely they require deviating from, or at least extending the 
theory underlying OCaml modules at the moment (and are likely to be not 
as nice).

 > Maybe I don't see the problem, but since I feel confident that I can
 > always solve this problem manually in a fairly mechanized and
 > straightforward way, I'd be surprised if this couldn't be done by the
 > compiler. Isn't it just a normal alpha conversion problem?

Christophe TROESTLER wrote:
 >
 > The substitution in itself is nothing difficult, isn't it.  Or is it
 > because you need to "backtrack" to change the inferred sigs?  Is the
 > problem when to do it?  Do you have examples?  I do not immediately
 > see why a rule like "duplicate types/modules are forbidden in a sig
 > unless one of them is explicitely renamed" would be difficult to 
check[1].

The first problem is that this construction is a special case - you 
write a signature and it contains occurrences of shadowing. In general 
shadowed items cannot just be forgotten (see the example above), so how 
do you characterise this special case? How can the type checker 
recognise it? It would probably be pretty ad-hoc.

The obstacles are the dependencies within a signature, which prohibit 
arbitrary reordering, and the inability to alpha-rename labels. An 
algorithm that covers all possible cases where a type or module name can 
be forgotten is non-obvious (probably as difficult as identifying these 
cases in the first place). I don't think it's easily doable within the 
current theoretical framework.

Jacques pointed to a paper that seems to be solving this problem, but it 
is using an entirely different framework (and quite a baroque one, I 
have to add). Not all signatures in this framework are translatable back 
to OCaml's, e.g. they can contain mutually dependent substructures.

However, if we just want renaming, and it is explicit, then everything 
should be pretty straightforward.

 > Yes, you are correct -- I was thinking of checking the sig against a
 > given one, not to generate it.

But as is, this isn't a valid sig, so you cannot match it against 
another one.

Cheers,

   - Andreas

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

Let's get rid of those possible thingies!  -- TB

Re: [Caml-list] Renaming structures during inclusions?

[Norman Ramsey]

 > [example] is not possible, because the names for type t in M1 and M2,
 > and the module names for module Std clash...
 >
 > The only solution that seems to make sense and does not impose
 > excessive work on the user is, IMHO, to provide for a facility to
 > rename types and modules...

Kathleen Fisher and Paul Govereau and I have been working out a
detailed proposal, but operating primarily on signatures, not
structures:

  http://www.eecs.harvard.edu/~nr/pubs/els-abstract.html

In some cases (such as renaming to avoid collisions), these operations
extend nicely to the structure level.  But in others, particularly
meet and join, extension to structures is not obvious.  

We would certainly be very interested in hearing from Caml programmers
whether you think our proposed extensions meet your needs.


Norman

P.S. We've made no effort to avoid introducing new syntax---at the
present stage, we are most interested in coming up with a good design
for ML-like module systems.  Figuring out how to fit the design into
an existing language with minimal disruption is a separate question.

[Caml-list] Renaming structures during inclusions?

[Markus Mottl]

On 5/11/05, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:
> Well, somebody already worked out a real solution to this problem, at
> least at the signature level:
>    http://www.eecs.harvard.edu/~nr/pubs/els-abstract.html

Thanks for the link, this looks like a very interesting proposal.

> The point is that once you have solved the signature level problem,
> you can solve the module level problem: you just have to duplicate your
> binding under a new name, and hide the old one with a signature
> where the type is renamed. You could have syntactic sugar for that,
> but the semantics is clear.

Right, the operations on signatures and modules do not seem to be
fundamentally different in nature.

> So my take on this problem is that the above proposal, or something
> equivalent, should be included in the language.

I fully agree. We work on some fairly large projects here that have
grown to many hundreds of modules written by different people and
often having somewhat more complicated dependencies. This sometimes
makes it difficult to express certain relationships between modules
without jumping through hoops.

Even though I think that OCaml supports "programming in the large" way
better than any other language I know, it would surely benefit from
some more improvements to the module language.  Since module systems
is one of Xavier's favourite research topics, I wonder what his point
of view is.  Any chance that we will see an even more expressive
module language in OCaml in the forseeable future?

Best regards,
Markus

--
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

Re: [Caml-list] Renaming structures during inclusions?

[Aleksey Nogin]

On 11.05.2005 08:44, Markus Mottl wrote:

> The only solution that seems to make sense and does not impose
> excessive work on the user is, IMHO, to provide for a facility to
> rename types and modules, e.g. maybe something like:
> 
> ----------------------------------------------
> module M = struct
>   include M1
>     with type t as m1_t
>     with module Std as M1Std
> 
>   include M2
>     with type t as m2_t
>     with module Std as M2Std
> 
>   module Std = struct
>     include M1Std
>     include M2Std
>   end
> end
> ----------------------------------------------

I would like to second this request. Currently, including several 
modules that share some structure is impossible and requires giving 
separate names for all the shared fields, with can be very painful. The 
"with" renaming seems simple enough and AFAICT would not break anything.

-- 
Aleksey Nogin

Home Page: http://nogin.org/
E-Mail: nogin@cs.caltech.edu (office), aleksey@nogin.org (personal)
Office: Moore 04, tel: (626) 395-2200