Derek Dreyer

Understanding and Evolving the ML Module System Degree Type: Ph.D. in Computer Science
Advisor(s): Robert Harper and Karl Crary
Graduated: May 2005

Abstract:

The ML module system stands as a high-water mark of programming language support for data abstraction. Nevertheless, it is not in a fully evolved state. One prominent weakness is that module interdependencies in ML are restricted to be acyclic, which means that mutually recursive functions and data types must be written in the same module even if they belong conceptually in different modules. Existing efforts to remedy this limitation either involve drastic changes to the notion of what a module is, or fail to allow mutually recursive modules to hide type information from one another. Another issue is that there are several dialects of ML, and the module systems of these dialects differ in subtle yet semantically significant ways that have been difficult to account for in any rigorous way. It is important to come to a clear assessment of the existing design space and consolidate what is meant by "the ML module system" before embarking on such a major extension as recursive modules.

In this dissertation I contribute to the understanding and evolution of the ML module system by: (1) developing a unifying account of the ML module system in which existing variants may be understood as subsystems that pick and choose different features, (2) exploring how to extend ML with recursive modules in a way that does not inhibit data abstraction, and (3) incorporating the understanding gained from (1) and (2) into the design of a new, evolved dialect of ML. I formalize the language of part (3) using the framework of Harper and Stone, in which the meanings of "external" ML programs are interpreted by translation into an "internal" type system.

In my exploration of the recursive module problem, I also propose a type system for statically detecting whether or not recursive module definitions are "safe" --- that is, whether they can be evaluated without referring to one another prematurely---thus enabling more efficient compilation of recursive modules. Future work remains, however, with regard to type inference and type system complexity, before my proposal can be feasibly incorporated into ML.

Thesis Committee:
Robert Harper (Co-chair)
Karl Crary (Co-chair)
Peter Lee
David MacQueen (University of Chicago)

Jeannette Wing, Head, Computer Science Department
Randy Bryant, Dean, School of Computer Science

Keywords:
ML, module systems, type systems, functors, abstract data types, lambda calculus, recursive modules, singleton kinds