Haskell w/ delimited continuations

Call-by-name lambda-calculus is strictly more expressive (in Felleisen sense) than call-by-value lambda-calculus, and the call-by-need (aka, lazy) lambda-calculus is observationally equivalent to the call-by-name. One can add shift/reset to any of these calculi (CBV shift/reset is most known; there are several CBN shift/reset, including the one I'm particularly attached to; in principle one can add shift/reset to call-by-need). Adding control effects (shift/reset) changes the expressivity results. Now all three calculi are distinct and none subsumes the other. For example, the expression reset( (\x -> 1) (abort 2)) evaluates to 1 in call-by-name and evaluate to 2 in call-by-value. The expression reset ((\x -> x + x) (shift f f)) has the type int->int in call-by-need (it is a function \x -> x + x) and it has the type int->int->int in call-by-name (and it is the curried addition function). The fact that call-by-need is no longer observationally equivalent to call-by-name and sharing becomes observable is the most distressing. It disables many optimizations GHC is allowed to do. Types help: there are call-by-name calculi with shift/reset with effect typing; one can look at the type and see what control effect an expression may make. That will still permit GHC optimize pure expressions and leave effectful expressions as they are. Alas, that type system is complex and I don't think inference is decidable there due to the presence of subtyping (one must annotate at least some of the binders with types, in particular, the binders of shift). It seems the simplest solution is to confine shift/reset to a monad. Regarding purity: the obligatory reference is Amr Sabry. What is a Purely Functional Language? In J. Functional Programming, 8(1), 1-22, Jan. 1998. http://www.cs.indiana.edu/~sabry/papers/purelyFunctional.ps Please see the definition 4.7. As Matthias Blume said, a bit informally, evaluation of a pure expression should not depend on CBN or CBV or some other such strategy. By this definition, an expression that involves shift/reset is not pure, as the above examples demonstrate.

On Sat, Feb 23, 2008 at 1:05 AM,
Adding control effects (shift/reset) changes the expressivity results. Now all three calculi are distinct and none subsumes the other. For example, the expression reset( (\x -> 1) (abort 2)) evaluates to 1 in call-by-name and evaluate to 2 in call-by-value. The expression reset ((\x -> x + x) (shift f f)) has the type int->int in call-by-need (it is a function \x -> x + x) and it has the type int->int->int in call-by-name (and it is the curried addition function).
Aha. Okay, so shift/reset exposes evaluation order, amongst other
things. Hm... thank you very much!
--
Taral

Taral
On Sat, Feb 23, 2008 at 1:05 AM,
wrote: reset ((\x -> x + x) (shift f f))
This one doesn't typecheck, since you can't unify the types (a -> r) and r.
Some type systems for delimited continuations, such as Danvy and Filinski's (http://www.daimi.au.dk/~danvy/Papers/fatc.ps.gz; DIKU TR 89/12), allows changing the answer type and admits this code. -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig God exists since mathematics is consistent, and the devil exists since its consistency cannot be proved. -- Hermann Weyl.
participants (3)
-
Chung-chieh Shan
-
oleg@okmij.org
-
Taral