Bluefin.Algae.DelCont

Delimited continuations

Native multi-prompt delimited continuations. These primitives let us manipulate slices of the call stack/evaluation context delimited by reset.

This module serves as a foundation for algebraic effect handlers, a more structured interface for manipulating continuations and implementing user-defined effects.

The behavior of reset and shift0 is summarized by the following equations:

reset (\_ -> pure x) = pure x
reset (\t -> C (shift0 t f)) = f (\x -> reset (\t -> C x))

where C is an evaluation context (in which t may occur), i.e., a term of the following form:

C x ::= C x >>= k      -- for any function k
      | H (\h -> C x)  -- for any handler H ∈ { reset, (`runState` s), ... }
      | x

This module ensures type safety. The rank-2 type of reset guarantees that shift0 will always have a maching reset on the stack.

References

• Delimited continuation primops (GHC proposal, implemented in GHC 9.6.1).
• Shift to Control (2004) by Chung-chieh Shan. The name shift0 follows the nomenclature in that paper.

Documentation

data PromptTag ss a s

Tag for a prompt of type Eff ss a and scope s.

reset :: forall a ss. (forall s. PromptTag ss a s -> Eff (s :& ss) a) -> Eff ss a

Run the enclosed computation under a prompt of type Eff ss a.

f : forall s. PromptTag ss a s -> Eff (s :& ss) a
-------------------------------------------------
reset (\t -> f t) : Eff ss a

The enclosed computation f is given a tag which identifies that prompt and remembers its type. The scope parameter s prevents the tag from being used outside of the computation.

A prompt (reset) delimits a slice of the call stack (or evaluation context), which can be captured with shift0. This slice, a continuation, becomes a function of type Eff ss0 b -> Eff ss a (where Eff ss0 b is the result type of shift0 at its calling site). Calling the continuation restores the slice on the stack.

shift0 :: forall s a b ss ss0. s :> ss0 => PromptTag ss a s -> (Continuation ss0 ss b a -> Eff ss a) -> Eff ss0 b

Capture the continuation up to the tagged prompt.

_ : s :> ss0
t : PromptTag ss a s
f : (Eff ss0 b -> Eff ss a) -> Eff ss a
---------------------------------------
shift0 t (\k -> f k) : Eff ss0 b

The prompt (reset) is reinserted on the stack when the continuation is called:

reset (\t -> C (shift0 t f)) = f (\x -> reset (\t -> C x))

data Continuation t s b a

Continuations are slices of the call stack, or evaluation context.

The Continuation type is abstract since not all functions Eff t b -> Eff s a represent evaluation contexts. In particular, weakenC1 is not definable for arbitrary such functions.

For example, in

reset \tag0 ->
  reset \tag1 ->
    reset \tag2 ->
      shift0 tag1 f >>= etc

shift0 captures a continuation, the slice represented by the following function:

MkContinuation \hole ->
  reset \tag1 ->
    reset \tag2 ->
      hole >>= etc

That continuation has type Continuation t s b a where Eff t b is the type of the hole, and Eff s a is the type of the result once the hole is plugged.

The second argument of shift0, f, is applied to the continuation:

reset \tag0 ->
 f (MkContinuation \hole ->
  reset \tag1 ->
    reset \tag2 ->
      hole >>= etc)

weakenC1 :: Continuation t s b a -> Continuation (e :& t) (e :& s) b a

Extend the context of a continuation.

resume :: Continuation t s b a -> Eff t b -> Eff s a

Resume a continuation with a computation under it.

continue :: Continuation t s b a -> b -> Eff s a

Resume a cancellable continuation with a result.

In other words, this converts a cancellable continuation to a simple continuation.

cancel :: Continuation t s b a -> Eff s ()

Cancel a continuation: resume by throwing a scoped exception and catch it.

The continuation SHOULD re-throw unknown exceptions. (That is guaranteed if you don't use Exception.Dynamic.)