A Syntactic Type System for Recursive Modules

Abstract

A modern programming language usually provides its own module system to facilitate the development and maintenance of large-scale software. The ML module system, among others, provides powerful support for modular programming and data abstraction using nested modules, higher-order functors, and abstract types. However, it does not traditionally support recursive modules, and due to the lack of recursive modules, ML programmers often have to consolidate conceptually separate mutually recursive definitions into a single module, thus compromising modular programming. In response, several authors have recently proposed recursive module extensions to ML, some of which are successfully implemented in Moscow ML and OCaml. However, previous proposals still do not allow some important patterns of recursive modules.To reach its full power, a type system for recursive modules should address at least two technical challenges. First it needs to solve the double vision problem, which refers to an inconsistency between external and internal views of recursive modules. Second it needs to overcome the tension between practical decidability and expressivity which arises from the potential presence of cyclic type definitions caused by recursion between modules. Although type systems in previous proposals solve the double vision problem and are also decidable, they fail to typecheck common patterns of recursive modules, such as functor fixpoints, that are essential to the expressivity of the module system and the modular development of recursive modules.In this thesis, we develop a novel type system for recursive modules that solves the double vision problem and typechecks common patterns of recursive modules including functor fixpoints. First we design a type system with a type equivalence relation based on weak bisimilarity, which does not lend itself to practical implementation in general, but accommodates a broad range of cyclic type definitions. Then we identify a practically implementable fragment of the type system using a type equivalence relation based on type normalization, which is expressive enough to typecheck typical uses of recursive modules. Our approach is purely syntactic and the definition of the type system is ready for use in an actual implementation.