-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Type-safe coroutines using lightweight session types.
--
-- This package provides a pure interface for composing independent
-- functions that have a well-defined communication protocol. It is
-- loosely based on Jesse Tov's Haskell Symposium 2008 paper Haskell
-- Session Types with (almost) no class
-- (http:www.ccs.neu.eduhometovpubssession08.html)
@package Coroutine
@version 0.1.0.0
module Control.Monad.Indexed
-- | IxMonad (Indexed Monad) carries type-level state through a
-- computation. For an IxMonad m, m px py a represents a computation with
-- precondition px, postcondition py, and result value a. px and
-- py can be thought of as type-level propositions that hold at
-- the beginning and end of the computation.
class IxMonad m
return :: (IxMonad m) => a -> m x x a
(>>=) :: (IxMonad m) => m x y a -> (a -> m y z b) -> m x z b
(>>) :: (IxMonad m) => m x y a -> m y z b -> m x z b
fail :: (IxMonad m) => String -> m x y a
-- | IxCont is a continuation monad that supports changing of the answer
-- type during the computation. The result is a functor s x, where
-- the caller of the computation controls the type held inside the
-- functor.
newtype IxCont s x y a
IxCont :: (forall b. (a -> s y b) -> s x b) -> IxCont s x y a
runIxCont :: IxCont s x y a -> forall b. (a -> s y b) -> s x b
-- | mapCont changes the answer type of an IxCont, given a function that
-- maps any (s x) to a (s y).
mapCont :: (forall a. s x a -> s y a) -> IxCont s x z a -> IxCont s y z a
instance IxMonad (IxCont s)
-- | 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.Coroutine
-- | 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
--
newtype WM m x y a
LiftWM :: m a -> WM m x y a
runWM :: WM m x y a -> m a
-- | Eps is the empty session.
data Eps
-- | a :?: r reads a followed by the session r
data (:?:) a r
-- | a :!: r writes a followed by the sesison r
data (:!:) a r
-- | a :&: b offers both the sessions a and
-- b to the other end
data (:&:) s1 s2
-- | a :|: b allows the choice between sessions a and
-- b at runtime
data (:|:) s1 s2
-- | a :?* b is the session a zero or more times followed
-- by b, offering the loop.
data (:?*) s r
-- | a :!* b is the session a zero or more times followed
-- by b, choosing whether or not to loop.
data (:!*) s r
-- | 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.
data (:++:) s1 s2
-- | a :* b is the session a zero or more times followed
-- by b. Either side may terminate the loop.
data (:*) s r
-- | 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
newtype Session x y a
Session :: IxCont InSession x y a -> Session x y a
getSession :: Session x y a -> IxCont InSession x y a
-- | 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.
-- | You never need to explicitly call close; doing so just seals
-- the "rest-of-computation" parameter of the session.
close :: Session Eps Eps ()
-- | get reads an element from the connected coroutine
get :: Session (a :?: r) r a
-- | put x sends the value x to the connected coroutine
put :: a -> Session (a :!: r) r ()
-- | cat m takes a completed session and connects it at the beginning of a
-- sequence inside another session.
cat :: Session a Eps v -> Session (a :++: r) r v
-- | offer s1 s2 gives the other side the choice of whether to continue
-- with session s1 or s2.
offer :: Session a r v -> Session b r v -> Session (a :&: b) r v
-- | sel1 chooses the first branch of an offer
sel1 :: Session (a :|: b) a ()
-- | sel2 chooses the second branch of an offer
sel2 :: Session (a :|: b) b ()
-- | Loop is just nicely-named Either; it is used for choosing whether or
-- not to loop in these simplified looping primitives.
data Loop a b
Loop :: a -> Loop a b
Done :: b -> Loop a b
-- | 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.
loopC :: Loop a b -> (a -> Session x Eps (Loop a b)) -> Session (x :!* r) r b
-- | 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.
loopS :: a -> (a -> Session x Eps a) -> Session (x :?* r) r a
-- | 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.
loop :: Loop a b -> (a -> Session x Eps (Loop a b)) -> Session (x :* r) r (Either a b)
-- | runSession converts a session computation into a connectable
-- session.
runSession :: Session c Eps a -> InSession c a
class Connect s
connect :: (Connect s, s ~ (Dual c), c ~ (Dual s)) => InSession s a -> InSession c b -> (a, b)
-- | connect two completed sessions to each other
connects :: (Connect s, (Dual s) ~ c, (Dual c) ~ s) => Session s Eps a -> Session c Eps b -> (a, b)
instance IxMonad Session
instance (Connect s1, Connect s2) => Connect (s1 :* s2)
instance (Connect s1, Connect s2) => Connect (s1 :!* s2)
instance (Connect s1, Connect s2) => Connect (s1 :?* s2)
instance (Connect s1, Connect s2) => Connect (s1 :++: s2)
instance (Connect s1, Connect s2) => Connect (s1 :|: s2)
instance (Connect s1, Connect s2) => Connect (s1 :&: s2)
instance (Connect s) => Connect (a :!: s)
instance (Connect s) => Connect (a :?: s)
instance Connect Eps
instance (Monad m) => IxMonad (WM m)