Type Systems for Modules

ML lacks support for recursive modules. For instance, two mutually recursive functions or types must be defined within the same module. There are two common work-arounds that people use, but they are not very satisfactory: 1. Defining a “preliminary ” version of one of the modules, with some of the types and/or functions parameterized explicitly over the components it needs to refer to from the other module. When defining this other module, the recursive knot is tied explicitly inside each type or function definition (using recursion at the core language). Finally, the “normal ” version of the first module is defined. This works for both functions and datatypes, but always requires an extra module definition, which is annoying. 2. Using references in the recursive part of one module, at the end backpatching them (this is similar to how Scheme handles recursive functions). This does not require additional module definitions but does not work for types as there are no references at the type level. There are examples that cannot be encoded. Also, real recursive modules would make it possible to use polymorphic recursion, i.e., to have recursive calls of a polymorphic function at different type instantiations. Assume that the ML module system is extended with a recursive module construct rec X:S.M. Regardin