In the interest of designing a recursive module extension to ML that
is as simple and general as possible, we propose a novel type system
for general recursion over effectful expressions. The presence of
effects seems to necessitate a backpatching semantics for recursion
based on Scheme's. Our type system ensures statically that recursion
is well-founded (that the body of a recursive expression will evaluate
without attempting to access the undefined recursive variable), which
avoids some unnecessary run-time costs associated with backpatching.
To ensure well-founded recursion in the presence of multiple recursive
variables and separate compilation, we track the usage of individual
recursive variables, represented statically by "names". So that
our type system may eventually be integrated smoothly into ML's,
reasoning involving names is only required inside code that uses our
recursive construct and does not need to infect existing ML code.
