The indexed state monad is not the only indexed monad out there; it's not even the only useful one. In this tutorial, we will explore another indexed monad, this time one that encapsulates the full power of delimited continuations: the indexed continuation monad.
The relationship between the indexed and regular state monads holds true as well for the indexed and regular continuation monads, but while the indexed state monad allows us to keep a state while changing its type in a type-safe way, the indexed continuation monad allows us to manipulate delimited continuations while the return type of the continuation block changes arbitrarily. This, unlike the regular continuation monad, allows us the full power of delimited continuations in a dynamic language like Scheme while still remaining completely statically typed.
First, some preliminary boilerplate:
Haskell:
module IndexedCont where
import Prelude hiding (fmap, (>>=), (>>), return)
Scala:
package indexedCont
C#:
using System;
public namespace IndexedCont
{
The indexed continuation monad has a final return type r
, an intermediate output type o
, and a contained value type a
. We eventually will want a result of type r
back, so we implement the indexed continuation monad as a function with a return type of r
. But what should our function take as a parameter? Why, the continuation we want access to, of course! That continuation will require a value of type a
(the value that our particular computation is producing) and return a value of type o
(the intermediate result of the continuation we are dealing with), so we implement it simply as a function from a
to o
. That means that the full implementation type of the indexed continuation monad is that of a function that takes a function from a
to o
and returns a value of type r
:
Haskell:
newtype ICont r o a = ICont { runICont :: (a -> o) -> r }
runIContId :: ICont r o o -> r
runIContId = flip runICont id
Scala:
final class ICont[+R, -O, +A](val run: (A => O) => R) extends IContIMonadOps[R, O, A] {
def runId[I >: A <: O]: R = run { (x: I) => x }
}
object ICont extends IContIMonadFuncs with IContFuncs {
def apply[R, O, A](f: (A => O) => R): ICont[R, O, A] = new ICont[R, O, A](f)
}
C#:
public delegate R ICont<out R, in O, out A>(Func<A, O> k);
public static class ICont
{
public static R Run<R, O, A>(this ICont<R, O, A> a, Func<A, O> k)
{
return a(k);
}
public static R RunId<R, O>(this ICont<R, O, O> a)
{
return a((O x) => x)
}
Since we want to be able to use each language's syntactic support for monad notation, we will implement the requisite monadic operations: unit
, map
, join
, and bind
in all three languages, as well as then
and fail
in Haskell and bindMap
in C#:
Haskell:
-- unit
return :: a -> ICont r r a
return x = ICont ($ x)
-- map
fmap :: (a -> b) -> ICont r o a -> ICont r o b
fmap f (ICont c) = ICont $ \k -> c $ k . f
-- join
join :: ICont r i (ICont i o a) -> ICont r o a
join (ICont c) = ICont $ \k -> c (`runICont` k)
-- bind
(>>=) :: ICont r i a -> (a -> ICont i o b) -> ICont r o b
ICont c >>= f = ICont $ \k -> c $ \x-> f x `runICont` k
-- then
(>>) :: ICont r i a -> ICont i o b -> ICont r o b
ICont c1 >> ICont c2 = ICont $ \k -> c1 $ \_ -> c2 k
-- fail
fail :: String -> ICont r o a
fail str = error str
Scala:
private[indexedCont] sealed trait IContMonadFuncs { this: ICont.type =>
// unit
def point[R, A](x: A): ICont[R, R, A] = ICont { k => k(x) }
}
private[indexedCont] sealed trait IContMonadOps[+R, -O, +A] { this: ICont[R, O, A] =>
// map
def map[B](f: A => B): ICont[R, O, B] = ICont { k => run(f andThen k) }
// join
def flatten[E, B >: A <: ICont[O, E, B]]: ICont[R, E, B] = ICont { k => run { _.run(k) } }
// bind
def flatMap[E, B](f: A => ICont[O, E, B]): ICont[R, E, B] = ICont { k => run { x => f(x).run(k) } }
}
C#:
// unit
public static ICont<R, R, A> ToICont<R, A>(this A x)
{
return ((Func<A, R> k) => k(x));
}
// map
public static ICont<R, O, B> Select<R, O, A, B>(this ICont<R, O, A> c, Func<A, B> f)
{
return ((Func<B, O> k) => c.Run((A x) => k(f(x))));
}
// join
public static ICont<R, O, A> Flatten<R, I, O, A>(this ICont<R, I, ICont<I, O, A>> c1)
{
return ((Func<A, O> k) => c1.Run((ICont<I, O, A> c2) => c2.Run(k)));
}
// bind
public static ICont<R, O, B> SelectMany<R, I, O, A, B>(this ICont<R, I, A> c, Func<A, ICont<I, O, B>> f)
{
return ((Func<B, O> k) => c.Run((A x) => f(x).Run(k)));
}
// bindMap
public static ICont<R, O, C> SelectMany<R, I, O, A, B, C>(this ICont<R, I, A> c, Func<A, ICont<I, O, B>> f1, Func<A, B, C> f2)
{
return ((Func<C, O> k) => c.Run((A x) => f1(x).Run((B y) => k(f2(x, y)))));
}
Next we implement the two ICont
-specific primitives: shift
and reset
:
Haskell:
shift :: ((a -> ICont i i o) -> ICont r j j) -> ICont r o a
shift f = ICont $ \k1 -> runIContId . f $ \x -> ICont $ \k2 -> k2 $ k1 x
reset :: ICont a o o -> ICont r r a
reset a = ICont $ \k -> k $ runIContId a
Scala:
private[indexedCont] sealed trait IContFuncs { this: ICont.type =>
def shift[R, I, J, O, A](f: (A => ICont[I, I, O]) => ICont[R, J, J]): ICont[R, O, A] = ICont { k1 => (f { x => ICont { k2 => k2(k1(x)) } }).runId }
def reset[R, O, A](a: ICont[A, O, O]): ICont[R, R, A] = ICont { k => k(a.runId) }
}
C#:
public static ICont<R, O, A> Shift<R, I, J, O, A>(Func<Func<A, ICont<I, I, O>>, ICont<R, J, J> f)
{
return ((Func<A, O> k1) => f((A x) => ((Func<O, I> k2) => k2(k1(x)))).RunId());
}
public static ICont<R, R, A> Reset<R, O, A>(ICont<A, O, O> a)
{
return ((Func<A, R> k) => k(a.RunId()));
}
}
}
We're done! We can now use our new indexed continuation monad to do arbitrary control flow in a statically type-safe manner.
Quite interesting...
I've been playing with indexing a a state-and-continuation monad with pre- and postconditions for developing a Hoare-style Logic for higher order control in Coq/SSreflect. Our continuation monad is
slightly different though, being the standard continuation monad-- no shift and reset either.
If you're interested, you are welcome to have a look at the paper and the ssreflect code here: http://software.imdea.org/~germand/HTTcc/
As to indexing monads (just state, no continuations) for control flow, you can have a look at this other paper:
http://software.imdea.org/~aleks/rhtt/oakland11.pdf
The code is also on Aleks' homepage.
Cheers!