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

[Andreas Rossberg <rossberg@mpi-sws.org>]

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