Maintainer | gatlin@niltag.net |
---|---|
Stability | experimental |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
CPS
Description
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 #