Control.Coroutine

This module allows you to implement coroutines that communicate in a type-safe manner using lightweight session types. An abstract group of session "type-combinators" are offered, and implementations are indexed by those types.

Indexed monads are used to thread the session state through the computation. We generally use them to implement "type-level substitution"; also known as "big lambda". For example, consider a session

  session1 :: forall r. Session (Int :?: String :!: r) r Int

This represents a session that reads an Int, then writes a String, and delivers an Int which can be used in the remainder of the session r. A way to write it with full type functions (not legal Haskell) would be

  session1 :: Session (/\r. Int :?: String :!: r) Float

Using the indexed monad bind operator, we can do, for example:

  session2 = do
      x <- session1
      put x

Now session2 has the type forall r. (Int :?: String :!: Float :!: r) r ()

Connecting two sessions is easy; if they are the dual of each other (one reads where the other writes), just call connects s1 s2. If the sessions are not compatible, you'll get a reasonably readable compile-time error.

Documentation

module Control.Monad.Indexed

newtype WM m x y a

WM stands for wrapped monad; it wraps any Prelude monad. This doesn't really belong in this module, but exporting it correctly from IxMonad is a real pain. This allows you to use NoImplicitPrelude when writing main in the following way:

 module Main where
 import Control.Coroutine
 main = runWM $ do
           LiftWM $ putStrLn hello world

Constructors

LiftWM

Fields

runWM :: m a

Instances

Monad m => IxMonad (WM m)

data Eps

Eps is the empty session.

Instances

Connect Eps

data a :?: r

a :?: r reads a followed by the session r

Instances

Connect s => Connect (:?: a s)

data a :!: r

a :!: r writes a followed by the sesison r

Instances

Connect s => Connect (:!: a s)

data s1 :&: s2

a :&: b offers both the sessions a and b to the other end

Instances

(Connect s1, Connect s2) => Connect (:&: s1 s2)

data s1 :|: s2

a :|: b allows the choice between sessions a and b at runtime

Instances

(Connect s1, Connect s2) => Connect (:|: s1 s2)

data s :?* r

a :?* b is the session a zero or more times followed by b, offering the loop.

Instances

(Connect s1, Connect s2) => Connect (:?* s1 s2)

data s :!* r

a :!* b is the session a zero or more times followed by b, choosing whether or not to loop.

Instances

(Connect s1, Connect s2) => Connect (:!* s1 s2)

data s1 :++: s2

a :++: b is session a followed by session b. This is mostly used for constructing looping constructs; you generally won't need to use it yourself.

Instances

(Connect s1, Connect s2) => Connect (:++: s1 s2)

data s :* r

a :* b is the session a zero or more times followed by b. Either side may terminate the loop.

Instances

(Connect s1, Connect s2) => Connect (:* s1 s2)

newtype Session x y a

By indexing using a data family, we get an untagged representation of the session; resolving how to link sessions together with connect can happen at compile-time. A similar encoding is possible using GADTs, but it requires runtime branching based on the GADT tag.

IxCont s x y a == forall b. (a -> s y b) -> s x b; that is, if you give us a continuation function that takes an a and outputs the rest of the session, we can give you a representation of the full session. When a session is complete, y is Eps, the empty session, so getting the full session out is just runIxCont (getSession session) Eps which gives you the result of type InSession session_type a

Constructors

Session

Fields

getSession :: IxCont InSession x y a

Instances

IxMonad Session

data family InSession s v

InSession s v is a functor type representing a session that results in the value v being computed by the session. s should be indexed by one of the session types above, although you can extended the session type system by adding additional instances here and to Dual and Connect below.

close :: Session Eps Eps ()

You never need to explicitly call close; doing so just seals the "rest-of-computation" parameter of the session.

get :: Session (a :?: r) r a

get reads an element from the connected coroutine

put :: a -> Session (a :!: r) r ()

put x sends the value x to the connected coroutine

cat :: Session a Eps v -> Session (a :++: r) r v

cat m takes a completed session and connects it at the beginning of a sequence inside another session.

offer :: Session a r v -> Session b r v -> Session (a :&: b) r v

offer s1 s2 gives the other side the choice of whether to continue with session s1 or s2.

sel1 :: Session (a :|: b) a ()

sel1 chooses the first branch of an offer

sel2 :: Session (a :|: b) b ()

sel2 chooses the second branch of an offer

data Loop a b

Loop is just nicely-named Either; it is used for choosing whether or not to loop in these simplified looping primitives.

Constructors

Loop a

Done b

loopC

Arguments

:: Loop a b

Initial loop state

-> (a -> Session x Eps (Loop a b))

Session for the loop

-> Session (x :!* r) r b

Result of the loop

loopC is the client side of a while loop; it takes the current loop state, and a computation that figures out the next loop state, and loops until the computation returns Done.

loopS

Arguments

:: a

Initial loop state

-> (a -> Session x Eps a)

Session for the loop

-> Session (x :?* r) r a

Result of the loop

loopS is the server side of a while loop; it must always offer the client the option to terminate the loop at each iteration, or to continue the loop.

loop

Arguments

:: Loop a b

Initial loop state

-> (a -> Session x Eps (Loop a b))

Session for the loop

-> Session (x :* r) r (Either a b)

Result of the loop

loop is a slightly more complicated looping primitive where either side of the loop may choose to terminate the loop at each iteration. It is useful for a server that has a fixed amount of data to give out, when the client can also choose to escape early.

runSession :: Session c Eps a -> InSession c a

runSession converts a session computation into a connectable session.

type family Dual a

class Connect s where

Methods

connect :: (s ~ Dual c, c ~ Dual s) => InSession s a -> InSession c b -> (a, b)

Instances

Connect Eps

(Connect s1, Connect s2) => Connect (:++: s1 s2)

(Connect s1, Connect s2) => Connect (:* s1 s2)

(Connect s1, Connect s2) => Connect (:!* s1 s2)

(Connect s1, Connect s2) => Connect (:?* s1 s2)

(Connect s1, Connect s2) => Connect (:|: s1 s2)

(Connect s1, Connect s2) => Connect (:&: s1 s2)

Connect s => Connect (:!: a s)

Connect s => Connect (:?: a s)

connects :: (Connect s, Dual s ~ c, Dual c ~ s) => Session s Eps a -> Session c Eps b -> (a, b)

connect two completed sessions to each other