University of Cambridge

Logic
&
Semantics

Types for Modules

By Claudio Russo (10th December 1999)

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 talk, I use Type Theory to recast the unconventional static semantics of Modules in more familiar terms, providing a basis for useful extensions to the language.

I will first present an equivalent, but more type-theoretic, reformulation of the static semantics of Modules. This presentation makes clear that the concepts underlying Modules are type parameterisation, type quantification and subtyping. In contrast to previous accounts, this type theory avoids the use of first-order dependent types.

Building on previous work by Biswas, my first extension generalises Modules to higher-order, allowing modules to take parameterised modules as arguments, and return them as results. This proposal supports a notion of type generativity.

My 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 as a natural generalisation of the type-theoretic semantics.

The talk will focus on the underlying concepts, motivated by programming examples. Details of the type systems and typing algorithms may be found in my PhD thesis "Types For Modules".

LS Home page or Talks in 1999/2000