Components and modules

We propose an extension with name variables of a calculus for incremental rebinding of code introduced in previous work. Names, which can be either constants or variables, are used as interface of fragments of code with free variables. Open code can be dynamically rebound by applying a rebinding, which is an association from names to terms. Rebinding is incremental, since rebindings can contain free variables as well, and can be manipulated by operators such as overriding and renaming. By using name variables, it is possible to write terms which are parametric in their nominal interface and/or in the way it is adapted, greatly enhancing expressivity. The type system is correspondingly extended by constrained name-polymorphic types, where simple inequality constraints prevent conflicts among parametric name interfaces.

We define a framework of components based on Java-like languages, where components are binary mixin modules. Basic components can be obtained from a collection of classes by compiling such classes in isolation; for allowing that, requirements in the form of type constraints are associated with each class. Requirements are specified by the user who, however, is assisted by the compiler that can generate missing constraints essential to guarantee type safety. Basic components can be composed together by using a set of expressive typed operators; thanks to soundness results, such a composition is always type safe. The framework is designed as a separate layer that can be instantiated on top of any Java-like language; to show the effectiveness of the approach, an instantiation on a small Java subset is provided, together with a prototype implementation. Besides safety, the approach achieves great flexibility in reusing components for two reasons: (1) type constraints generated for a single component exactly capture all possible contexts where it can be safely used; (2) composition of components is not limited to conventional linking, but is achieved by means of a set of powerful operators typical of mixin modules.

We define a framework of components based on Java-like languages, where components are binary mixin modules. Basic components can be obtained from a collection of classes by compiling such classes in isolation; for allowing that, requirements in the form of type constraints are associated with each class. Requirements are specified by the user who, however, is assisted by the compiler which can generate missing constraints essential to guarantee type safety. Basic components can be composed together by using a set of expressive typed operators; thanks to soundness results, such a composition is always type safe. The framework is designed as a separate layer which can be instantiated on top of any Java-like language; a prototype implementation is available for a small Java subset. Besides safety, the approach achieves great flexibility in reusing components for two reasons: (1) type constraints generated for a single component exactly capture all possible contexts where it can be safely used; (2) composition of components is not limited to conventional linking, but is achieved by means of a set of powerful operators typical of mixin modules.

We present SmartJavaMod, a language of mixin modules supporting compositional compilation, and constructed on top of the Java language. More in detail, this means that basic modules are collections of Java classes which can be typechecked in isolation, inferring constraints on missing classes and allowing safe reuse of the module in as many contexts as possible. Furthermore, it is possible to write structured module expressions by means of a set of module operators, and a type system at the module level ensures type safety, in the sense that we can always reduce a module expression to a well-formed collection of Java classes. What we obtain is a module language which is extremely flexible and allows the encoding (without any need of enriching the core level, that is, the Java language) of a variety of constructs supporting software reuse and extensibility.

Dynamic rebinding is the ability of changing the definitions of names at execution time. While dynamic rebinding is clearly useful in practice, and increasingly needed in modern systems, most programming languages provide only limited and ad-hoc mechanisms, and no adequate semantic understanding currently exists. Here, we provide a simple and powerful mechanism for dynamic rebinding by means of a calculus of mixin modules (mutually recursive modules allowing redefinition of components) where, differently from the traditional approach, module operations can be performed after selecting and executing a module component: in this way, execution can refer to virtual components, which can be rebound when module operators are executed. In particular, in our calculus module operations are performed on demand, when execution would otherwise get stuck. We provide a sound type system, which ensures that execution never tries to access module components which cannot become available, and show how the calculus can be used to encode a variety of real-world dynamic rebinding mechanisms.

The first part of the paper gives a brief overview of meta-programming, in particular program generation, and its use in software development. The second part introduces a basic calculus, related to FreshML, that supports program generation (as described through examples and a translation of MetaML into it) and programming in-the-large (this is demonstrated by a translation of CMS into it).

Building on our previous work, we present a simple module calculus where execution steps of a module component can be interleaved with reconfiguration steps (that is, reductions at the module level), and where execution can partly control precedence between these reconfiguration steps. This is achieved by means of a low priority link operator which is only performed when a certain component, which has not been linked yet, is both available and really needed for execution to proceed, otherwise precedence is given to the outer operators. We illustrate the expressive power of this mechanism by a number of examples. We ensure soundness by combining a static type system, which prevents errors in applying module operators, and a dynamic check which raises a linkage error if the running program needs a component which cannot be provided by reconfiguration steps. In particular no linkage errors can be raised if all components are potentially available.

We propose an innovative type system for Java-like languages which can infer the minimal set of assumptions guaranteeing type correctness of a class c, and generate (abstract) bytecode for c, by inspecting the source code of c in isolation. We prove the above properties of our type system by showing that it has principal typings. As well known, principal typings support compositional analysis, whereby a collection of classes can be safely linked together without further inspection of the classes' code, provided that each class has been typechecked in isolation (intra-checking), and that the mutual class assumptions are satisfied (inter-checking). We also develop an algorithm for inter-checking, and prove it correct.

We define a basic calculus for name management, which is obtained by an appropriate combination of three ingredients: extensible records (in a simplified form), names (as in FreshML), computational types (to allow computational effects, including generation of fresh names). The calculus supports the use of symbolic names for programming in-the-large, e.g. it subsumes Ancona and Zucca's calculus for module systems, and for meta-programming (but not the intensional analysis of object level terms supported by FreshML), e.g. it subsumes (and improves) Nanevski and Pfenning's calculus for meta-programming with names and necessity. Moreover, it models some aspects of Java's class loaders.

A recent paper proposes a calculus for modeling dynamic linking independently of the details of a particular programming environment. Here we use a particular instantiation of this calculus to encode a toy language, called MCL, which provides an abstract view of the mechanism of dynamic class loading with multiple loaders as in Java. The aim is twofold. On one hand, we show the effectiveness of the calculus in modeling existing loading and linking policies. On the other hand, we provide a simple formal model which allows a better understanding of Java-like loading mechanisms and also shows an intermediate solution between the rigid approach based only on the classpath and that which allows arbitrary user-defined loaders, which can be intricate and error-prone.

Modern programming environments such as those of Java and C# support dynamic loading of software fragments. More in general, we can expect that in the future systems will support more and more forms of interleaving of reconfiguration steps and standard execution steps, where the software fragments composing a program are dynamically changed and/or combined on demand and in different ways. However, existing kernel calculi providing formal foundations for module systems are based on a static view of module manipulation, in the sense that open code fragments can be flexibly combined together, but all module operators must be performed once for all before starting execution of a program, that is, evaluation of a module component. The definition of clean and powerful module calculi supporting lazy module operators, that is, operators which can be performed after the selection of some module component, is still an open problem. Here, we provide an example in this direction (the first at our knowledge), defining DCMS, an extension of the Calculus of Module Systems where module operators can be performed at execution time and, in particular, are executed on demand, that is, only when needed by the executing program. In other words, execution steps, if possible, take the precedence over reconfiguration steps. The type system of the calculus, which is proved to be sound, relies on a dependency analysis which ensures that execution will never try to access module components which cannot become available by performing reconfiguration steps.

We define a calculus for investigating the interactions between mixin modules and computational effects, by combining the purely functional mixin calculus CMS with a monadic metalanguage supporting the two separate notions of simplification (local rewrite rules) and computation (global evaluation able to modify the store). This distinction is important for smoothly integrating the CMS rules (which are all local) with the rules dealing with the imperative features. In our calculus mixins can contain mutually recursive computational components which are explicitly computed by means of a new mixin operator whose semantics is defined in terms of a Haskell-like recursive monadic binding. Since we mainly focus on the operational aspects, we adopt a simple type system like that for Haskell, that does not detect dynamic errors related to bad recursive declarations involving effects. The calculus serves as a formal basis for defining the semantics of imperative programming languages supporting first class mixins while preserving the CMS equational reasoning.

We define a calculus for modeling dynamic linking independently of the details of a particular programming environment. The calculus distinguishes at the language level the notions of software configuration and execution, by introducing separate syntactic notions of linkset expression and command, respectively. A reduction step can be either a simplification of a linkset expression, or the execution of a command w.r.t. a specific underlying software configuration denoted by a linkset expression; because of dynamic linking, these two kinds of reductions are interleaved. The type system of the calculus, which is proved to be sound, relies on an accurate dependency analysis for ensuring type safety without losing the advantages offered by dynamic linking.

We present CMS, a simple and powerful calculus of modules supporting mutual recursion and higher order features, which can be instantiated over an arbitrary core calculus satisfying standard assumptions. The calculus allows to express a large variety of existing mechanisms for combining software components, including parameterized modules like ML functors, extension with overriding of object-oriented programming, mixin modules and extra-linguistic mechanisms like those provided by a linker. Hence CMS can be used as a paradigmatic calculus for modular languages, in the same spirit the lambda calculus is used for functional programming. As usual, we first present an untyped version of the calculus and then a type system; we prove the confluence, progress and subject reduction properties. Then, we show how it is possible to define a derived calculus of mixin modules directly in terms of CMS and to encode other primitive calculi (the lambda calculus and the Abadi-Cardelli's object calculus). Finally, we consider the problem of introducing a subtype relation for module types.

Mixins are modules which may contain deferred components, i.e. components not defined in the module itself; moreover, in contrast to parameterized modules (like ML functors), they can be mutually dependent and allow their definitions to be overridden. In a preceding paper we have defined syntax and denotational semantics of a kernel language of mixin modules. Here, we take instead an axiomatic approach, giving a set of algebraic laws expressing the expected properties of a small set of primitive operators on mixins. Interpreting axioms as rewriting rules, we get a reduction semantics for the language and prove the existence of normal forms. Moreover, we show that the model defined in the earlier paper satisfies the given axiomatization.

We present JavaMod, a true module system constructed on top of a Java-like language. More in detail, this means that basic modules are collections of Java classes and specify in their interface the imported and exported classes with their types; furthermore, it is possible to write structured module expressions by means of a set of module operators and a type system at the module level ensures type safety. In designing such a type system, one has to face non trivial problems, notably the fact that a module M which extends an imported class C can be correctly combined only with modules exporting a class C which, besides providing the expected services, causes no interferences with its subclasses defined in M. What we obtain is a module language which is extremely flexible and allows to express (without any need of enriching the syntax of the core level, that is, the Java language), for instance, generic types as in Pizza and GJ, mixin classes (that is, subclasses parametric in the direct superclass) and mutually recursive class definitions split in independent modules.

In this paper we show how it is possible to define a rather rich language of mixin modules suitable for combining together large logic programs without changing the underlying logic. The type and reduction rules for the language are presented in a somehow informal way, whereas more emphasis is given to the usefulness of the constructs from the programming point of view and to the comparison with other proposals for modular logic programming found in the literature.

We define the language of mixin modules MIX(FL) with the aim of providing foundations for the design of module systems supporting mixins. Several working examples are presented showing the benefits of the use of mixins and overriding in module systems. The language is strongly typed and supports separate compilation. The denotational semantics of the language is based on an algebraic approach and is parametric in the semantics of the underlying core language. Hence, even though the language is defined on top of a specific core language, other kinds of core languages could be considered as well.

We present a simple and powerful calculus of modules supporting mutual recursion and higher order features. The calculus allows to encode a large variety of existing mechanisms for combining software components, including parameterized modules like ML functors, extension with overriding of object-oriented programming, mixin modules and extra-linguistic mechanisms like those provided by a linker. As usual, we first present an untyped version of our calculus and then a type system which is proved sound w.r.t. the reduction semantics; moreover we give a translation of other primitive calculi.

Mixins are modules in which some components are deferred, i.e. their definition has to be provided by another module. Moreover, differently from parameterized modules (like ML functors), mixin modules can be mutually dependent and their composition supports redefinition of components (overriding). In this paper, we present a formal model of mixins and their basic composition operators. These operators can be viewed as a kernel language with clean semantics in which to express more complex operators of existing modular languages, including variants of inheritance in object oriented programming. Our formal model is given in an "institution independent" way, i.e. is parameterized by the semantic framework modeling the underlying core language.

We propose a new way of handling imperative features in the algebraic approach to composition of software modules, meant in its abstract categorical formulation. The basic idea is to consider, instead of a global state, orthogonal to the modular structure, the local state of a module as the collection of those components which have no associated definition but an extension which may vary dynamically. Following this intuition, composition of modules via classical operators like merge, renaming and hiding involves composition of the corresponding states, allowing one to give a truly compositional semantics of module languages. Thanks to the abstract categorical formulation, we are able to define a canonical construction of a framework for modules with state starting from a framework with no imperative features. This provides the theoretical basis for designing languages of modules with state in a way independent of the underlying core language.

In this thesis we present two formal frameworks for modeling modular languages. Following a modular approach, we separate the module and the core level of a modular language. On the linguistic side, this corresponds to define a kernel module language parametric in the underlying core language. On the semantic side, this corresponds to build a model part (in the sense of institutions), on top of a standard module framework. The standard module framework is a model part, too, satisfying some additional properties and intended as the formal counterpart of the core language. The first formal framework we propose deals with the notion of state, an essential component of modules in imperative languages. The second one is concerned with a notion of module, called mixin, which includes those of generic module and abstract class. In both cases, we present two canonical constructions yielding a formal framework where models denote modules with state and mixins, respectively, and we define a set of primitive operations over them.

Mixins are modules which may contain deferred components, i.e. components not defined in the module itself, and allow definitions to be overridden. We give an axiomatic definition of a set of operations for mixin combination, corresponding to a variety of constructs existing in programming languages (merge, hiding, overriding, functional composition, ...). In particular, we show that they can all be expressed in terms of three primitive operations (namely, sum, reduct and freeze), which are characterized by a small set of axioms. We show that the given axiomatization is sound w.r.t. to a model provided in some preceding work. Finally, we prove the existence of anormal form for mixin expressions.

We show that many different overriding operators present in programming languages can be expressed, adopting a mixin-based framework, in terms of three basic operators. In particular we propose two orthogonal classifications: strong (the overridden definition is canceled) or weak (the overridden definition still remains significant, as in Smalltalk's super feature), and preferential (priority to one of the two arguments) or general. We formalize the relation between all these versions. Our analysis and results are not bound to a particular language, since they are formulated within an algebraic framework for mixin modules which can be instantiated over different core languages.

We present an algebraic formalization of the notion of mixin module, i.e. a module where the definition of some components is deferred. Moreover, we define a set of basic operators for composing mixin modules, intended to be a kernel language with clean semantics in which to express more complex operators of existing modular languages, including variants of inheritance in object oriented programming. The semantics of the operators is given in an institution independent way, i.e. is parameterized on the semantic framework modeling features of the underlying core language.

We present a module algebra interpreted in the model of dynamic data-types. A data-type with state, or dynamic data type, is a data type in which the interpretation of operation symbols is depending on the internal state, which may change during the time. We formalize the above notion by a new mathematical structure, called object structure. From the point of view of programming languages, an object structure is the overall semantic value (the denotation) of a software module in an imperative context: Ada packages, Modula-2 modules and objects of object based languages can be thought as syntactic counterparts of object structures. Thus a first result of our approach is an abstract and natural definition of the semantic value of a whole module. A further result that we want to achieve is this semantics to be truly compositional, i.e. operations of composing modules to be interpreted as operations of object structures at the semantic level. We illustrate that by giving syntax and semantics of a module language which is parametric in the concrete syntax used for defining methods and components of the state. The introduction of state makes necessary to review the semantics of classical operators as given in a standard algebraic setting. In particular, we introduce a distinction between the visible and the internal signature of an object structure, which is essential for defining a reduct operation, hence for modelling export/hiding operators. Composition of visible signatures must be propagated to internal signatures in order to keep unchanged hidden components modulo renaming; this corresponds to consider co-products of particular diagrams in the category of signatures.