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

[Lucas Dixon <lucas.dixon@gmail.com>]

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