A Type System for Well-Founded Recursion

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.