A Type System for Well-Founded Recursion

Derek Dreyer

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


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.

Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:42
Maintainer Xavier.Leroy@inria.fr.
Start Conference Manager
Conference Systems