A functional correspondence between monadic evaluators and abstract machines for languages with computational effects
We extend our correspondence between evaluators and abstract machines from the pure setting of the lambda-calculus to the impure setting of the computational lambda-calculus. We show how to derive new abstract machines from monadic evaluators for the computational lambda-calculus. Starting from (1) a generic evaluator parameterized by a monad and (2) a monad specifying a computational effect, we inline the components of the monad in the generic evaluator to obtain an evaluator written in a style that is specific to this computational effect. We then derive the corresponding abstract machine by closure-converting, CPS-transforming, and defunctionalizing this specific evaluator. We illustrate the construction with the identity monad, obtaining the CEK machine, and with a lifted state monad, obtaining a variant of the CEK machine with error and state. In addition, we characterize the tail-recursive stack inspection presented by Clements and Felleisen as a lifted state mound. This enables us to combine this stack-inspection monad with other monads and to construct abstract machines for languages with properly tail-recursive stack inspection and other computational effects. The construction scales to other monads-including one more properly dedicated to stack inspection than the lifted state monad-and other monadic evaluators. (c) 2005 Elsevier B.V. All rights reserved.
monads abstract machines effects lambda-calculus defunctionalization stack inspection interpreters closure conversion transformation into continuation-passing style (cps) proper tail recursion