tag:blogger.com,1999:blog-2447174102813539049.post5432238908376918714..comments2024-03-29T03:43:02.688-07:00Comments on Room 101: Types are Anti-ModularGilad Brachahttp://www.blogger.com/profile/17934280339206214042noreply@blogger.comBlogger69125tag:blogger.com,1999:blog-2447174102813539049.post-4025805433448152642022-04-12T05:16:12.743-07:002022-04-12T05:16:12.743-07:00SAP SD Training In Noida<a href="https://www.vevioz.com/read-blog/53906_sap-sd-training-institute-in-noida-2022.html" rel="nofollow">SAP SD Training In Noida</a>ERP Training Noidahttps://www.blogger.com/profile/16035514502876470407noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-41797894852901386352011-11-15T14:42:47.024-08:002011-11-15T14:42:47.024-08:00Even without types, syntactic extensions (such as ...Even without types, syntactic extensions (such as macros or readtables in Lisp, a dynamically-typed language) constitute essential meta-level information about modules that require this pulling in of all transitive dependencies to compile a given module.<br /><br />Static I-modularity is only a special case of S-modularity where your language is too poor to express rich meta-level information.<br /><br />Note that if you're interested in best effort for the common case, you can pre-compile with incorrect information about the meta-level context, then recompile the parts where you got it wrong when the hypotheses are invalidated. Or why not be completely lazy at compiling? A JIT is the ultimate provider of dynamic I-modularity. No need to statically compile at all!Faréhttps://www.blogger.com/profile/14063105144178880818noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-9667155737671507042011-08-06T09:00:16.837-07:002011-08-06T09:00:16.837-07:00John,
Good point. The expression problem is reall...John,<br /><br />Good point. The expression problem is really a type problem. It isn't nearly as acute if you aren't worried about the typechecking. I guess I should write a post about that sometime. But I have to get on a plane soon - so don't expect prompt follow up :-)Gilad Brachahttps://www.blogger.com/profile/17934280339206214042noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-86465269831051817622011-08-05T18:04:06.340-07:002011-08-05T18:04:06.340-07:00Phil,
Thanks for the clarification! Now your ori...Phil,<br /><br />Thanks for the clarification! Now your original note on the Expression Problem is much clearer, and explains the confusion many (including me) had!<br /><br />The Expression Problem deals with the fact that I-modular is impossible in typed languages, so S-modular is the best we can do when extending both functions and/or data.<br /><br />I buy that.<br /><br />This then sets up a delightful question: What about I-modular for untyped languages and extending both functions and/or data? If Gilad's approach with many forms of static analysis is a good one, then this question should help explain why it is a good one.John Zabroskihttps://www.blogger.com/profile/17294832205855394228noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-17070996652904098282011-08-05T06:58:44.398-07:002011-08-05T06:58:44.398-07:00"I value I-modularity, full reflection, and f..."I value I-modularity, full reflection, and freedom to express my ideas in code more than the benefits of typechecking."<br /><br />That's crazy! Just because I-modularity allows modules to be *compiled* without verification against one another doesn't mean you are free to express ideas more freely: any data that can be passed from module to module requires that both modules understand the structure of the data - whether that structure is defined (verifiably) in a third module or is merely defined (unreliably) in the heads of the programmers, there is still a dependency that must be respected to achieve a correct program. Not even full reflection can properly recover the *meaning* of that exchanged data without either a programmer or a type somehow embedding the functional constraints of that data - again, forcing at least some kind of dependency.<br /><br />The "free composability" or "free expression of ideas" supposedly afforded by I-modularity is an illusion!David V. McKayhttps://www.blogger.com/profile/14797607289938236220noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-72040008229644536012011-08-03T06:48:16.243-07:002011-08-03T06:48:16.243-07:00Hi Phil,
Thank you for your comment, which is ver...Hi Phil,<br /><br />Thank you for your comment, which is very much to the point. The high bit is that there are not only benefits, but also costs associated with types and typechecking.<br />The absence of I-Modularity is one of them.<br /><br />Depending on ones goals, context etc. such costs may be considered very worthwhile or not. I value I-modularity, full reflection, and freedom to express my ideas in code more than the benefits of typechecking. There isn't much in the way of science to measure this, so the debate rages on religiously, colored by personal experience.<br /><br /> In practice, I continue to advocate a pragmatic engineering approach where typechecking is one of many possible static analyses (pluggable types) and not a basic requirement every a legal program must fullfill. I believe it gives a better engineering tradeoff<br /><br />But you knew all that. And I agree, the thread is too long.Gilad Brachahttps://www.blogger.com/profile/17934280339206214042noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-77263984686086153692011-08-03T06:40:38.180-07:002011-08-03T06:40:38.180-07:00The point is about S-modularity, and thus more tro...The point is about S-modularity, and thus more troubling. <br /><br />In a large program, in a language with user-defined types, the types used in an interface are themselves defined in other interfaces. To compile a module, you need not just the interfaces of all the modules it depends on, but also all the interfaces of all the types that interface uses, transitively.<br /><br />Thus, (nominal) types add a significant number of extra interfaces the compiler has to look at in order to compile one module.Lex Spoonhttps://www.blogger.com/profile/13859632965228608649noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-80554716124486571892011-08-03T03:37:44.429-07:002011-08-03T03:37:44.429-07:00Gilad,
Modulo mottoes, everything you say is true...Gilad,<br /><br />Modulo mottoes, everything you say is true.<br /><br />The same word may carry many meanings, so let's clarify terminology:<br /><br /><i>S-modular</i>: supports separate compilation. Every module has an interface and a source. Compiling a module requires access to the interface, but not the source, of every module the compiled module depends upon.<br /><br /><i>I-modular</i>: supports independent compilation. Compiling a module requires access only to the source of the module being compiled.<br /><br />Your motto becomes 'Types are anti-I-modular', which is unarguable.<br /><br />Implicit in your argument is the claim that I-modularity is to be valued over S-modularity. I would claim that the additional checking offered by S-modularity is more important to separation of concerns than the independence offered by I-modularity. What is your argument against my claim?<br /><br />(Apologies if you answered this point in the comments thread---it was too lengthy for me to read all of it.)<br /><br />Yours, -- PPhilip Wadlerhttps://www.blogger.com/profile/12009347515095774366noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-21091590977187589972011-07-24T12:13:07.150-07:002011-07-24T12:13:07.150-07:00For independent compilation (and design) of typed ...For independent compilation (and design) of typed interfaces, modules can declare their interfaces independently, then a glue module coerces their interfaces to interopt.<br /><br />Imagine a client that integrates a test server. The interface of the test server is the external interface of the client.<br /><br />Or in other words, the boundary between intra-module modularity and inter-module modularity is arbitrary and thus doesn't exist.<br /><br />All type systems leak implementation to the extent that the semantic invariants are not checked by the compiler. Checking more invariants (stronger typing) is an attempt to leak less implementation, to catch more errors at compile-time.<br /><br />P.S. the failure of an arbitrary barrier to the free market is expected by Coase's Theorem. Coase's Theorem is a special case of 2nd law of thermo, and the 2nd law states the the universe trends to maximum independent (more precisely orthogonal) actors (i.e. disorder/entropy).shelbyhttps://www.blogger.com/profile/04192118408905938326noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-38958014266401925922011-07-19T16:21:42.463-07:002011-07-19T16:21:42.463-07:00Broad, negatively flavored expressions such as &qu...Broad, negatively flavored expressions such as "[x] is Anti-[y]" or "[x] Considered Harmful" make excellent headlines - because they are inflammatory and command attention; but only just long enough for readers to be convinced the headline is incorrect.<br /><br />I will give the author the benefit of the doubt in assuming he was not attempting to broadly dismiss the utility of Static Type Systems in constructing practical, maintainable software solutions with useful degrees of modularity. Rather, I will assume this is an academic argument that Static Type Systems strongly inhibit our ability to construct units of software that can inter-operate at runtime without common references to the same type definitions. The author uses this assertion to advocate Dynamic Type Systems, petitio principii, are more useful due to their late-bound composability. ...Because this is "more modular" and because "more modular is better" because "it is more modular."<br /><br />Now I will argue that dependent compilation is in fact a benefit of Static Type Systems, because it limits the possible behaviours of the system to strictly those behaviours that can be predicted, analysed, and verified at design-time -- automatically, and with ample opportunity to correct the defects before affecting users in production. By counterpoint, the late-bound composability of dynamic type systems cannot make such guarantees via automatic verification; to ensure these systems do not fail in deployment, the engineers must manually devise a comprehensive suite of unit tests - but to achieve full comprehensiveness, the programmers must either have access to all modules that might be integrated at runtime, or must make strong assumptions about the competence of other programmers, in that third party modules must conform to the documented interfaces. This entails documentation that is clear, up to date, and is furthermore correctly understood and implemented by the third party.<br /><br />In short, Dynamic Type Systems achieve this "freer composability" at the expense of shifting the onus of verification to humans. Regardless, the total information required to construct and compose all modules is equivalent whether the composition be late-bound or not.<br /><br /><br />I appreciate the reflection of these earlier posts:<br />Dave Herman 6/11/11 4:21 PM<br />Jon Rimmer 6/25/11 6:13 AM<br />The Observer 7/06/11 7:51 AMDavid V. McKayhttps://www.blogger.com/profile/14797607289938236220noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-29301009290581644182011-07-07T06:34:06.930-07:002011-07-07T06:34:06.930-07:00I was under the impression that Barbara Liskov'...I was under the impression that Barbara Liskov's CLU had modules with separate compilation. I have a copy of the CLU Reference manual which seems to indicate that this is supported on page 17.<br /><br />Digging around online throws up this .pdf version:<br /><br />http://publications.csail.mit.edu/lcs/pubs/pdf/MIT-LCS-TR-225.pdf<br /><br />I've really no idea whether this is THE solution, but I have long favoured its approach (especially its use of type-orientation rather than object orientation).Uncompetativehttps://www.blogger.com/profile/11740139097865154127noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-18398836511230230822011-07-06T07:51:36.564-07:002011-07-06T07:51:36.564-07:00To be completely modular, a program must take in a...To be completely modular, a program must take in arbitrary input and put out arbitrary output, with no regard for what either the input or output is. The problem is that such a program can't do anything useful. In order to preform useful operations, one must have some knowledge of what the input and output will be. Type systems simply formalize this notion and make its declaration explicit so that it can be checked by a compiler. This relieves the burden of having to check and debug types manually, but adds the burden of having to structure your code properly and provide extra information before compilation. Does this restrict the freedom of the programmer? Yes, but it does so in order to limit errors. It's a tradeoff.The Observerhttps://www.blogger.com/profile/14453002621235541278noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-54270520113502348792011-07-05T10:15:32.004-07:002011-07-05T10:15:32.004-07:00Not only does module composition consume informati...Not only does module composition consume information about the code inside the modules, the entire NATURE and PURPOSE of module composition is to consume information about the code inside the modules. Therefore, any such information is "anti-modular". It's a feature, not a bug!Faréhttps://www.blogger.com/profile/14063105144178880818noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-32873548822240145212011-06-27T07:28:56.611-07:002011-06-27T07:28:56.611-07:00It's not impossible, you simply need type infe...It's not impossible, you simply need type inference to lift the dependencies inferred from the implementation to the module boundary. See the link I provided earlier on first-class messages. There will obviously be some limitations, and Gilad is concerned this will leak implementation details, but it doesn't seem like this has really been tried before, so it's not a foregone conclusion I'd say.Sandro Magihttps://www.blogger.com/profile/05446177882449578817noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-71595057281377526892011-06-27T01:56:57.599-07:002011-06-27T01:56:57.599-07:00> where you compile something without even know...> where you compile something without even knowing what the signature are of what you are depending on. Of course, that is impossible to do in a statically typed language<br /><br />Exactly. And my two statements are: 1) it's impossible in any type-safe language ("independent compilation" is impossible in statically typed languages, "compilation" is, in fact, impossible in dynamically typed ones), and 2) it has absolutely nothing to do with modularity, the difference being - forgive me for this analogy - same as between freedom and anarchy.migmithttps://www.blogger.com/profile/06981055611018991476noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-71215368657443616432011-06-26T20:27:05.834-07:002011-06-26T20:27:05.834-07:00migmit,
Units are more like ML functors that supp...migmit,<br /><br />Units are more like ML functors that support recursive assembly. Or, if you prefer the C header analogy, they are parameterized, statically type checked, and support true separate compilation.<br /><br />Research on separate compilation is pretty flushed out, its not a problem anymore. However, not much research on modular compilation has been adopted by industry and new languages continue to lack it. To me, this means that separate compilation wasn't a real problem needing to be solved.<br /><br />On closer reading, Gilad presents independent compilation as a new concept distinct from separate compilation, where you compile something without even knowing what the signature are of what you are depending on. Of course, that is impossible to do in a statically typed language: you need the context of your unit to be encoded in order to compile it.Sean McDirmidhttps://www.blogger.com/profile/16610011228675377563noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-80405806367564944322011-06-25T06:13:25.276-07:002011-06-25T06:13:25.276-07:00I don't have the theoretical background to con...I don't have the theoretical background to contribute much to this discussion, but it seems to me that saying types are a countervailing force to modularity is like saying the land is a countervailing force to the sea. There's a certain attraction to it on a surface level, but on a deeper level it misrepresents the relationship between the two as one that is somehow antagonistic, when in fact it is one of existential interdependence.<br /><br />A module is a sort of a partial enclosure. And the 'partial' aspect, implying a degree of flow or exchange between modules, is just as important to the concept as that of enclosure. Modularity is not synonymous with independence, but rather a conscious and managed dependence. In situations where they are used therefore, it can be said that types are pro-modular, as they facilitate the managed dependence that is essential for modularity to even exist.<br /><br />Discussions of static-vs-dynamic typing, independent compilation, separate interfaces, etc., are all very important. But in discussing the practical details of these approaches, we shouldn't lose sight of modularity being both independence <i>and</i> dependence (sort of a yin-yang thing, if you will). With this in mind, it seems unfair to denigrate typing as a whole, and will just lead us down an incorrect path of viewing greater independence as more perfect modularity, when it is not so.Jon Rimmerhttps://www.blogger.com/profile/07587503998121686945noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-90783749924940345562011-06-24T14:50:26.538-07:002011-06-24T14:50:26.538-07:00Gilad,
I am not sure what you mean by checking in...Gilad,<br /><br />I am not sure what you mean by checking intention when linking globally, but my best guess based on intuition is that you would need to have an inconsistency tolerant linker.<br /><br />I am not saying this as an ad-hominem attack on your idea, e.g. "Is inconsistency tolerance really a path you want to go down?". I have just thought about this sort of stuff for a very long time, and focused on my personal dream of building a computer network that can function at the scale of a hojillion nodes. When I think about global design trade-offs, I am literally wondering about things like propagation delay when the speed of light is your bottleneck. What does the structure of an efficient software system look like at that scale?<br /><br />Postscript:<br />Modularity is a complex topic. Surveying Hacker News, Reddit and Lambda the Ultimate meta-discussion about this blog post reveals many different viewpoints on the topic. I could add several more. For example, algebraic semiotics of Joe Goguen and his classical example of a "modular" description of a sign post that says "Stop".<br /><br />I think there are enough "good" theories. What needs to be outlined are the trade-offs, and those trade-offs then need to be used to judge how we can automate human social processes in niche human organizations - like your pet peeve of static build definition for the Organization of Software Engineers.John Zabroskihttps://www.blogger.com/profile/17294832205855394228noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-19938074832478709882011-06-24T01:08:22.478-07:002011-06-24T01:08:22.478-07:00> It is not strictly true that you need a globa...> It is not strictly true that you need a global namespace somewhere to boot strap a module system.<br /><br />I'm kinda confused. When did I mention namespaces?<br /><br />Read Jiazzi paper; not impressed. Seems a lot like C headers.migmithttps://www.blogger.com/profile/06981055611018991476noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-62275160820657991582011-06-23T08:35:34.898-07:002011-06-23T08:35:34.898-07:00John,
Your comments are most apropos.
My underst...John,<br /><br />Your comments are most apropos.<br /><br />My understanding of the expression problem as Phil formulated it is that it is problem of typed languages as Martin said. I find that quite in line with what I have stated in this post. <br /><br />I'm not sure I see how erasure helps here - we still have to specify the types which has the same problems of redundancy/information leakage/external dependency. <br /><br />What might bepractical in my view may be, as I indicated, to type check locally based on inferred dependencies and then check intention when linking globally.Gilad Brachahttps://www.blogger.com/profile/17934280339206214042noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-61856442764585574472011-06-23T02:06:39.545-07:002011-06-23T02:06:39.545-07:00migmit,
It is not strictly true that you need a g...migmit,<br /><br />It is not strictly true that you need a global namespace somewhere to boot strap a module system. Modules can always directly describe the shapes of their imports and exports, while module linking can occur via tangible reference (basically, you refer to the module by its complete definition). See the OOPSLA '01 Jiazzi paper for a discussion on that. <br /><br />For usability and compatibility reasons, you do want a global namespace somewhere; i.e., modules are referred to by name in a global namespace while they share signatures to economize shape description. Global namespaces are also very convenient for helping people to find and reuse things (but make the namespace truly global, as in the web).Sean McDirmidhttps://www.blogger.com/profile/16610011228675377563noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-17151463710338624172011-06-23T01:59:14.411-07:002011-06-23T01:59:14.411-07:00> You can parameterize the types in your module...> You can parameterize the types in your module to obtain real independent compilation.<br /><br />Ehm, really?<br /><br />But shouldn't the type parameters at least implement some specific interface?<br /><br />And interfaces are types, which brings us to square one.migmithttps://www.blogger.com/profile/06981055611018991476noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-26179922053865294162011-06-23T00:03:26.958-07:002011-06-23T00:03:26.958-07:00migmit,
You can parameterize the types in your mo...migmit,<br /><br />You can parameterize the types in your module to obtain real independent compilation. Jiazzi was one of my old research projects that did this for Java. To make that scalable is challenging, but not impossible. <br /><br />However, it does not seem to add much value, types aren't the real problem with separate compilation, or separate compilation is not a real problem (C# chugs away just fine with no real support for separate compilation).Sean McDirmidhttps://www.blogger.com/profile/16610011228675377563noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-26145480831107979322011-06-22T23:59:28.689-07:002011-06-22T23:59:28.689-07:00This comment has been removed by the author.migmithttps://www.blogger.com/profile/06981055611018991476noreply@blogger.comtag:blogger.com,1999:blog-2447174102813539049.post-71508794697254312892011-06-22T23:58:11.317-07:002011-06-22T23:58:11.317-07:00So... it seems that you're equating "modu...So... it seems that you're equating "modularity" with "independent compilation". Doubtful as it is, another question is more interesting: are there any practical examples of "independent compilation"? Seems like the only choice we have is between "non-independent compilation with types" and "no types and no real compilation at all".migmithttps://www.blogger.com/profile/06981055611018991476noreply@blogger.com