A module system with applicative functors and recursive path references

When developing a large software program, it is useful to decompose the program into smaller parts and to reuse them in different contexts. Many modern programming languages provide some forms of module systems to facilitate such factoring of programs. The ML module system is well-known for its flexibility in program structuring. A programmer can factor programs into hierarchy using nested structures and can define functors, which are functions over modules, to reuse program codes. Moreover, signatures, which represent types of modules, allow the programmer to control abstraction of modules. In spite of this flexibility, modules cannot be defined recursively in ML, since dependencies between modules must accord with the order of definitions. A complex program may be naturally decomposed into recursive modules. Yet, this constraint of ML will force the programmer to consolidate conceptually separate components into a single module, intruding on modular programming. Introducing recursive modules is a natural way out of this predicament. Existing proposals, however, vary in expressiveness and verbosity. In this paper, we propose a type system for recursive modules, which can infer their signatures. Opaque signatures can also be given explicitly, to provide type abstraction either inside or outside the recursion. The type system is decidable, and is sound for a call-by-value semantics.