Higher-Order and Symbolic Computation, 12(1)75-104
Unchecked Exceptions Can Be Strictly More Powerful Than Call/CCMark Lillibridge, Systems Research Center, Compaq Computer Corporation, 130 Lytton Avenue, Palo Alto, CA 94301
|
Abstract: We demonstrate that in the context of
statically-typed purely-functional lambda calculi without recursion,
unchecked exceptions (e.g., SML exceptions) can be strictly more
powerful than call/cc. More precisely, we prove that a natural
extension of the simply-typed lambda calculus with unchecked
exceptions is strictly more powerful than all known sound extensions
of Girard's F_omega (a superset of the simply-typed lambda calculus) with
call/cc. This result is established by showing that the first
language is Turing complete while the later languages permit only a
subset of the recursive functions to be written. We show that our
natural extension of the simply-typed lambda calculus with unchecked
exceptions is Turing complete by reducing the untyped lambda calculus
to it by means of a novel method for simulating recursive types using
unchecked-exception?returning functions. The result concerning
extensions of F_omega with call/cc stems from previous work of the author
and Robert Harper.
Keywords: studies of programming constructs, control primitives, exceptions, recursion, lambda-calculus, type theory, functional programming |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)