garden

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 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, but 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.

Together, these operators characterize the idea of delimited continuations: we are able to manipulate control flow by, effectively, shifting chunks of the call stack etc into closures and beginning a new thread of control. For this reason CPS is often considered the control-flow monad and brought up when discussing parallelization and concurrency primitives.

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

Synopsis

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

Constructors

 CPS Fields(#) :: (answer -> m result) -> m result

#### Instances

Instances details
 Monad (CPS r m) Source # Instance detailsDefined in CPS Methods(>>=) :: CPS r m a -> (a -> CPS r m b) -> CPS r m b Source #(>>) :: CPS r m a -> CPS r m b -> CPS r m b Source #return :: a -> CPS r m a Source # Functor (CPS r m) Source # Instance detailsDefined in CPS Methodsfmap :: (a -> b) -> CPS r m a -> CPS r m b Source #(<\$) :: a -> CPS r m b -> CPS r m a Source # Applicative (CPS r m) Source # Instance detailsDefined in CPS Methodspure :: a -> CPS r m a Source #(<*>) :: CPS r m (a -> b) -> CPS r m a -> CPS r m b Source #liftA2 :: (a -> b -> c) -> CPS r m a -> CPS r m b -> CPS r m c Source #(*>) :: CPS r m a -> CPS r m b -> CPS r m b Source #(<*) :: CPS r m a -> CPS r m b -> CPS r m a Source # MonadIO (CPS () HIO) Source # Instance detailsDefined in Orc MethodsliftIO :: IO a -> CPS () HIO a Source # HasFork m => Alternative (CPS () m) Source # Instance detailsDefined in CPS Methodsempty :: CPS () m a Source #(<|>) :: CPS () m a -> CPS () m a -> CPS () m a Source #some :: CPS () m a -> CPS () m [a] Source #many :: CPS () m a -> CPS () m [a] Source # HasFork m => MonadPlus (CPS () m) Source # Instance detailsDefined in CPS Methodsmzero :: CPS () m a Source #mplus :: CPS () m a -> CPS () m a -> CPS () m a Source #

shift :: Monad m => ((a -> m r) -> CPS r m r) -> CPS r m a Source #

reset :: Monad m => CPS r m r -> m r Source #

# Utilities

lift :: Monad m => m a -> CPS r m a Source #