Exceptions, continuations and macro-expressiveness

Abstract

This paper studies the the problem of expressing exceptions using first-class continuations in a functional-imperative language. Themain result is that exceptions cannot be macro-expressed using first-class continuations and references (contrary to “folklore”). This is shown using two kinds of counter example. The first consists of two terms whichare equivalent with respect to contexts containing continuations and references,but which can be distinguished using exceptions. It is shown,however, that there are no such terms which do not contain callcc.However, there is a Π1 sentence of first-order logic which is satisfied when interpreted in the domain of programs containing continuations and references but not satisfied in the domain of programs with exceptions and references. This is used to show that even when callcc isomitted from the source language, exceptions still cannot be expressed using continuations and references.