A Functional Correspondence between Monadic Evaluators and Abstract Machines for Languages with Computational Effects

Authors

  • Mads Sig Ager
  • Olivier Danvy
  • Jan Midtgaard

DOI:

https://doi.org/10.7146/brics.v10i35.21803

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.

Downloads

Published

2003-11-06

How to Cite

Ager, M. S., Danvy, O., & Midtgaard, J. (2003). A Functional Correspondence between Monadic Evaluators and Abstract Machines for Languages with Computational Effects. BRICS Report Series, 10(35). https://doi.org/10.7146/brics.v10i35.21803