APPSEM Report on Theme B Year 1

Theme B: Program structuring - First year Progress Report

Coordinators: E.Moggi and M.Jones.
Partners: Chalmers (Coquand, Hughes, von Sydow), Copenhagen (Tofte), ENS (di Cosmo), Genova (Moggi), Nottingham (M. Jones, Peyton-Jones), INRIA (Mauny, Remy), QMW (Robinson).

The plan was to focus on two structuring mechanisms: modules and encapsulation of computational effects. Both have been extensively investigated in the context of functional languages. The goal is to make these structuring mechanisms language independent, through a deeper theoretical understanding of their workings.

Achievements

The major achievements in Year 1 have been on generic modules languages, and on types and constructs for multi-stage programming (this was not among the topics indicated in the WG proposal). While there have been no major achievements on encapsulation of computational effects, yet. The First annual meeting included also overview talks. Those directly related to Theme B were by M.Jones on "Program Structuring in Haskell" and X.Leroy on "A Modular Module System".

Theme B emphasizes the role of modules for programming in-the-large and "component-based programming" (as proposed in M.Jones' overview talk). In this respect it is important to support first-class modules, even at the expense of separate compilation.

Multi-stage programming is a method for improving the performance of programs through the introduction of controlled program specialization. In Theme B the goal is to provide high-level constructs, which enable the programmer to directly control specialization and execution of programs, while in Theme E the emphasis is on automatic (behind the scene) optimization. However, the two approaches share a common theoretical underpinning.

Program Structuring in Haskell (Mark Jones, Nottingham). In his overview talk M.Jones exemplifies several uses of Haskell's Constructor Classes to promote modularity and extensibility and to reduce the coupling between different sections of a program. As future goal, M.Jones suggests a new language design based on an orthogonal treatment of modules and type classes.
A Modular Module System (Xavier Leroy, INRIA). In his overview talk X.Leroy presents a simple implementation of a SML-like module system as a module parameterized by a base language and its type-checker. This demonstrates constructively the applicability of that module system to a wide range of programming languages. X.Leroy indicates as useful (but "difficult") extensions of the proposed system: recursion between modules (see work on mixin modules, below), macros and staged computations, modules systems for logical frameworks (see Theme C).
Mixin Modules (Davide Ancona and Elena Zucca, Genova). [AZ99] presents 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. First it gives an untyped version of the calculus and then a type system which is proved sound w.r.t. the reduction semantics. Expressivity of the calculus is demonstrated by giving translations of other primitive calculi into it.
Another Idealized MetaML (Eugenio Moggi, Genova and in collaboration with OGI) also related to Theme E. [MTBS99] introduces AIM, a simply typed multi-stage functional language, where one can manipulate open code (including symbolic evaluation under lambda) and close code (including execution). AIM solves elegantly the problem of finding a language providing programming facilities for both partial evaluation and run-time code generation. Indeed, AIM incorporates ideas that ultimately come from two-level languages originally proposed by N.Jones et al. and by F. and H.Nielson. [BMTS99] reports the results from a study of categorical models for multi-stage languages, and shows how a language exploiting interactions between two logical modalities is well suited for multi-stage programming.
Non-dependent Types for Modules (Claudio Russo, Edinburgh). [Rus99] presents an equivalent, but more type-theoretic, reformulation of the static semantics of SML Modules. This presentation makes clear that the concepts underlying Modules are type parameterization, type quantification and subtyping. In contrast to recent work on modules, this type theory avoids the use of first-order dependent types. The theory also supports natural generalizations to higher-order and first-class modules.

References

[AZ98] D.Ancona, E.Zucca. A Theory of Mixin Modules: Basic and Derived Operators. MSCS 8(4), 1998.
[AZ99] D.Ancona, E.Zucca. A Primitive Calculus for Module Systems. Submitted for publication, March 1999.
[BMTS99] Z.-E.-A. Benaissa, E.Moggi, W.Taha, T.Sheard. Logical Modalities and Multi-Stage Programming. Submitted for publication, March 1999.
[MTBS99] E.Moggi, W.Taha, Z.-E.-A. Benaissa, T.Sheard. An idealized MetaML: Simpler, and more expressive. In ESOP'99, LNCS, 1999.
[Rus99] C.V.Russo. Non-Dependent Types for Standard ML Modules. Submitted for publication, March 1999.
[Rus98] C.V.Russo. Types For Modules. University of Edinburgh, LFCS thesis ECS-LFCS-98-389. 1998.

Besides the interactions funded by APPSEM the following visits were relevant to Theme B: E.Moggi visits OGI (28/05-08/06/1998 - MURST and OGI funding), X.Leroy visit Genova (01-24/09/1998 - Italian CNR funding).

Changes

M.Jones has moved to OGI (Portland, OR, USA), S.Peyton-Jones has moved to MS Research (Cambridge, UK). Both are outstanding researchers with top-level expertise on Haskell. Collaboration with M.Jones (and other people at OGI) is expected to continue through other sources of funding. Therefore, we don't see the need to revise our objectives. Finally, D.Remy has agreed to replace M.Jones in the coordination of Theme B.