Home

Unchecked Exceptions can be Strictly More Powerful than Call/CC

Here's a little light reading for your day-after-Labor-Day (or whatever yesterday was where you live): Unchecked Exceptions can be Strictly More Powerful than Call/CC, Mark Lillibridge and Olivier Danvy, 1999, Higher-Order and Symbolic Computation.

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.

I have to say that on seeing the title I was surprised: I cut my functional teeth on Scheme and every baby Schemer sucks up the knowledge that call/cc lets you create all manner of flow control including exceptions. But, as the paper makes clear, that's not necessarily the case in a statically-typed context.

Edit: Citeseerx was not responding very well, here's an alternative URL for the paper.

By James Iry at 2008-09-02 15:39 | Functional | Lambda Calculus | Type Theory | other blogs | 9882 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

As a follow up

I was also going to post the more complete Contrasting Exceptions and Continuations, but it turns out Ehud already posted it some time ago.

By James Iry at Tue, 2008-09-02 15:58 | login or register to post comments

Interesting.

Unfortunately, citeseer appears to be down at the moment, so my comments are based only on the above summary rather than on the paper itself--but two notions of "expressiveness" seem to be confused--one being succinctness--how easily a programmer can specify an algorithm, the other being computational completeness.

The appear appears to show that adding exceptions to a sub-Turing formalism (the STLC) makes it Turing complete; whereas adding call/cc to the same formalism does not. While interesting--especially in light of conventional wisdom that call/cc can emulate any exception-handling scheme you can think of--the paper doesn't appear to reach the other notion of expressiveness (which is more useful for the programmer). And if you start with a language that is Turing-complete, the significance of the result vanishes. And there lots of other ways to extend the STLC into Turing completeness, that are far less interesting. :)

This might even be an argument for call/cc--for those cases where you want to avoid Turing-completeness; call/cc doesn't blow a big hole under the waterline. Designing a language which is useful but not TC can be tricky--it's far too easy to accidentally let a recursive construct slip in somehow.

By Scott Johnson at Tue, 2008-09-02 16:53 | login or register to post comments

Checked only

I believe it's only checked exceptions call/cc can be used to implement, precisely because it has a safety net whereas unchecked exceptions don't.

By Keith Gaughan at Tue, 2008-09-02 17:09 | login or register to post comments

Not sure

I believe it's only checked exceptions call/cc can be used to implement, precisely because it has a safety net whereas unchecked exceptions don't

I don't think that's the case.

Let's say you have a function with type A -> B. Rewrite it to accept a continuation and it becomes A -> (B -> r) -> r.

B -> r is the type of the continuation, r is a type variable that's the type of result of the continuation. If you want to add a second continuation for exception handling, the natural extension is A -> (B -> r) -> (C -> r) -> r. Here C is the type of exception that the exception handler must be able to handle.

For Java style checked exceptions C can be some union or sum type.

For unchecked exceptions, C could be a universal top exception type.

Of course, I could be missing something...

By James Iry at Tue, 2008-09-02 18:42 | login or register to post comments

Alternative URL

citeseer appears to be down at the moment

I've edited the article with an alternative URL in case others experience problems with citeseerx.

By James Iry at Tue, 2008-09-02 18:48 | login or register to post comments

dynamic-wind

James Iry wrote I have to say that on seeing the title I was surprised: I cut my functional teeth on Scheme and every baby Schemer sucks up the knowledge that call/cc lets you create all manner of flow control including exceptions.

Dynamic-wind was added to R4RS scheme because the rrrs-authors saw that the functionality, then becoming widely used in object oriented programming, could not be expressed in R3RS scheme.

By Charles Stewart at Wed, 2008-09-03 10:07 | login or register to post comments

dynamic-wind and call/cc

My impression was that dynamic-wind could almost be implemented in terms of call/cc except that then doing a call/cc into or out of the target body wouldn't provide the right guarantees about before and after thunks. This FAQ seems to say so:

Many Schemes implement both in Scheme on top of a primitive, non-"wind-safe" call-with-current-continuation. This is a particularly common implementation strategy because previous versions of the Scheme standard did not include dynamic-wind and wind-safe call-with-current-continuation. Note that implementations following this strategy must ensure that the original call-with-current-continuation is no longer reachable from application code since that could compromise the wind-safety of the entire application.

So perhaps my commentary should be amended: call/cc provides the power to create a large variety of control flow features and then provides the power to subvert them.

By James Iry at Wed, 2008-09-03 15:57 | login or register to post comments

Wind-safe continuation

How do you ensure that a continuation is wind-safe, and what does it mean?

By Denis Bredelet -jido at Wed, 2008-09-03 20:12 | login or register to post comments

Scheme promises

The how isn't something I've studied, but the what is in the documentation for dynamic-wind.

  • The dynamic extent is also entered when execution is not within the dynamic extent and a continuation is invoked that was captured (using call-with-current-continuation) during the dynamic extent.
  • It is also exited when execution is within the dynamic extent and a continuation is invoked that was captured while not within the dynamic extent.
By James Iry at Wed, 2008-09-03 22:55 | login or register to post comments

dynamic-wind and unwind-protect

The need for the BEFORE thunk in dynamic/wind is because of call/cc; without continuations, I believe that unwind-protect as per CL would provide the same functionality. Cf. Aubrey Jaffer's email to rrrs-authors, providing an operational semantics of dynamic-wind:

; "dynwind.scm", wind-unwind-protect for Scheme
; Copyright (c) 1992, Aubrey Jaffer

;This facility is a generalization of Common Lisp `unwind-protect',
;designed to take into account the fact that continuations produced by
;CALL-WITH-CURRENT-CONTINUATION may be reentered.

Studying Jaffer's implementation will prove interesting for some folks here, I think.

Postscript: Not 100% sure that dynamic-wind and unwind-protect are equi-expressive in the absence of call/cc, but I would be surprised if it were not true.

By Charles Stewart at Thu, 2008-09-04 13:40 | login or register to post comments

Kent Pitman

I have not studied it, but Kent Pitman maintains a page on UNWIND-PROTECT vs. Continuations.

By Manuel J. Simoni at Mon, 2008-09-08 14:50 | login or register to post comments

Will Clinger's two implementations

Kent Pitman's comments about Clinger's implementation are a little tricky to decipher: he doesn't discuss the revised (2005) implementation UWESC/uwesc.sch, although this is what he links to, but he only treats the "joke" (2003) version Temp/uwesc.sch (wayback machine). Clinger is not kind to Pitman's claim that unwind-protect cannot be implemented.

By Charles Stewart at Tue, 2008-09-09 14:00 | login or register to post comments

dynamic-unwind not a solution

As Kent Pitman says, dynamic-unwinds addresses a different problem. You don't want to call the unwind code at each continuation invocation and the wind code when the continuation returns if you are dealing with something like an open file.

For my part, I don't really see the need for full continuations. My continuations have a predefined scope and cannot be captured. The unwind code is called at the exit of this scope.

By Denis Bredelet -jido at Tue, 2008-09-09 13:33 | login or register to post comments

Superficial reading

A couple of superficial observations:

page 3-277: Fω extended with call/cc was shown to be sound under all the strategies except for the strategy most like ML (the call-by-value, evaluating beneath type abstractions strategy) which was shown to be unsound for full Fω. Restricting so that polymorphism can only be used on values, not general expression, restores soundness for this strategy. This restriction has since been adopted for SML where it is called the value restriction.
[...] all programs in the sound subsets must terminate. Hence, adding call/cc to Fω in a sound manner permits only recursive functions to be be written; Fω plus call/cc is therefore not Turing complete.

Does that say that adding call/cc makes Fω unsound, so they use a less powerful language? Why not use a language that can remain sound with the inclusion of call/cc and is Turing-complete with call/cc?

page 8-282: Note that because functions are first-class in λ->, exceptions may carry functional values. Our results depend on this ability.

Is a language with exceptions equivalent to a CPS language? In that case, allowing a function as exception type means that we have the equivalent of call/cc, doesn't it?

By Denis Bredelet -jido at Wed, 2008-09-03 20:09 | login or register to post comments

What it says

Does that say that adding call/cc makes Fω unsound,

From the paper

Fω extended with call/cc was shown to be sound under all the strategies ...

So, nope, it's sound, except one special case

except for the strategy most like ML (the call-by-value, evaluating beneath type abstractions strategy) which was shown to be unsound for full Fω.

So, when they tried it under ML-like semantics they had an unsound type system and all bets were off. Fortunately, the ML community already knows about that issue and how to fix the hole in SML.

Restricting so that polymorphism can only be used on values, not general expression, restores soundness for this strategy. This restriction has since been adopted for SML where it is called the value restriction.

By James Iry at Wed, 2008-09-03 23:15 | login or register to post comments