Theme B: Program structuring - First year Progress Report
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.
- Coordinators: E.Moggi and M.Jones.
Chalmers (Coquand, Hughes, von Sydow),
ENS (di Cosmo),
Nottingham (M. Jones, Peyton-Jones),
INRIA (Mauny, Remy),
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.
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
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
- 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
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).
- [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,
- [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.
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