Abstract: Typed lambda-calculus is an important tool in programming language research because it provides an extensible framework for studying language features both in isolation and in their relation to each other. In earlier work we introduced a predicative function calculus, XML, for modelling several aspects of the Standard ML type system. Following MacQueen, our study focussed on the use of dependent types to represent the modularity constructs of Standard ML. In addition to shedding some light on the trade-offs between language features, our analysis suggested that the first-order modules system of ML could be naturally extended to higher orders. However, whereas ML maintains a clear distinction between compile-time and run-time in both its implementation and formal semantics, the XML calculus blurs this distinction. Since static type checking is, in our view, essential to the practical utility of ML, we introduce a refinement of the XML calculus for which type checking is decidable at compile time. This calculus is based on a refinement of our earlier treatment of universes, and employs a non-standard equational theory of modules and signatures inspired by a category-theoretic account of the phase distinction.
A revised version of this report was published in the Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, January 17th-19th 1990, pp341--354. An extended version of that revision is available.Previous | Index | Next