Haskell w/ delimited continuations

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Haskell w/ delimited continuations

oleg-30

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.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Haskell w/ delimited continuations

Taral
On Sat, Feb 23, 2008 at 1:05 AM,  <[hidden email]> wrote:

>  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 <[hidden email]>
"Please let me know if there's any further trouble I can give you."
    -- Unknown
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Haskell w/ delimited continuations

Taral
In reply to this post by oleg-30
On Sat, Feb 23, 2008 at 1:05 AM,  <[hidden email]> wrote:
>         reset ((\x -> x + x) (shift f f))

This one doesn't typecheck, since you can't unify the types (a -> r) and r.

--
Taral <[hidden email]>
"Please let me know if there's any further trouble I can give you."
    -- Unknown
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Haskell w/ delimited continuations

Chung-chieh Shan-2
Taral <[hidden email]> wrote in article <[hidden email]> in gmane.comp.lang.haskell.cafe:
> On Sat, Feb 23, 2008 at 1:05 AM,  <[hidden email]> 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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe