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 <reports@dcs.ed.ac.uk>,
Laboratory for Foundations of Computer Science (LFCS),
The University of Edinburgh,
JCMB, The Kings Buildings,
Mayfield Road,
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 
dependent types.

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.