Control.Coroutine
Description
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.
- 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 :?: r reads a followed by the session r
a :!: r writes a followed by the sesison r
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 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
| |
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 "rest-of-computation" 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 nicely-named Either; it is used for choosing whether or not to loop in these simplified looping primitives.
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.
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 aSource
runSession converts a session computation into a connectable session.
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) |