[Caml-list] functors and modules (was "What is an applicative functor?")

[Caml-list] functors and modules (was "What is an applicative functor?")

[Lucas Dixon]

> -------- Original Message --------
> Subject: Re: [Caml-list] What is an applicative functor?
> Date: Tue, 19 Apr 2011 16:04:50 +0200
> From: Andreas Rossberg <rossberg@mpi-sws.org>
> To: Lucas Dixon <ldixon@inf.ed.ac.uk>
> CC: caml-list@inria.fr
>
> On Apr 15, 2011, at 05.08 h, Lucas Dixon wrote:
>>
>> On 13/04/2011 03:23, Andreas Rossberg wrote:
>>>
>>> My experience with the early MLKit, which used this so-called "closed
>>> functor style", was that it is horrible. You need lots of functor
>>> parameters, lots of structure nesting and reexporting (the sizes of
>>> signatures can grow exponentially!),  and plenty of subtle sharing
>>> constraints.
>>
>> My feeling was that a little improvement on the syntax of signatures
>> and sharing would deal with these issues fairly easily.
>
> I think this is very much a semantic problem, but I still would be
> interested to hear what improvements you have in mind.

1. I think you want to have a reasonable language to modify signatures
- one that has all the obvious set-stuff, e.g. remove/add etc.
(basically following the paper on an expressive language for
signatures).

2. the resulting signature of a Functor should be able to refer to the
input signatures. This would allow multiple inheritance in a natural
way:   functor S2(S1) : S1 + sig val f : S1.t -> int end;

3. implicit signature dependencies:
let S1 : SIG1 ... in
functor F1(S2) = ...
functor F2(S3) = ...
end;
=
functor F1(S1 and S2) = ...
functor F2(S1 and S3) = ...

4. sharing of structures should allow be fine-grained modification,
and should have sensible syntax (it's not a symmetric operation, so
don't use a symmetric syntax: use <= instead of =):
e.g..
sharing (S1 except S1.t) <= S2
Also when types are ground, if they are the same, then it shouldn't complain.
If you fix these things, signature sharing is pretty easy.

Once you do this, I think you also want to have a way to canonically
name structures in error messages. e.g. never say "S1.t is not equal
to S1.t: this was a common problem in PolyML until fairly recently."

>> In terms of growing exponentially: that sounds like a serious
>> problem; I would expect it to grow linearly on the number of
>> dependencies. Or did you mean to use exponentially informally; as in
>> gets too bug too quick?
>
> No, I meant it literally. One common idiom with functors is to re-
> export all parameter structures in the result, in order to have a self-
> contained result signature (and ease sharing later on). When you
> continue doing that up the entire dependency graph, then signatures
> can grow exponentially (in the depth of the dependency chain).

While the number of paths to the sub-structures is exponential, the
number of actual signatures is not. If the implementation does a
reasonable job at only storing one copy when they are shared, then I
don't think this is a problem.

I think it is a problem if people don't specify their dependencies
correctly, and the language should make it easy. Providing
sub-structures to hold everything is not a good idea. So in some sense
I agree: we need the right syntax for expressing what our
dependencies.

>>> And when some new code you're writing does not type check,
>>> you sometimes spend considerable time figuring out whether that was a
>>> "real" error or you just forgot some type sharing somewhere.
>>
>> I ended up pushing improvements to the type-error printing which
>> helped a lot in PolyML. That combined with a finding a style that
>> works out not too hideously: I create a sub-structure, typically
>> called "Sharing" to hold just types that are relevant to a
>> particular module. I can then use sharing on this substructure to
>> share all types and save the others painful problem to remember to
>> share every type.
>
> Sure, such idioms can help, but I don't think they solve the general
> problem. The more dependencies you have (e.g. in some more top-level
> module) the more unstructured their relations become, and it is
> difficult to organize them in a useful way.

I think you want a reasonable language for specifying dependencies,
and actually I think functors, with some tweaks to the signature
language, would be pretty good. I can't see any better than saying
what you need and what you provide, which is essentially all that a
functor does. The main complication is name-space management. But,
like I suggest above, I think that a sensible signature language could
deal with that.

> In a way, parameterizing out all imports is a kind of manual closure
> conversion. You wouldn't want to be forced to doing that in the small,
> and I don't see why you should in the large. I feel that it also
> exposes too much of what should be considered implementation details.

I'm not sure I understand... I guess you mean you want concise syntax
that lets you say you depend on more than you really do? And then
maybe you work out the details of what you really depend on later.
Course-grained dependencies? I think functors kind of do that...
imagine a structure is an import, you specify the structures you use,
although maybe they contain much more than you really do use. You can
automatically analyse what you don't use of course...

>> yes, the concept of module for SML is really a functor and
>> dependencies are explicit.
>
> I guess the underlying question is what constitutes a module? I think
> you have to distinguish modules (as individual abstractions) from
> components/libraries/packages/whatever you like to call them. The
> latter can consist of many modules.

I don't see why they need to be separate... I think structures can be
individual modules as well as packages.

> In that spectrum, there is a place
> for both definite and indefinite references to other modules. You
> often want the the latter when you cross boundaries to other
> libraries. But the current functor mechanism is not an adequate means
> for expressing them, because it cannot be used at that level.

I still think it almost is... :-P

Maybe we need to sketch a bit more of a detailed picture of what we
want... maybe you have some examples, analogies to other languages we
can flesh out a bit more? I suspect that your idea of indefinite
references is something like (3) of my suggestions above... is that
the kind of thing you were thinking of?

... I'd like to imagine what the most beautiful way to write things
would be, and then infer the logic behind it :)

best,
lucas

[Caml-list] Re: functors and modules (was "What is an applicative functor?")

[Andreas Rossberg]

On Apr 28, 2011, at 07:06, Lucas Dixon wrote:
> 1. I think you want to have a reasonable language to modify signatures
> - one that has all the obvious set-stuff, e.g. remove/add etc.
> (basically following the paper on an expressive language for
> signatures).

Agreed.

> 2. the resulting signature of a Functor should be able to refer to the
> input signatures. This would allow multiple inheritance in a natural
> way:   functor S2(S1) : S1 + sig val f : S1.t -> int end;

I don't understand. Is S1 a signature or structure here? In the former  
case, how is this different from:

   functor S2(X : S1) : sig include S1 val f : X.t -> int end

In the latter case, how is it different from saying (in OCaml 3.12):

   module S2(S1 : SIG) : sig include module type of S1 val f : S1.t ->  
int end

Granted, it would be much nicer with mixin composition. ;)

> 3. implicit signature dependencies:
> let S1 : SIG1 ... in
> functor F1(S2) = ...
> functor F2(S3) = ...
> end;
> =
> functor F1(S1 and S2) = ...
> functor F2(S1 and S3) = ...

Again, I don't understand what universes your Si are in, nor what you  
mean by "implicit signature dependency" or the "and" keyword. Assuming  
the Si are module identifiers, then isn't that just a nested functor?

   functor F (S1 : SIG1) =
   struct
     functor F1 (S2 : SIG2) = ...
     functor F2 (S3 : SIG3) = ...
   end

which in this case is isomorphic to the use of currying:

     functor F1 (S1 : SIG1) (S2 : SIG2) = ...
     functor F2 (S1 : SIG1) (S3 : SIG3) = ...

All this can be done in OCaml and in several SML implementations.

> 4. sharing of structures should allow be fine-grained modification,
> and should have sensible syntax (it's not a symmetric operation, so
> don't use a symmetric syntax: use <= instead of =):
> e.g..
> sharing (S1 except S1.t) <= S2

Sharing constraints a la SML are an anachronism. You simply want  
transparent (aka manifest) module specifications. E.g. in OCaml (or  
similarly in some SML dialects):

   sig
     ...
     module S1 = S2
     ...
   end

or

   S with module S1 = S2

Not sure what you intend with the "except", though.

> Also when types are ground, if they are the same, then it shouldn't  
> complain.

Yes, don't use structure sharing in SML. Ever. It was merely a  
backwards compatibility device for SML'90 code.

>> No, I meant it literally. One common idiom with functors is to re-
>> export all parameter structures in the result, in order to have a  
>> self-
>> contained result signature (and ease sharing later on). When you
>> continue doing that up the entire dependency graph, then signatures
>> can grow exponentially (in the depth of the dependency chain).
>
> While the number of paths to the sub-structures is exponential, the
> number of actual signatures is not. If the implementation does a
> reasonable job at only storing one copy when they are shared, then I
> don't think this is a problem.

The size of a signature includes nested ones. You still have to do all  
the signature matching on the full thing, which is structural and  
involves varying instantiations, so you cannot generally "cache" it.

> I think it is a problem if people don't specify their dependencies
> correctly, and the language should make it easy. Providing
> sub-structures to hold everything is not a good idea. So in some sense
> I agree: we need the right syntax for expressing what our
> dependencies.

The alternative to nesting the full structures is just flattening out  
their relevant type members. That makes the overall signature smaller,  
and is indeed the style used in most ML functor code today. But now it  
is just the number of direct type members that grows exponentially (at  
least in the worst case), which tends to be even more annoying to  
write down (although I could imagine you often can use some idiom of  
packaging them up in a single substructure that you can then include,  
but that still is kind of unpleasant).

> I think you want a reasonable language for specifying dependencies,
> and actually I think functors, with some tweaks to the signature
> language, would be pretty good. I can't see any better than saying
> what you need and what you provide, which is essentially all that a
> functor does.

Well, there is a difference between referring to a concrete module you  
need, just by name (a definite reference) or abstracting over the  
concrete module, by giving its complete interface specification (an  
indefinite reference). I'm just saying you want both, scoping and  
functorisation, depending on whether the modules are in the same  
"package" or not. Always having to give the full signature spec is  
just way too inconvenient.

>> I guess the underlying question is what constitutes a module? I think
>> you have to distinguish modules (as individual abstractions) from
>> components/libraries/packages/whatever you like to call them. The
>> latter can consist of many modules.
>
> I don't see why they need to be separate... I think structures can be
> individual modules as well as packages.

A package is typically too large to be written in one source file. So  
you want to split it into several modules without having to functorise  
everything by everything. OTOH, you actually want to functorise the  
whole thing in the end, and that is something you cannot do with the  
language as is. (OCaml provides some extra-linguistic means to do the  
former, via the compiler's -pack option, but nothing for the latter.)

Cheers,
/Andreas

[Caml-list] Re: functors and modules (was "What is an applicative functor?")

[Lucas Dixon]

On 29 April 2011 09:09, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
>> 2. the resulting signature of a Functor should be able to refer to the
>> input signatures. This would allow multiple inheritance in a natural
>> way:   functor S2(S1) : S1 + sig val f : S1.t -> int end;
>
> I don't understand. Is S1 a signature or structure here?

I'm sorry! that was a terribly formatted, late night confusion of a
sketch of my thoughts, lets see if I can clean up this poor
presentations...

Here's a better presentation of the idea:
http://informallyabstract.blogspot.com/2011/04/typed-signature-variables-for.html

> In the former case,
> how is this different from:
>
>  functor S2(X : S1) : sig include S1 val f : X.t -> int end
>
> In the latter case, how is it different from saying (in OCaml 3.12):
>
>  module S2(S1 : SIG) : sig include module type of S1 val f : S1.t -> int end
>
> Granted, it would be much nicer with mixin composition. ;)

I'd like to treat S1 as a signature variable... see blog post linked above.

>> 3. implicit signature dependencies:
>> let S1 : SIG1 ... in
>> functor F1(S2) = ...
>> functor F2(S3) = ...
>> end;
>> =
>> functor F1(S1 and S2) = ...
>> functor F2(S1 and S3) = ...
>
> Again, I don't understand what universes your Si are in, nor what you mean
> by "implicit signature dependency" or the "and" keyword. Assuming the Si are
> module identifiers, then isn't that just a nested functor?
>
>  functor F (S1 : SIG1) =
>  struct
>    functor F1 (S2 : SIG2) = ...
>    functor F2 (S3 : SIG3) = ...
>  end
>
> which in this case is isomorphic to the use of currying:
>
>    functor F1 (S1 : SIG1) (S2 : SIG2) = ...
>    functor F2 (S1 : SIG1) (S3 : SIG3) = ...
>
> All this can be done in OCaml and in several SML implementations.

again, sorry for confusion. Yes it's a syntax like:

functor F (S1 : SIG1) =
struct
  functor F1 (S2 : SIG2) = ...
  functor F2 (S3 : SIG3) = ...
end

which is useful, but, as you note, doesn't change semantics at all.
The thing is that I'd like to be able to include files within to to
push for more flexibility in the way we consider context. e.g.

functor F (S1 : SIG1) =
struct
  use "submodule1.ML";
  use "submodule2.ML";
end;

A little thought is needed here, but it seems reasonable... I think. :)

>> 4. sharing of structures should allow be fine-grained modification,
>> and should have sensible syntax (it's not a symmetric operation, so
>> don't use a symmetric syntax: use <= instead of =):
>> e.g..
>> sharing (S1 except S1.t) <= S2
>
> Sharing constraints a la SML are an anachronism. You simply want transparent
> (aka manifest) module specifications. E.g. in OCaml (or similarly in some
> SML dialects):
>
>  sig
>    ...
>    module S1 = S2
>    ...
>  end
>
> or
>
>  S with module S1 = S2
>
> Not sure what you intend with the "except", though.

I actually think that sharing is a good idea, but it has confused
syntax. Categorically, I think the idea is to provide a syntax for
pushouts, which is a naturally compositional construction; exactly
what I think one wants for module system. When you depend on two
things, and they can have different kinds of overlaps, then you should
be able to say *how* they overlap. This is what sharing is doing, and
I think it's the right idea...

Maybe if we sketch out an example it becomes clearer...

Lets imagine defining a module that depends on two kinds of mapping
structures, both instances of MAP, as defined by something like this:

signature MAP =
sig
  type key
  type value
  type map
  ...
and

e.g. you have:
functor  new_module(
  Map1 : MAP
  Map2 : MAP
) : ...
= struct ...

then there are lots of ways which these maps may be related.
perhaps Map1.key = Map2.key, perhaps Map2.key = Map1.value, etc. I
think that the dependencies of module should be a well-defined
signature, and the question is how to express this elegantly. The idea
being that we want to be able to check at compile time if the
composition of modules will work. I want a lightweight syntax for
this, and tools support also (e.g. signature inference for modules, so
you don't have to type it out). I do think you want explicit syntax
for it, because this lets different people implement stuff
independently. It makes code, and code development compositional...
this is a nice theory, but do you also think it's a good idea? I've
sometimes wondered about the need for all this explicitness, generally
I do think it's good, as long as you can find short, easy syntax....

anyway, the idea of "except" is just to extend the expressive language
of signatures to sharing.  It's just a syntactic mechanism to express
exactly what is shared. Except lets you removing some stuff from a
structure that you want to express is shared...

e.g. writing
  sharing (Map1 except map) <= Map2
is the same as
  sharing Map1.key = Map2.key
  sharing Map1.value = Map2.value
i.e. the keys and values are the same, but the data structure
implementing the maps is different. The idea is that set-like
expressions are a convenient way to say exactly what is shared.

>> Also when types are ground, if they are the same, then it shouldn't
>> complain.
>
> It was merely a backwards
> compatibility device for SML'90 code.

Indeed.

> Yes, don't use structure sharing in SML. Ever.

haha, but I do! :)

but seriously, I like being able to say how my module inputs are
related. I like SML functors and sharing. I just don't like the
impoverished syntax I have to write it with.

Maybe it's all been sorted out already, and we're just disagreeing on
what to call it. I remember reading some of your module papers and
thinking most of the problems have been solved, and we should just
implement it in ML. So hopefully I'm not just (re)sketching stuff
you've already done...

>>> No, I meant it literally. One common idiom with functors is to re-
>>> export all parameter structures in the result, in order to have a self-
>>> contained result signature (and ease sharing later on). When you
>>> continue doing that up the entire dependency graph, then signatures
>>> can grow exponentially (in the depth of the dependency chain).
>>
>> While the number of paths to the sub-structures is exponential, the
>> number of actual signatures is not. If the implementation does a
>> reasonable job at only storing one copy when they are shared, then I
>> don't think this is a problem.
>
> The size of a signature includes nested ones. You still have to do all the
> signature matching on the full thing, which is structural and involves
> varying instantiations, so you cannot generally "cache" it.

OK, I think I see what you mean; lets take a slightly concrete example:

MAP = {  ... }
SIG2A = { Map : SIG1 ... }
SIG2B = { Map : SIG1 ... }

SIG3A = { S2a : SIG2A;  S2b : SIG2B; sharing S2a.Map = S2b.Map; ... }
SIG3B = { S2a : SIG2A;  S2b : SIG2B; sharing S2a.Mao = S2b.Map; ... }

SIG4 = { S3a : SIG3A; S3b : SIG3B; sharing S3a.S2a.Map = S3b.S2a.Map; ... }

Note that SIG4 has 4 paths to MAP, they must all have same types.

So now if we let F5(S4 : SIG4) be a functor taking an instance of a
SIG4, then we need to check all four paths to Map are implementing the
same MAP. Hence the number of checks is exponential.

Caching can help in terms of avoiding detailed checks for each case,
but there are still an exponentially number of cases. I think I agree
with this.

But! I think a better language for expressing signatures can easily fix this.
e.g. we should be able to write:

MAP = {  ... }
SIG2A = { Map : SIG1 ... }
SIG2B = { Map : SIG1 ... }
SIG3A = {
  Map : MAP;
  S2a : SIG2A where S2a.Map := Map;
  S2b : SIG2B where S2a.Map := Map;
  ... }

Having structure/signature level substitutions seems to naturally fix
this: you now check a single Map at the top level, and modify all
types in S2a to refer to those in the parent structure. This also
cleans up the many occurrences of the same structure: I'm assuming
that S2a.Map no longer exists after you write S2a.Map := ..., instead
just have the single top-level Map. Maybe ":=" is not the best
syntax... but I think you get the idea.

>> I think it is a problem if people don't specify their dependencies
>> correctly, and the language should make it easy. Providing
>> sub-structures to hold everything is not a good idea. So in some sense
>> I agree: we need the right syntax for expressing what our
>> dependencies.
>
> The alternative to nesting the full structures is just flattening out their
> relevant type members. That makes the overall signature smaller, and is
> indeed the style used in most ML functor code today. But now it is just the
> number of direct type members that grows exponentially (at least in the
> worst case), which tends to be even more annoying to write down (although I
> could imagine you often can use some idiom of packaging them up in a single
> substructure that you can then include, but that still is kind of
> unpleasant).

I think you can have an explicit, but still convenient syntax for
structure sharing/substitutions... what do you think of the suggestion
above?

>> I think you want a reasonable language for specifying dependencies,
>> and actually I think functors, with some tweaks to the signature
>> language, would be pretty good. I can't see any better than saying
>> what you need and what you provide, which is essentially all that a
>> functor does.
>
> Well, there is a difference between referring to a concrete module you need,
> just by name (a definite reference) or abstracting over the concrete module,
> by giving its complete interface specification (an indefinite reference).
> I'm just saying you want both, scoping and functorisation, depending on
> whether the modules are in the same "package" or not. Always having to give
> the full signature spec is just way too inconvenient.

But when you specify a signature, you don't have to specify everything
it has, only a super-set of what you use, I can't see how you could
get away with less and maintain checking of module compositions...
actually I'm not sure I'm understanding this point, maybe you can
expand on it a bit?

>>> I guess the underlying question is what constitutes a module? I think
>>> you have to distinguish modules (as individual abstractions) from
>>> components/libraries/packages/whatever you like to call them. The
>>> latter can consist of many modules.
>>
>> I don't see why they need to be separate... I think structures can be
>> individual modules as well as packages.
>
> A package is typically too large to be written in one source file. So you
> want to split it into several modules without having to functorise
> everything by everything. OTOH, you actually want to functorise the whole
> thing in the end, and that is something you cannot do with the language as
> is. (OCaml provides some extra-linguistic means to do the former, via the
> compiler's -pack option, but nothing for the latter.)

Yes, I agree. File structure should be flexible, and at the same time,
reflect the structure of the code. I think the deeper problem here is
that we treat file-systems as trees, when what you want is a graph.
File systems are of course really DAGs, so maybe every directory
should be a module. And within every module directory, you have a
"deps" directory with sym-links to modules it depends on. Now you'll
want some tools for visualizing and developing this, but that's not
hard... Now you can have the module structure of your code broken up
into files and/or directories, as you feel is appropriate... or
perhaps we could take the idea of being able to write "use" within a
functor definition?

best,
lucas

[Caml-list] Re: functors and modules (was "What is an applicative functor?")

[Andreas Rossberg]

On May 1, 2011, at 00.19 h, Lucas Dixon wrote:
>>> 2. the resulting signature of a Functor should be able to refer to  
>>> the
>>> input signatures. This would allow multiple inheritance in a natural
>>> way:   functor S2(S1) : S1 + sig val f : S1.t -> int end;
>>
>> I don't understand. Is S1 a signature or structure here?
>
> I'm sorry! that was a terribly formatted, late night confusion of a
> sketch of my thoughts, lets see if I can clean up this poor
> presentations...
>
> Here's a better presentation of the idea:
> http://informallyabstract.blogspot.com/2011/04/typed-signature-variables-for.html
> [...]
> I'd like to treat S1 as a signature variable... see blog post linked  
> above.

Sorry, I still don't get it. How can you project S1.t then?

> The thing is that I'd like to be able to include files within to to
> push for more flexibility in the way we consider context. e.g.
>
> functor F (S1 : SIG1) =
> struct
>  use "submodule1.ML";
>  use "submodule2.ML";
> end;

Yes, but what you _actually_ want is a way to compile the submodules  
separately, which is where the real problem lies.

> functor  new_module(
>  Map1 : MAP
>  Map2 : MAP
> ) : ...
> = struct ...
>
> then there are lots of ways which these maps may be related.
> perhaps Map1.key = Map2.key, perhaps Map2.key = Map1.value, etc. I
> think that the dependencies of module should be a well-defined
> signature, and the question is how to express this elegantly. The idea
> being that we want to be able to check at compile time if the
> composition of modules will work. I want a lightweight syntax for
> this, and tools support also (e.g. signature inference for modules, so
> you don't have to type it out). I do think you want explicit syntax
> for it, because this lets different people implement stuff
> independently. It makes code, and code development compositional...
> this is a nice theory, but do you also think it's a good idea? I've
> sometimes wondered about the need for all this explicitness, generally
> I do think it's good, as long as you can find short, easy syntax....

Well, "sharing" and "where"/"with" don't really differ in syntactic  
weight. I don't think you can make it much slimmer either. With  
sharing you don't have to eta-expand all type constructors, but that  
seems like a minor point.

> anyway, the idea of "except" is just to extend the expressive language
> of signatures to sharing.  It's just a syntactic mechanism to express
> exactly what is shared. Except lets you removing some stuff from a
> structure that you want to express is shared...
>
> e.g. writing
>  sharing (Map1 except map) <= Map2
> is the same as
>  sharing Map1.key = Map2.key
>  sharing Map1.value = Map2.value
> i.e. the keys and values are the same, but the data structure
> implementing the maps is different. The idea is that set-like
> expressions are a convenient way to say exactly what is shared.

I see. That seems doable. The problem with using subtractive  
composition for this purpose, though, is that it isn't particularly  
robust against signature extensions. What if somebody upstream later  
decides to add type t as a synonym for map to the MAP signature, to  
make certain functor compositions easier? It will break your constraint.

> But! I think a better language for expressing signatures can easily  
> fix this.
> e.g. we should be able to write:
>
> MAP = {  ... }
> SIG2A = { Map : SIG1 ... }
> SIG2B = { Map : SIG1 ... }
> SIG3A = {
>  Map : MAP;
>  S2a : SIG2A where S2a.Map := Map;
>  S2b : SIG2B where S2a.Map := Map;
>  ... }
>
> Having structure/signature level substitutions seems to naturally fix
> this: you now check a single Map at the top level, and modify all
> types in S2a to refer to those in the parent structure. This also
> cleans up the many occurrences of the same structure: I'm assuming
> that S2a.Map no longer exists after you write S2a.Map := ..., instead
> just have the single top-level Map. Maybe ":=" is not the best
> syntax... but I think you get the idea.

You actually have that in OCaml 3.12, with almost exactly your syntax.  
But your idiom again implements a form of flattening that will pollute  
the namespace of the signature's toplevel, and I think can still grow  
exponentially, just with a smaller constant factor.

I think there is no general solution. Specifying the signatures of  
arbitrary slices through a complex software architecture will produce  
ugly, big and complex signatures. That's why I don't want to be forced  
to do it everywhere. I only want to specify signatures at suitable  
package boundaries, where I expect looser coupling than within. Within  
a package, I just want to use other modules of the same package  
without (explicitly) reiterating their signature at every import edge.  
I.e., writing functors is not what I want there.

>> Well, there is a difference between referring to a concrete module  
>> you need,
>> just by name (a definite reference) or abstracting over the  
>> concrete module,
>> by giving its complete interface specification (an indefinite  
>> reference).
>> I'm just saying you want both, scoping and functorisation,  
>> depending on
>> whether the modules are in the same "package" or not. Always having  
>> to give
>> the full signature spec is just way too inconvenient.
>
> But when you specify a signature, you don't have to specify everything
> it has, only a super-set of what you use, I can't see how you could
> get away with less and maintain checking of module compositions...
> actually I'm not sure I'm understanding this point, maybe you can
> expand on it a bit?

Does my explanation above answer it?

Cheers,
/Andreas

[Caml-list] Re: functors and modules (was "What is an applicative functor?")

[Lucas Dixon]

On 3 May 2011 14:47, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
> On May 1, 2011, at 00.19 h, Lucas Dixon wrote:
>>>>
>>>> 2. the resulting signature of a Functor should be able to refer to the
>>>> input signatures. This would allow multiple inheritance in a natural
>>>> way:   functor S2(S1) : S1 + sig val f : S1.t -> int end;
>>>
>>> I don't understand. Is S1 a signature or structure here?
>>
>> I'm sorry! that was a terribly formatted, late night confusion of a
>> sketch of my thoughts, lets see if I can clean up this poor
>> presentations...
>>
>> Here's a better presentation of the idea:
>>
>> http://informallyabstract.blogspot.com/2011/04/typed-signature-variables-for.html
>> [...]
>> I'd like to treat S1 as a signature variable... see blog post linked
>> above.
>
> Sorry, I still don't get it.

Probably my fault, the post had some typos :( I think I've fixed them
now, as well as swapped the signature ordering, which makes more sense
now: more stuff = bigger.

>How can you project S1.t then?

S1 still has a type/signature, even though it is a variable: it's just
like an extensible record type (which is now signatures are often
implemented). S1 : { type t, ... }. So you can still project out what
you know is in S1. It's just that S1 may have more stuff as well.

Does that make sense?

I've extended the example and clarified it in the blog post.

>> The thing is that I'd like to be able to include files within to to
>> push for more flexibility in the way we consider context. e.g.
>>
>> functor F (S1 : SIG1) =
>> struct
>>  use "submodule1.ML";
>>  use "submodule2.ML";
>> end;
>
> Yes, but what you _actually_ want is a way to compile the submodules
> separately, which is where the real problem lies.

Ah, indeed! So we'd perhaps like each file to implicitly be a functor:

in "submodule1.ML":

given M1 : SIG1;
val x = M1.f "some argument string";
...

Is this what you're thinking of in terms of a looser module coupling?

>> functor  new_module(
>>  Map1 : MAP
>>  Map2 : MAP
>> ) : ...
>> = struct ...
>>
>> then there are lots of ways which these maps may be related.
>> perhaps Map1.key = Map2.key, perhaps Map2.key = Map1.value, etc. I
>> think that the dependencies of module should be a well-defined
>> signature, and the question is how to express this elegantly. The idea
>> being that we want to be able to check at compile time if the
>> composition of modules will work. I want a lightweight syntax for
>> this, and tools support also (e.g. signature inference for modules, so
>> you don't have to type it out). I do think you want explicit syntax
>> for it, because this lets different people implement stuff
>> independently. It makes code, and code development compositional...
>> this is a nice theory, but do you also think it's a good idea? I've
>> sometimes wondered about the need for all this explicitness, generally
>> I do think it's good, as long as you can find short, easy syntax....
>
> Well, "sharing" and "where"/"with" don't really differ in syntactic weight.
> I don't think you can make it much slimmer either. With sharing you don't
> have to eta-expand all type constructors, but that seems like a minor point.

If you have lots of types, it's a real pain to eta-expand them all by
hand. So being able to refer to large groups of them is quite
important. But I agree, it's a minor point really. It's just that the
syntax for doing this in SML is a bit broken.

>> anyway, the idea of "except" is just to extend the expressive language
>> of signatures to sharing.  It's just a syntactic mechanism to express
>> exactly what is shared. Except lets you removing some stuff from a
>> structure that you want to express is shared...
>>
>> e.g. writing
>>  sharing (Map1 except map) <= Map2
>> is the same as
>>  sharing Map1.key = Map2.key
>>  sharing Map1.value = Map2.value
>> i.e. the keys and values are the same, but the data structure
>> implementing the maps is different. The idea is that set-like
>> expressions are a convenient way to say exactly what is shared.
>
> I see. That seems doable. The problem with using subtractive composition for
> this purpose, though, is that it isn't particularly robust against signature
> extensions. What if somebody upstream later decides to add type t as a
> synonym for map to the MAP signature, to make certain functor compositions
> easier? It will break your constraint.

It's a good question and I'm not sure, but I think synonyms shouldn't
matter: a way you could do this is group type-names into
synonym-groups, and the "except" syntax removes the group.
Equivalently, type abbreviations are expanded and then are ignored for
sharing. That way you can use the synonym for sharing constraints, but
don't need to worry about it further.

A possible issue with this attitude is that if Map2 is actually some
extension of MAP, call it MAP2, which may have a type "t" (not a
synonym for MAP2.map), and then maybe you wanted Map1.t = Map2.t,
which wouldn't happen in the above story.

However, I suspect this is actually the right behaviour (as in Map1.t
is not made equal to Map2.t); and of course a warning should be issued
for such cases.

The point that subtraction is not robust to future extension: I agree.
This, I think, hits at a deeper issue in the modularity of structure
sharing: extending the signature of a module *can break* later module
compositions. This is because sharing constraints may no longer be met
after an earlier signature was extended.

This suggests that a collection of types in a module should be
explicitly grouped and named, and that group of names is what should
be shared. This would then be robust to extending the signatures of
earlier modules. It seems like it also requires more verbose writing
of how types from modules are related... maybe when types are declared
they could be explicitly added into 'type-groups' for sharing? or we
need a separate explicit collection of type names. (a bit like the
idiom of Sharing substructures...)

>> But! I think a better language for expressing signatures can easily fix
>> this.
>> e.g. we should be able to write:
>>
>> MAP = {  ... }
>> SIG2A = { Map : SIG1 ... }
>> SIG2B = { Map : SIG1 ... }
>> SIG3A = {
>>  Map : MAP;
>>  S2a : SIG2A where S2a.Map := Map;
>>  S2b : SIG2B where S2a.Map := Map;
>>  ... }
>>
>> Having structure/signature level substitutions seems to naturally fix
>> this: you now check a single Map at the top level, and modify all
>> types in S2a to refer to those in the parent structure. This also
>> cleans up the many occurrences of the same structure: I'm assuming
>> that S2a.Map no longer exists after you write S2a.Map := ..., instead
>> just have the single top-level Map. Maybe ":=" is not the best
>> syntax... but I think you get the idea.
>
> You actually have that in OCaml 3.12, with almost exactly your syntax. But
> your idiom again implements a form of flattening that will pollute the
> namespace of the signature's toplevel, and I think can still grow
> exponentially, just with a smaller constant factor.

I don't think it grows exponentially: Map does not exist in S2a or S2b.
I also don't think it is a form of name-space pollution. You need to
have some syntax for Map, so it has to live somewhere.  Or maybe I'm
missing something?

> I think there is no general solution. Specifying the signatures of arbitrary
> slices through a complex software architecture will produce ugly, big and
> complex signatures. That's why I don't want to be forced to do it
> everywhere. I only want to specify signatures at suitable package
> boundaries, where I expect looser coupling than within. Within a package, I
> just want to use other modules of the same package without (explicitly)
> reiterating their signature at every import edge. I.e., writing functors is
> not what I want there.

This sounds to me like just putting things in a global name-space, and
having a hierarchy of uses. I agree that this is useful, but isn't
this just avoiding the act of modularity altogether? I guess I'm
misunderstanding something. Maybe an small example would clarify?

>>> Well, there is a difference between referring to a concrete module you
>>> need,
>>> just by name (a definite reference) or abstracting over the concrete
>>> module,
>>> by giving its complete interface specification (an indefinite reference).
>>> I'm just saying you want both, scoping and functorisation, depending on
>>> whether the modules are in the same "package" or not. Always having to
>>> give
>>> the full signature spec is just way too inconvenient.
>>
>> But when you specify a signature, you don't have to specify everything
>> it has, only a super-set of what you use, I can't see how you could
>> get away with less and maintain checking of module compositions...
>> actually I'm not sure I'm understanding this point, maybe you can
>> expand on it a bit?
>
> Does my explanation above answer it?

Perhaps; but I think I might be misunderstanding, it seems that you're
suggesting just using the top-level to place background libraries. I
think this is often sensible, but this seems independent of having a
module system. So I suspect you're thinking of something else... ?

best,
lucas

[Caml-list] Re: functors and modules (was "What is an applicative functor?")

[Andreas Rossberg]

On May 11, 2011, at 15.11 h, Lucas Dixon wrote:
>>> Here's a better presentation of the idea:
>>>
>>> http://informallyabstract.blogspot.com/2011/04/typed-signature-variables-for.html
>>> [...]
>>> I'd like to treat S1 as a signature variable... see blog post linked
>>> above.
>>
>> Sorry, I still don't get it.
>
> Probably my fault, the post had some typos :( I think I've fixed them
> now, as well as swapped the signature ordering, which makes more sense
> now: more stuff = bigger.

OK, after reading it again, I'm afraid I still have more questions  
than answers: ;)

- What do you mean by "typed signature variables"? In what sense are  
ML's signature identifiers not variables, or not typed? Also, it seems  
that all your examples are easily expressible with existing language  
features, such as `include'. Consequently, I'm somewhat confused what  
exactly you are trying to achieve.

- I don't understand the semantics of your =: operator. AFAICS, the  
most specific signature of M1 is not S1, but "S1 with type T = int".  
(But even that depends on the details of the type system. If you had,  
for example, something akin to SML'90's structure sharing, then the  
most specific signature of M1 would, in fact, be the singleton M1.)

- It seems you want to express a form of mixin composition with your +  
operator, but you gloss over what the binding structure should be.  
That is, you seem to expect being able to say S1 + S2, where S2  
arbitrarily refers to members from S1. How is that supposed to work?  
(And would it differ from our `with' operator in MixML?)

- Similarly, where do you express the dependency between argument and  
result in a functor signature? S1 -> S1 is not the most specific  
signature of the identity functor over S1, that would be "(X:S1) -> S1  
with type T = X.T" in most ML's. How should I read your "exact" type  
of F2?


>> How can you project S1.t then?
>
> S1 still has a type/signature, even though it is a variable: it's just
> like an extensible record type (which is now signatures are often
> implemented). S1 : { type t, ... }. So you can still project out what
> you know is in S1. It's just that S1 may have more stuff as well.
>
> Does that make sense?

Not quite. :) I thought S1 is a signature itself? What does S1 :  
{ type t, ... } mean then?


>>> functor F (S1 : SIG1) =
>>> struct
>>>  use "submodule1.ML";
>>>  use "submodule2.ML";
>>> end;
>>
>> Yes, but what you _actually_ want is a way to compile the submodules
>> separately, which is where the real problem lies.
>
> Ah, indeed! So we'd perhaps like each file to implicitly be a functor:
>
> in "submodule1.ML":
>
> given M1 : SIG1;
> val x = M1.f "some argument string";
> ...
>
> Is this what you're thinking of in terms of a looser module coupling?

Depends on what that declaration does. AFAIU, it would still require  
me to functorize each individual module, just with a different syntax.


>>> But! I think a better language for expressing signatures can  
>>> easily fix
>>> this.
>>> e.g. we should be able to write:
>>>
>>> MAP = {  ... }
>>> SIG2A = { Map : SIG1 ... }
>>> SIG2B = { Map : SIG1 ... }
>>> SIG3A = {
>>>  Map : MAP;
>>>  S2a : SIG2A where S2a.Map := Map;
>>>  S2b : SIG2B where S2a.Map := Map;
>>>  ... }
>>>
>>> Having structure/signature level substitutions seems to naturally  
>>> fix
>>> this: you now check a single Map at the top level, and modify all
>>> types in S2a to refer to those in the parent structure. This also
>>> cleans up the many occurrences of the same structure: I'm assuming
>>> that S2a.Map no longer exists after you write S2a.Map := ...,  
>>> instead
>>> just have the single top-level Map. Maybe ":=" is not the best
>>> syntax... but I think you get the idea.
>>
>> You actually have that in OCaml 3.12, with almost exactly your  
>> syntax. But
>> your idiom again implements a form of flattening that will pollute  
>> the
>> namespace of the signature's toplevel, and I think can still grow
>> exponentially, just with a smaller constant factor.
>
> I don't think it grows exponentially: Map does not exist in S2a or  
> S2b.
> I also don't think it is a form of name-space pollution. You need to
> have some syntax for Map, so it has to live somewhere.  Or maybe I'm
> missing something?

What this feature buys you is that you can eliminate duplicates from  
your dependencies. That is, you actually get to represent your  
dependency graph in the signature as a DAG instead of a tree with  
copies. But you still potentially include that whole dependency graph  
in every signature.


>> I think there is no general solution. Specifying the signatures of  
>> arbitrary
>> slices through a complex software architecture will produce ugly,  
>> big and
>> complex signatures. That's why I don't want to be forced to do it
>> everywhere. I only want to specify signatures at suitable package
>> boundaries, where I expect looser coupling than within. Within a  
>> package, I
>> just want to use other modules of the same package without  
>> (explicitly)
>> reiterating their signature at every import edge. I.e., writing  
>> functors is
>> not what I want there.
>
> This sounds to me like just putting things in a global name-space, and
> having a hierarchy of uses. I agree that this is useful, but isn't
> this just avoiding the act of modularity altogether? I guess I'm
> misunderstanding something. Maybe an small example would clarify?

Well, small examples are difficult with this topic.

A module for me, typically, is an individual ADT. More generally, you  
can have modules with several abstract types, or cases with none, but  
the ADT is the essence of small-scale modularity.

But a module is not a library. A library (or package, or whatever term  
you prefer), is a collection of modules that are interdependent and  
closely related in terms of functionality as well as implementation.  
Building applications (or other libraries) from libraries is large- 
scale modularity. I don't think it's useful trying to turn every  
individual module into a stand-alone library -- which is what always  
functorizing amounts to.


>>> But when you specify a signature, you don't have to specify  
>>> everything
>>> it has, only a super-set of what you use, I can't see how you could
>>> get away with less and maintain checking of module compositions...
>>> actually I'm not sure I'm understanding this point, maybe you can
>>> expand on it a bit?
>>
>> Does my explanation above answer it?
>
> Perhaps; but I think I might be misunderstanding, it seems that you're
> suggesting just using the top-level to place background libraries. I
> think this is often sensible, but this seems independent of having a
> module system. So I suspect you're thinking of something else... ?

Yes: I simply want to parameterize libraries as a whole over their  
library dependencies, with as little fuzz as possible. At the level of  
individual modules, I want to use functors only where I need  
genericity. The ML module system is great for the latter, but  
currently not very useful for the former, i.e., it wasn't designed as  
a package system.

Cheers,
/Andreas

[Caml-list] Re: functors and modules (was "What is an applicative functor?")

[Lucas Dixon]

On 15 May 2011 05:05, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
> On May 11, 2011, at 15.11 h, Lucas Dixon wrote:
>>>>
>>>> Here's a better presentation of the idea:
>>>>
>>>>
>>>> http://informallyabstract.blogspot.com/2011/04/typed-signature-variables-for.html
>>>> [...]
>>>> I'd like to treat S1 as a signature variable... see blog post linked
>>>> above.
>>>
>>> Sorry, I still don't get it.
>>
>> Probably my fault, the post had some typos :( I think I've fixed them
>> now, as well as swapped the signature ordering, which makes more sense
>> now: more stuff = bigger.
>
> OK, after reading it again, I'm afraid I still have more questions than
> answers: ;)
>
> - What do you mean by "typed signature variables"? In what sense are ML's
> signature identifiers not variables, or not typed?

in a functor, the signatures are defined, there are no lambda
variables which have a signature as a type... see below...

> Also, it seems that all
> your examples are easily expressible with existing language features, such
> as `include'. Consequently, I'm somewhat confused what exactly you are
> trying to achieve.
>
[moved the next up]
> - Similarly, where do you express the dependency between argument and result
> in a functor signature? S1 -> S1 is not the most specific signature of the
> identity functor over S1, that would be "(X:S1) -> S1 with type T = X.T" in
> most ML's. How should I read your "exact" type of F2?

Ah, I think I know what was confusing things: I was using the same
name of signature when what I really meant was a lambda-abstraction...
(the old free-variable implicitly being a lambda abstraction...
sigh... ); how about this explanation:

I want to define a functor like this:
F(M : S1) = { open M; val y = ... };

and I want it to have a type like this:
F : "For S <= S', S -> (S + { val y: T. })"

if I give F an input of signature S1 (which must itself be expressible
as an include of S', that's what the <= means) then I get a structure
with signature:
  "sig include S1; val y : T end;"

if, on the other hand, I give F an input of signature S2, then I get
out a structure with signature:
  "sig include S2; val y : T end;"

This cannot (to my knowledge) be expressed in ML at present. In ML I'd
need to write the same functor for each typing. i.e.:

functor F1(M : S1) : sig include S1; val y : T end
= struct open M; val y : T end;

and

functor F2(M : S2) : sig include S2; val y : T end
= struct open M; val y : T end;

If you give yourself signature level variables in functors, you rather
nicely express many OO style things in functors.

> - I don't understand the semantics of your =: operator. AFAICS, the most
> specific signature of M1 is not S1, but "S1 with type T = int". (But even
> that depends on the details of the type system. If you had, for example,
> something akin to SML'90's structure sharing, then the most specific
> signature of M1 would, in fact, be the singleton M1.)

For M =: S, I'm considering M as a record, each type and value is an
entry. And M =: S says that M has no more entries in the record, than
are specified in S.

There is a fine distinction between the usual unification based notion
and this one, which I don't think I fully appreciated until I started
writing this email: unification mixes up whats in the domain with what
it can be instantiated with. I have a hunch that these are separate
things and should be treated as such.

> - It seems you want to express a form of mixin composition with your +
> operator, but you gloss over what the binding structure should be. That is,
> you seem to expect being able to say S1 + S2, where S2 arbitrarily refers to
> members from S1. How is that supposed to work? (And would it differ from our
> `with' operator in MixML?)

Nothing fancy; I was thinking simply of sequential union, I guess I
should not have used "+" as that's normally thought of as commutative.
But using MixML's "with" would be fine too.

>>> How can you project S1.t then?
>>
>> S1 still has a type/signature, even though it is a variable: it's just
>> like an extensible record type (which is now signatures are often
>> implemented). S1 : { type t, ... }. So you can still project out what
>> you know is in S1. It's just that S1 may have more stuff as well.
>>
>> Does that make sense?
>
> Not quite. :) I thought S1 is a signature itself? What does S1 : { type t,
> ... } mean then?

The reply above is not probably more meaningful than this thread of
the conversation, but what I meant was that S1 can be expressed using
an include of sig type T = ... end; I'm thinking of signatures as the
typing of a record: i.e. the names of the fields, and their typing.
Variables of record type don't need to specify all fields. You get the
natural mix-in style typing.

>>>> functor F (S1 : SIG1) =
>>>> struct
>>>>  use "submodule1.ML";
>>>>  use "submodule2.ML";
>>>> end;
>>>
>>> Yes, but what you _actually_ want is a way to compile the submodules
>>> separately, which is where the real problem lies.
>>
>> Ah, indeed! So we'd perhaps like each file to implicitly be a functor:
>>
>> in "submodule1.ML":
>>
>> given M1 : SIG1;
>> val x = M1.f "some argument string";
>> ...
>>
>> Is this what you're thinking of in terms of a looser module coupling?
>
> Depends on what that declaration does. AFAIU, it would still require me to
> functorize each individual module, just with a different syntax.

Yes, reading the stuff you wrote below, I think I finally understand
the distinction you're aiming for in terms of modules from libraries.
Makes sense. :)

>>>> But! I think a better language for expressing signatures can easily fix
>>>> this.
>>>> e.g. we should be able to write:
>>>>
>>>> MAP = {  ... }
>>>> SIG2A = { Map : SIG1 ... }
>>>> SIG2B = { Map : SIG1 ... }
>>>> SIG3A = {
>>>>  Map : MAP;
>>>>  S2a : SIG2A where S2a.Map := Map;
>>>>  S2b : SIG2B where S2a.Map := Map;
>>>>  ... }
>>>>
>>>> Having structure/signature level substitutions seems to naturally fix
>>>> this: you now check a single Map at the top level, and modify all
>>>> types in S2a to refer to those in the parent structure. This also
>>>> cleans up the many occurrences of the same structure: I'm assuming
>>>> that S2a.Map no longer exists after you write S2a.Map := ..., instead
>>>> just have the single top-level Map. Maybe ":=" is not the best
>>>> syntax... but I think you get the idea.
>>>
>>> You actually have that in OCaml 3.12, with almost exactly your syntax.
>>> But
>>> your idiom again implements a form of flattening that will pollute the
>>> namespace of the signature's toplevel, and I think can still grow
>>> exponentially, just with a smaller constant factor.
>>
>> I don't think it grows exponentially: Map does not exist in S2a or S2b.
>> I also don't think it is a form of name-space pollution. You need to
>> have some syntax for Map, so it has to live somewhere.  Or maybe I'm
>> missing something?
>
> What this feature buys you is that you can eliminate duplicates from your
> dependencies. That is, you actually get to represent your dependency graph
> in the signature as a DAG instead of a tree with copies. But you still
> potentially include that whole dependency graph in every signature.

If you eliminate all duplication, the size of the DAG will only be as
big as it needs to be. It can't be any smaller. I guess the key issue
is: can sufficiently nice syntax exists to express DAG in the way we
want it; and in particular, for abstracting certain details as you
build up your library/modules. That's perhaps the key issue. That's
where I think deletion syntax may be particularly useful...

>>> I think there is no general solution. Specifying the signatures of
>>> arbitrary
>>> slices through a complex software architecture will produce ugly, big and
>>> complex signatures. That's why I don't want to be forced to do it
>>> everywhere. I only want to specify signatures at suitable package
>>> boundaries, where I expect looser coupling than within. Within a package,
>>> I
>>> just want to use other modules of the same package without (explicitly)
>>> reiterating their signature at every import edge. I.e., writing functors
>>> is
>>> not what I want there.
>>
>> This sounds to me like just putting things in a global name-space, and
>> having a hierarchy of uses. I agree that this is useful, but isn't
>> this just avoiding the act of modularity altogether? I guess I'm
>> misunderstanding something. Maybe an small example would clarify?
>
> Well, small examples are difficult with this topic.
>
> A module for me, typically, is an individual ADT. More generally, you can
> have modules with several abstract types, or cases with none, but the ADT is
> the essence of small-scale modularity.

cool, that makes sense, that's what I think of too. :)
How's this for a starting point of an example... libraries will want
to define lots of different ADTs, e.g. for trees, heaps, queues,
directed graphs, tables, XML, IO, ... Many will be built in terms of
each other... I guess the ML Standard Basis library is an example, or
the Isabelle libraries, or the ocaml batteries?

In the Isabelle libraries there is essentially no modularity
management of the library as a whole. Locally things are functorised
for some genericity, but overall everything just sits on a top-level.
So I guess if you wanted to include "just the right" bits, it would be
a little unclear how to do it. What I do at present is to load it all
up, then push out stuff from the top-level, and use the garbage
collector to clean up...

I think I see the problem of library management/modularity now - how
to make the (inter) dependencies of bigger libraries less ad-hoc. So
that we can easily identify which bits we use, what to link and what
not to...  cool, it's nice to see a problem. :)

In a sense, I think there are two issues here: one is name-space
management, and the other is linking/compilation of just what is
needed... if name-space is delt with properly, then it feels like all
linking/compilation should be inferable from some small bit of
top-level code that is explicitly intended to be used... it seems like
a garbage collection-like problem - track the detailed dependencies...
? So maybe the real issue is name-space management?

> But a module is not a library. A library (or package, or whatever term you
> prefer), is a collection of modules that are interdependent and closely
> related in terms of functionality as well as implementation. Building
> applications (or other libraries) from libraries is large-scale modularity.

Nice terminology; that's good, and I think I see the distinction you
are making now between libraries and modules. It makes lots of sense.

> I don't think it's useful trying to turn every individual module into a
> stand-alone library -- which is what always functorizing amounts to.

I guess I'm still not sure why... or maybe I do... I mean I agree that
if you carelessly include sub-structures that's bad in many ways and
leads to terribly big signatures; and so I agree that this is not 'the
right way' to do it. I guess I still think that we can change some
syntax and it might be all rosy...  :)

>>>> But when you specify a signature, you don't have to specify everything
>>>> it has, only a super-set of what you use, I can't see how you could
>>>> get away with less and maintain checking of module compositions...
>>>> actually I'm not sure I'm understanding this point, maybe you can
>>>> expand on it a bit?
>>>
>>> Does my explanation above answer it?
>>
>> Perhaps; but I think I might be misunderstanding, it seems that you're
>> suggesting just using the top-level to place background libraries. I
>> think this is often sensible, but this seems independent of having a
>> module system. So I suspect you're thinking of something else... ?
>
> Yes: I simply want to parameterize libraries as a whole over their library
> dependencies, with as little fuzz as possible. At the level of individual
> modules, I want to use functors only where I need genericity. The ML module
> system is great for the latter, but currently not very useful for the
> former, i.e., it wasn't designed as a package system.

I totally agree with this. :)

I guess now I've understood, I don't mind letting this tread
trickle-out, and maybe speaking to you in person would be more
efficient... :)

cheers!
lucas