New Generation Computing, 20(2002)53-73
Ohmsha, Ltd. and Springer-Verlag

A Unifying Approach to Goal-directed Evaluation

Olivier DANVY, Bernd GROBAUER and Morten RHIGER
BRICS*, Department of Computer Science, University of Aarhus
Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark

{danvy,grobauer,mrhiger}@brics.dk

Received 1 June 2001
Revised manuscript received 17 July 2001

Abstract

Goal-directed evaluation, as embodied in Icon and Snobol, is built on the notions of backtracking and of generating successive results, and therefore it has always been something of a challenge to specify and implement. In this article, we address this challenge using computational monads and partial evaluation.
We consider a subset of Icon and we specify it with a monadic semantics and a list monad. We then consider a spectrum of monads that also fit the bill, and we relate them to each other. For example, we derive a continuation monad as a Church encoding of the list monad. The resulting semantics coincides with Gudeman's continuation semantics of Icon.
We then compile Icon programs by specializing their interpreter (i.e., by using the first Futamura projection), using type-directed partial evaluation. Through various back ends, including a run-time code generator, we generate ML code, C code, and Ocaml byte code. Binding-time analysis and partial evaluation of the continuation-based interpreter automatically give rise to C programs that coincide with the result of Proebsting's optimized compiler.

* Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

Keywords: (Type-directed) Partial Evaluation, Computational Monads, Continuations, (Run-time) Code Generation, Code Templates.

[Back]