Unchecked Exceptions Can Be Strictly More Powerful Than Call/CC |
| |
Authors: | Lillibridge Mark |
| |
Affiliation: | (1) 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 (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 with call/cc stems from previous work of the author and Robert Harper. |
| |
Keywords: | studies of programming constructs control primitives exceptions recursion -calculus" target="_blank">gif" alt="lambda" align="BASELINE" BORDER="0">-calculus type theory functional programming |
本文献已被 SpringerLink 等数据库收录! |
|