|
A Functional Correspondence between Monadic Evaluators and Abstract
Machines for Languages with Computational Effects
Mads Sig Ager
December 2004 |
Abstract:
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
first with the identity monad, obtaining the CEK machine, and then with a
lifting monad, a state monad, and with a lifted state monad, obtaining
variants of the CEK machine with error handling, state and a combination of
error handling and state.
In addition, we characterize the tail-recursive stack inspection presented by Clements and Felleisen as a lifted state monad. 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. Available as PostScript, PDF, DVI. |