Date Added: Feb 2010
The ML module system facilitates the modular development of large programs, through decomposition, abstraction and reuse. To increase its flexibility, much work has been devoted to extending it with recursion, which is currently prohibited. The introduction of recursion certainly adds expressivity to the module system. However it also brings out non-trivial problems that a non-recursive module system does not have. In this paper, the authors address one of such problems, namely resolution of path references. Paths are how one refers to nested modules in ML. Without recursion, well-typedness guarantees termination of path resolution, in other words, they can statically determine the module that a path refers to.