Thesis announcement: Types For Modules
I am pleased to announce the availability of my PhD thesis:
"Types For Modules"
The thesis investigates the static semantics of Standard ML Modules,
gives a type theoretic account of type generativity, discusses
separate compilation and presents natural extensions to higher-order
and first-class modules.
The thesis is available electronically from the LFCS on-line
repository of technical reports:
Paper copies of the thesis can be ordered from:
Kendal Reid <email@example.com>,
Laboratory for Foundations of Computer Science (LFCS),
The University of Edinburgh,
JCMB, The Kings Buildings,
Edinburgh EH9 3JZ,
Source code for a prototype implementation of the extensions to
higher-order and first-class modules may be downloaded from:
(For historical reasons, this code is written in Caml Light 7.x (a
dialect of ML) and requires the Caml Light 7.x compiler. The
distribution's readme file contains further instructions.)
For those without web access, I've included the thesis abstract below.
Feedback on the thesis is most welcome.
Claudio Russo (Harlequin Ltd.)
(formerly at the LFCS, University of Edinburgh).
The programming language Standard ML is an amalgam of two, largely
orthogonal, languages. The Core language expresses details of algorithms
and data structures. The Modules language expresses the modular
architecture of a software system. Both languages are statically typed,
with their static and dynamic semantics specified by a formal definition.
Over the past decade, Standard ML Modules has been the source of
inspiration for much research into the type-theoretic foundations of
modules languages. Despite these efforts, a proper type-theoretic
understanding of its static semantics
has remained elusive. In this thesis, we use Type
Theory as a guideline to reformulate the unconventional
static semantics of Modules, providing a
basis for useful extensions to the Modules language.
Our starting point is a stylised presentation of the existing static
semantics of Modules, parameterised by an arbitrary Core language. We
claim that the type-theoretic concepts underlying Modules are type
parameterisation, type quantification and subtyping. We substantiate this
claim by giving a provably equivalent semantics with an alternative, more
type-theoretic presentation. In particular, we show that the notion of
type generativity corresponds to existential quantification over types. In
contrast to previous accounts, our analysis does not involve first-order
Our first extension generalises Modules to higher-order, allowing modules
to take parameterised modules as arguments, and return them as results. We
go beyond previous proposals for higher-order Modules
by supporting a notion of type generativity.
We give a sound and complete algorithm for type-checking higher-order
Modules. Our second extension permits modules to be treated as first-class
citizens of an ML-like Core language, greatly extending the range of
computations on modules. Each extension arises from a natural
generalisation of our type-theoretic semantics.
This thesis also addresses two pragmatic concerns. First, we propose
a simple approach to the separate compilation of Modules, which is
adequate in practice but has theoretical limitations. We suggest a
modified syntax and semantics that alleviates these limitations. Second, we
study the type inference problem posed by uniting our extensions to
higher-order and first-class modules with an implicitly-typed, ML-like
Core language. We present a hybrid type inference algorithm
that integrates the classical algorithm for ML with the type-checking
algorithm for Modules.