Maintainer | gatlin@niltag.net |
---|---|

Stability | experimental |

Safe Haskell | Safe-Inferred |

Language | Haskell2010 |

# A prologue to continuations

For any type `A`

, its *continuation* is some arrow `A -> ⊥`

, eg, a function
which consumes it as an argument.

*Continuation passing style* is a programming pattern where every term is a
function with at least one argument, a continuation for its *answer* (eg,
`return`

is an explicit argument).

Because a function may not actually return `⊥`

(in fact that is perhaps
literally the only type that is not a legal return type), in CPS we replace it
with some *result* type.

Hence, a `CPS r m a`

is a term that internally possesses an `a`

(or the
potential for one) which awaits some *continuation* to transform it into a
`r`

esult.

In this implementation the true result type may be a type of any kind, eg a
type-level numeral or a symbol kind, or maybe a `Constraint`

.
A *modifier* type `m :: k -> Type`

serves both to ground the result in a type.
It also presents an opportunity to separate an effect-ful type from its base
value so they may be manipulated separately.
Eg, if `m ~ IO`

, then by `lift`

ing a term `IO r`

into `CPS r IO a`

we
effectively decouple the `IO`

from the `r`

.

This is taken advantage of in the WhyNot module: a carefully defined and
constrained `m`

can allow for statically verifiable effect polymorphism.

When a given term's `answer`

is the same as its `result`

, and `m`

is a `Monad`

,
then `reset`

can evaluate the `CPS`

computation result in the underlying monad
context of `m`

.
As well you may `shift`

the suspended program continuation onto the stack as an
argument to be resumed later via application.

*Nota bene*: while this is certainly imprecise, incomplete, and probably
incorrect, my main objective is more intuition than absolute proof.

# Delimited Continuation Monad Transformer

newtype CPS (result :: k) (m :: k -> Type) (answer :: Type) Source #