[Prev][Next][Index][Thread]

Dissertation on Translucent Sums Available


	My Dissertation entitled "Translucent Sums: A Foundation for
Higher-Order Module Systems" is now available via the world-wide web at
the following URL:

	http://www.research.digital.com/SRC/personal/Mark_Lillibridge/


I've included an abstract at the end of this message.  This work fleshes
out the ideas presented in an earlier POPL'94 paper by Robert Harper and
me, entitled "A type-theoretic approach to higher-order modules with
sharing".


						Best regards,
						Mark Lillibridge
						mdl@pa.dec.com
						Systems Research Center
						Digital Equipment Corporation


------------------------------ cut here ------------------------------

			Translucent Sums:
	    A Foundation for Higher-Order Module Systems

			- Mark Lillibridge


	The ease of understanding, maintaining, and developing a large
program depends crucially on how it is divided up into modules, which is
constrained by the available modular programming facilities ("module
system") of the programming language being used.  Experience with
Standard ML's module system has shown the usefulness of functions
mapping modules to modules and modules with module subcomponents.  For
example, functions over modules permit abstract data types (ADTs) to be
parameterized by other ADTs, and submodules permit modules to be
organized hierarchically.  Module systems with such facilities are
called higher-order, by analogy with higher-order functions.

	Previous higher-order module systems can be classified as either
"opaque" or "transparent."  Opaque systems totally obscure
information about the identity of type components of modules, often
resulting in overly abstract types.  This loss of type identities
precludes most interesting uses of higher-order features.  Transparent
systems, on the other hand, completely reveal type identities by
inspecting module implementations, which subverts data abstraction and
prevents separate compilation.

	In this dissertation, I describe a novel approach that avoids
these problems based on a new type-theoretic concept, the translucent
sum.  A translucent sum is a kind of weak sum that can optionally
specify the identity of its type components.  Under my approach type
identities are not determined by inspecting module implementations,
permitting separate compilation.  By default, module operations reveal
the connections between the types in their input and output modules.
However, these connections can be obscured using type coercion.  This
controlled visibility permits data abstraction where desired without
limiting the uses of higher-order features.  My approach also allows
modules to be treated as first-class values, a potentially valuable
feature.

	In order to lay out the groundwork for my new approach to
designing higher-order module systems and to demonstrate its utility, I
develop in complete detail a kernel system using my approach.  I
establish formally the theoretical properties of the system, including
soundness even in the presence of side effects.  I also show how the
system may be effectively type checked.