Typed dynamic control operators for delimited continuations

Abstract

We study the dynamic control operators for delimited continuations, Control and Prompt. Based on recent developments on purely functional CPS translations for them, we introduce a polymorphically typed calculus for these control operators which allows answer-type modification. We show that our calculus enjoys type soundness and is compatible with the CPS translation. We also show that the typed dynamic control operators can macro-express the typed static ones (Shift and Reset), while the converse direction is not possible, which exhibits a sharp contrast with the type-free case. © 2008 Springer-Verlag Berlin Heidelberg.