public
Last active

An introduction to the indexed continuation monad in Haskell, Scala, and C#.

  • Download Gist
IndexedCont.md
Markdown

The Indexed Continuation Monad in Haskell, Scala, and C#

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.

Motivation

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.

Implementation

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!

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.