 Continuations (and call/cc) in Haskell
started 1/3/2004; 4:03:49 AM - last post 1/5/2004; 5:25:30 PM
|
|
Ehud Lamm - Continuations (and call/cc) in Haskell 
1/3/2004; 4:03:49 AM (reads: 10088, responses: 4)
|
|
|
|
Carlos Scheidegger - Re: Continuations (and call/cc) in Haskell
1/3/2004; 7:37:50 AM (reads: 611, responses: 0)
|
|
|
(Minor english edits)
Similar discussion on LtU not long ago. The same FPCA'95 paper by Gunther, Riecke and Remy is cited.
In the Haskell thread, there have been some examples of bad interactions between RT and call/cc, but is there any published theoretical result concerning this? I'd like to read them.
A more general, but related question: I've seen some proofs that go "control operator X can be implemented in terms of control operator Y", but I don't recall seeing any proofs that go "X cannot be implemented in terms of Y". Are there any published results of those?
This would imply a partial order on the control operators, and we'd have a firmer notion of expressiveness of them. The problem seems to be how to mix and match these control operators with the presence of state and higher-order syntax.
|
|
Neel Krishnaswami - Re: Continuations (and call/cc) in Haskell
1/3/2004; 7:51:38 AM (reads: 608, responses: 0)
|
|
|
Take a look at Andrzej Filinski's PhD thesis, Controlling Effects -- in it, he shows how any monadic effect can be described in terms of call/cc and a reference cell.
So if you want to find control operators that can't be expressed in terms of call/cc and a reference, then you need to find one that can't be given a monadic formulation; possibly some versions of the stack-inspection primitives in aspect-oriented programming would qualify.
|
|
Oleg - Re: Continuations (and call/cc) in Haskell
1/5/2004; 3:29:36 PM (reads: 340, responses: 0)
|
|
Carlos Scheidegger wrote:
I've seen some proofs that go "control operator X can be implemented
in terms of control operator Y", but I don't recall seeing any proofs
that go "X cannot be implemented in terms of Y". Are there any
published results of those?
Yes, of course. The original shift/reset paper "Abstracting Control"
by Danvy and Filinski implies a number of such inexpressibility
results.
For example, call/cc in a language without mutations cannot
express shift/reset [see
citeseer.nj.nec.com/felleisen90expressive.html for the definition of
'express' used here].
The reason for that is simple: CPS of an applicative mutation-free
program with call/cc is a tail-call program. OTH, CPS of an
applicative program with shift/reset generally includes non-tail
calls.
An applicative program with shift/reset requires two CPS
transformations to bring it into a tail-call form. It is known (see
the messages on the Haskell list thread that started this discussion)
that call/cc alone cannot emulate mutation. Therefore, if we have a program
with mutations and call/cc, we need one CPS-like transformation to
explicitly thread the state (and thus convert a program with
mutations into a purely applicative form), and another CPS
transformation to eliminate call/cc. If we call a tail-index of a
program the number of CPS transformations needed to turn it into a
tail-call form, then
- an applicative tail-call program has the index of 0
- a general applicative program with or without call/cc
has the index of 1
- a program with assignments and call/cc has the index of 2
- an applicative shift/reset program has the index of 2, in
general.
Higher-order shift/reset introduced in the Danvy/Filinski paper have
larger indices. Thus a higher-order shift/reset is inexpressible with
lower-order shift/resets.
|
|
Carlos Scheidegger - Re: Continuations (and call/cc) in Haskell
1/5/2004; 5:25:30 PM (reads: 326, responses: 0)
|
|
|
Thank you so much, Oleg and Neel, for the great pointers. This was exactly what I was looking for.
So many nice PLT readings, so little time!
|
|
|
|