Program Fragments Linking and Modularization Luca Cardelli luca pa dec com Digital Equipment Corporation Systems Research Center Abstract Module mechanisms have received considerable theoretical attention but the associated concepts of separate compilation and linking have not been emphasized Anomalous module systems have emerged in functional and object oriented programming where software components are not separately typecheckable and compilable In this paper we provide a context where linking can be studied and separate compilability can be formally stated and checked We propose a framework where each module is separately compiled to a self contained entity called a linkset we show that separately compiled compatible modules can be safely linked together 1 Introduction Program modularization arose from the necessity of splitting large programs into fragments in order to compile them As system libraries grew in size it became essential to compile the libraries separately from the user programs libraries acquired interfaces that minimized compilation dependencies A linker was used to patch compiled fragments together It was soon realized that modularization had great advantages in terms of large grain program structuring 19 Much fundamental and practical research focused on modularization principles and properties milestones in this process are embodied in such constructs as object oriented classes Modula 2 modules and Standard ML functors Since program structuring is of great importance in software engineering there is motivation for continuously increasing the flexibility and convenience of modularization constructs Unfortunately in the shadow of many exciting developments there has been a tendency to overlook the original purpose of modularization Some language definitions specify what are to be the compilation units e g Ada 12 but others do not e g Standard ML 17 A paradoxical question then arises when does a module system really support modularization meant as separate compilation Appears in the Proceedings of the 24th Annual ACM Symposium on Principles of Programming Languages Paris France January 1997 ACM In designing and formalizing module systems many proposals have focused on the analogy between modules and data structures and between interfaces and data types e g as in Burstall s influential paper 4 In such proposals modules and interfaces become language constructs to program with This approach has the advantage of adding clean programmability to the area of system configuration where it has traditionally been lacking When pushing this approach to extremes though there is the danger of losing sight of the requirements of separate compilation In this paper we take a different approach in order to maintain a natural and accurate view of the separate compilation and linking process We consider linking as the fundamental process from which module mechanisms arise not merely as a technique for managing large programs and libraries Further we consider modularization as inseparable from separate compilation not merely as a program structuring mechanism Instead of considering interfaces as just another program construct we look at interfaces as typing environments that are intrinsically external to the programming language By adopting this view we can develop modularization mechanisms with precise notions of separate compilation inter module typechecking and linking Today the purpose of separate compilation is to be able to write check deliver maintain and upgrade libraries of code possibly hiding the source code from the clients of the libraries Many things can go wrong in languages and environments designed or coerced to support separate compilation To understand the range of problems that may arise let us consider an example of a software development cycle and the obstacles that may impede it In this example a library module and a user module interact over time it is instructive to assume that library development and client development happen in separate locations Day 1 Library description A library interface ILib is publicized before any corresponding implementation module MLib is made available The purpose is to allow early development of client software that will later be integrated with the library Therefore in this scenario we assume that there exists a notion of largely code free interfaces Obstacles Early programming languages both procedural and object oriented did not separate interfaces from implementations Languages that are designed to be small or untyped often lack interfaces Certain language features may require glo Thursday October 24 1996 11 32 am 1 bal analysis and may thus conflict with modularity examples are multimethods 7 and overloading Day 2 User program description A user interface IUsr is written without yet producing the corresponding user module MUsr The purpose is to begin designing the structure of MUsr and its interaction with ILib before making any actual implementation commitments The interface IUsr is based on ILib Obstacles It is important to be able to write IUsr on the basis of definitions contained in ILib the purpose of ILib is often to define shared types Modula 2 for example allows type definitions in interfaces However this feature has surprisingly complex interactions with the type theory of modules and even advanced module systems like Standard ML s did not consider it until recently 11 13 Day 3 User program compilation A user module MUsr is written and compiled It is checked to be compatible with IUsr and ILib The compilation of MUsr produces a linkable image LUsr No running program is generated yet because no implementation of ILib has been delivered Obstacles The code of generic library modules may have to be instantiated before the user code can be typechecked then an implementation MLib of ILib must be available to typecheck MUsr The instantiation of generic interfaces and modules performed by the client may produce unexpected type errors in the library code that were not detected by simple testing of the library 18 page 47 Some object oriented languages need to retypecheck superclass code potentially library code to verify the correct use of Self types in subclasses 20 Standard ML s transparent signatures 15 allow situations where MUsr depends on the types defined in a particular implementation of ILib therefore MUsr cannot be isolated by ILib from that implementation 13 Even when it is possible to typecheck MUsr purely