A Functional Correspondence between Monadic Evaluators and Abstract
Machines for Languages with Computational Effects
Mads Sig Ager
November 2003 |
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. Specifically, we show how to derive new
abstract machines from monadic evaluators for the computational
lambda-calculus. Starting from a monadic evaluator and a given monad, we
inline the components of the monad in the evaluator and we derive the
corresponding abstract machine by closure-converting, CPS-transforming, and
defunctionalizing this inlined interpreter. We illustrate the construction
first with the identity monad, obtaining yet again the CEK machine, and then
with a state monad, an exception monad, and a combination of both.
In addition, we characterize the tail-recursive stack inspection presented by Clements and Felleisen at ESOP 2003 as a canonical state monad. Combining this state monad with an exception monad, we construct an abstract machine for a language with exceptions and properly tail-recursive stack inspection. The construction scales to other monads--including one more properly dedicated to stack inspection than the state monad--and other monadic evaluators Available as PostScript, PDF, DVI. |