This module allows you to implement coroutines that communicate in a typesafe manner using lightweight session types. An abstract group of session "typecombinators" 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 "typelevel 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 compiletime error.
 module Control.Monad.Indexed
 newtype WM m x y a = LiftWM {
 runWM :: m a
 data Eps
 data a :?: r
 data a :!: r
 data s1 :&: s2
 data s1 :: s2
 data s :?* r
 data s :!* r
 data s1 :++: s2
 data s :* r
 newtype Session x y a = Session {
 getSession :: IxCont InSession x y a
 data family InSession s v
 close :: Session Eps Eps ()
 get :: Session (a :?: r) r a
 put :: a > Session (a :!: r) r ()
 cat :: Session a Eps v > Session (a :++: r) r v
 offer :: Session a r v > Session b r v > Session (a :&: b) r v
 sel1 :: Session (a :: b) a ()
 sel2 :: Session (a :: b) b ()
 data Loop a b
 loopC :: Loop a b > (a > Session x Eps (Loop a b)) > Session (x :!* r) r b
 loopS :: a > (a > Session x Eps a) > Session (x :?* r) r a
 loop :: Loop a b > (a > Session x Eps (Loop a b)) > Session (x :* r) r (Either a b)
 runSession :: Session c Eps a > InSession c a
 type family Dual a
 class Connect s where
 connects :: (Connect s, Dual s ~ c, Dual c ~ s) => Session s Eps a > Session c Eps b > (a, b)
Documentation
module Control.Monad.Indexed
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
a :&: b
offers both the sessions a
and b
to the other end
a :: b
allows the choice between sessions a
and b
at runtime
a :?* b
is the session a
zero or more times followed by b
, offering the loop.
a :!* b
is the session a
zero or more times followed by b
, choosing whether or not to loop.
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.
a :* b
is the session a
zero or more times followed by b
. Either side may terminate the loop.
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 compiletime. 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
Session  

data family InSession s v Source
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 ()Source
You never need to explicitly call close; doing so just seals the "restofcomputation" parameter of the session.
cat :: Session a Eps v > Session (a :++: r) r vSource
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 vSource
offer s1 s2 gives the other side the choice of whether to continue with session s1 or s2.
Loop is just nicelynamed Either; it is used for choosing whether or not to loop in these simplified looping primitives.
:: 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 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 aSource
runSession converts a session computation into a connectable session.
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) 