From mboxrd@z Thu Jan 1 00:00:00 1970 X-Sympa-To: caml-list@inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p4BDBU5E013698 for ; Wed, 11 May 2011 15:11:30 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjgDAEKKyk3RVdY2kGdsb2JhbAClfggUAQEBAQkJDQcUBCGIcKJKjBmCMoUON4hfAQEDBoYKBI9winQ7g04 X-IronPort-AV: E=Sophos;i="4.64,353,1301868000"; d="scan'208";a="98814657" Received: from mail-bw0-f54.google.com ([209.85.214.54]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 11 May 2011 15:11:24 +0200 Received: by bwz12 with SMTP id 12so895331bwz.27 for ; Wed, 11 May 2011 06:11:24 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:in-reply-to:references:date :message-id:subject:from:to:cc:content-type :content-transfer-encoding; bh=lZkPF5/QqNd818MkScsvuitYxqb4QMgGPiPIxK1Dmz0=; b=BtzAem16YU8SpPCh+oe6YeZL7ayYZpFfah+41JpLKWJorhlxUr0bgebMN6oQSSfUV4 P6wMxt7kRTbRLAde1tjJ4P5VPzL3aMK0ATkAJ3M8efyYnUsaAFoPPKEhSKPh+8lxuB6V 4QQnfrB0CBCfun341TCEYRK2j564xnTQq+U2c= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=drvm7zAd7JNnDGs1JNw7DWubqfnGr5lBMWU+2TZdp+PL6HYJa29/Ko3FJUplJ7GeZD NNrgmZHwVWpwiuMaseJFnQen7oHVkSJOFg3GAs6BIqrGwDQHI51d5rzjxHgEMgJKzftv stmKoFYZ9PUGO88fbTE9bqE0SpAEg9FQOECxs= MIME-Version: 1.0 Received: by 10.204.82.200 with SMTP id c8mr3674364bkl.90.1305119484100; Wed, 11 May 2011 06:11:24 -0700 (PDT) Received: by 10.204.59.129 with HTTP; Wed, 11 May 2011 06:11:23 -0700 (PDT) In-Reply-To: References: <1CD0C5CF-4339-4365-A05C-58A12EE7AE2D@mpi-sws.org> Date: Wed, 11 May 2011 09:11:23 -0400 Message-ID: From: Lucas Dixon To: Andreas Rossberg Cc: caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p4BDBU5E013698 X-Validation-by: lucas.dixon@gmail.com Subject: [Caml-list] Re: functors and modules (was "What is an applicative functor?") On 3 May 2011 14:47, Andreas Rossberg 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