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 result.

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 lifting 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.