sessions-2008.2.22: Session Types for Haskell Contents Index

Control.Concurrent.Session

Synopsis

data OfferImpls where OfferImplsNil :: OfferImpls Nil prog progOut progIn finalState finalResult sjump :: forall l prog prog' progOut progIn outgoing incoming. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', Elem progOut l (MVar (ProgramCell (Cell outgoing))), Elem progIn l (MVar (ProgramCell (Cell incoming)))) => (SessionChain prog progOut progIn) (Cons (Jump l) Nil, Cons (Jump l) Nil) (outgoing, incoming) () soffer :: forall finalState finalResult prog prog' progOut progIn jumps. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => OfferImpls jumps prog progOut progIn finalState finalResult -> (SessionChain prog progOut progIn) (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) finalState finalResult sselect :: forall prog prog' progOut progIn label jumps outgoing incoming len jumpTarget. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, ListLength jumps len, SmallerThan label len, TypeNumberToInt label, Elem jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', Elem progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), Elem progIn jumpTarget (MVar (ProgramCell (Cell incoming)))) => label -> (SessionChain prog progOut progIn) (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (outgoing, incoming) () ssend :: forall t prog prog' progOut progIn nxt incoming. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => t -> (SessionChain prog progOut progIn) (Cons t nxt, incoming) (nxt, incoming) () srecv :: forall t prog prog' progOut progIn nxt outgoing. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => (SessionChain prog progOut progIn) (outgoing, Cons t nxt) (outgoing, nxt) t run :: forall prog prog' progOut progIn init fromO fromI toO toI toO' toI' res res'. (Dual prog prog', Dual prog' prog, ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', Elem progOut init (MVar (ProgramCell (Cell fromO))), Elem progIn init (MVar (ProgramCell (Cell fromI)))) => prog -> init -> SessionChain prog progOut progIn (fromO, fromI) (toO, toI) res -> SessionChain prog' progIn progOut (fromI, fromO) (toO', toI') res' -> IO (res, res') data End data Send where Send :: t -> Send t SendInt :: Send Int SendBool :: Send Bool SendChar :: Send Char SendStr :: Send String SendDouble :: Send Double data Recv where Recv :: t -> Recv t RecvInt :: Recv Int RecvBool :: Recv Bool RecvChar :: Recv Char RecvStr :: Recv String RecvDouble :: Recv Double data Jump l data Select data Offer jump :: TyNum n => n -> Cons (Jump n) Nil end :: Cons End Nil select :: SListOfJumps (Cons val nxt) => (Cons val nxt) -> Cons (Select (Cons val nxt)) Nil offer :: SListOfJumps (Cons val nxt) => (Cons val nxt) -> Cons (Offer (Cons val nxt)) Nil class Dual a b | a -> b, b -> a where dual :: a -> b (~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> (Cons a nxt) (~|~) :: (TyNum target, TyList nxt) => target -> nxt -> Cons (Cons (Jump target) Nil) nxt class SWellFormedConfig idxA idxB ss testWellformed :: SWellFormedConfig idxA idxB ss => ss -> idxA -> idxB -> Bool data Cons cons :: TyList n => t -> n -> (Cons t n) data Nil nil :: Nil data E = E data D0 n = D0 n data D1 n = D1 n data D2 n = D2 n data D3 n = D3 n data D4 n = D4 n data D5 n = D5 n data D6 n = D6 n data D7 n = D7 n data D8 n = D8 n data D9 n = D9 n newtype SChain m x y a = SChain { runSChain :: x -> m (a, y) } class SMonad m where (~>>) :: m x y a -> m y z b -> m x z b (~>>=) :: m x y a -> (a -> m y z b) -> m x z b sreturn :: a -> m x x a newtype SStateT s m x y a = SStateT { runSStateT :: s -> m x y (a, s) } class SMonadTrans t where slift :: SMonad m => m x y a -> t m x y a class SMonad m => SMonadIO m where sliftIO :: IO a -> m x x a class SMonad m => SMonadState s m | m -> s where sget :: m x x s sput :: s -> m x x ()

Documentation

data OfferImpls where

Use OfferImpls to construct the implementations of the branches of an offer. Really, it's just a slightly fancy list. Constructors OfferImplsNil :: OfferImpls Nil prog progOut progIn finalState finalResult

sjump :: forall l prog prog' progOut progIn outgoing incoming. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', Elem progOut l (MVar (ProgramCell (Cell outgoing))), Elem progIn l (MVar (ProgramCell (Cell incoming)))) => (SessionChain prog progOut progIn) (Cons (Jump l) Nil, Cons (Jump l) Nil) (outgoing, incoming) ()

Perform a jump. Now you may think that you should indicate where you want to jump to. But of coures, that's actually specified by the session type so you don't have to specify it at all in the implementation.

soffer :: forall finalState finalResult prog prog' progOut progIn jumps. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => OfferImpls jumps prog progOut progIn finalState finalResult -> (SessionChain prog progOut progIn) (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) finalState finalResult

Offer a number of branches. This is basically an external choice - the other party uses sselect to decide which branch to take. Use OfferImpls in order to construct the list of implementations of branches. Note that every implementation must result in the same final state and emit the same value.

sselect :: forall prog prog' progOut progIn label jumps outgoing incoming len jumpTarget. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, ListLength jumps len, SmallerThan label len, TypeNumberToInt label, Elem jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', Elem progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), Elem progIn jumpTarget (MVar (ProgramCell (Cell incoming)))) => label -> (SessionChain prog progOut progIn) (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (outgoing, incoming) ()

Select which branch we're taking at a branch point. Use a type number (Control.Concurrent.Session.Number) to indicate the branch to take.

ssend :: forall t prog prog' progOut progIn nxt incoming. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => t -> (SessionChain prog progOut progIn) (Cons t nxt, incoming) (nxt, incoming) ()

Send a value to the other party. Of course, the value must be of the correct type indicated in the session type.

srecv :: forall t prog prog' progOut progIn nxt outgoing. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => (SessionChain prog progOut progIn) (outgoing, Cons t nxt) (outgoing, nxt) t

Recieve a value from the other party. This will block as necessary. The type of the value received is specified by the session type. No magic coercion needed.

run :: forall prog prog' progOut progIn init fromO fromI toO toI toO' toI' res res'. (Dual prog prog', Dual prog' prog, ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', Elem progOut init (MVar (ProgramCell (Cell fromO))), Elem progIn init (MVar (ProgramCell (Cell fromI)))) => prog -> init -> SessionChain prog progOut progIn (fromO, fromI) (toO, toI) res -> SessionChain prog' progIn progOut (fromI, fromO) (toO', toI') res' -> IO (res, res')

Run! Provide a program and a start point within that program (which also then means that all implementations must start with sjump), the two implementations which must be duals of each other, run them, have them communicate, wait until they both finish and die and then return the results from both of them.

data End

Instances Show End STerminal End SNoJumpsBeyond End idx Dual End End

data Send where

Constructors Send :: t -> Send t SendInt :: Send Int SendBool :: Send Bool SendChar :: Send Char SendStr :: Send String SendDouble :: Send Double Instances SNonTerminal (Send t) SNoJumpsBeyond (Send t) idx Dual (Recv t) (Send t) Dual (Send t) (Recv t)

data Recv where

Constructors Recv :: t -> Recv t RecvInt :: Recv Int RecvBool :: Recv Bool RecvChar :: Recv Char RecvStr :: Recv String RecvDouble :: Recv Double Instances SNonTerminal (Recv t) SNoJumpsBeyond (Recv t) idx Dual (Recv t) (Send t) Dual (Send t) (Recv t)

data Jump l

Instances Show l => Show (Jump l) TyNum l => STerminal (Jump l) SmallerThan l idx => SNoJumpsBeyond (Jump l) idx Dual (Jump l) (Jump l)

data Select

Instances SListOfJumps (Cons val nxt) => STerminal (Select (Cons val nxt)) SNoJumpsBeyond lol idx => SNoJumpsBeyond (Select lol) idx Dual (Offer lst) (Select lst) Dual (Select lst) (Offer lst)

data Offer

Instances SListOfJumps (Cons val nxt) => STerminal (Offer (Cons val nxt)) SNoJumpsBeyond lol idx => SNoJumpsBeyond (Offer lol) idx Dual (Offer lst) (Select lst) Dual (Select lst) (Offer lst)

jump :: TyNum n => n -> Cons (Jump n) Nil

end :: Cons End Nil

select :: SListOfJumps (Cons val nxt) => (Cons val nxt) -> Cons (Select (Cons val nxt)) Nil

offer :: SListOfJumps (Cons val nxt) => (Cons val nxt) -> Cons (Offer (Cons val nxt)) Nil

class Dual a b | a -> b, b -> a where

Methods dual :: a -> b Instances Dual Nil Nil Dual End End Dual (Offer lst) (Select lst) Dual (Offer lst) (Select lst) Dual (Select lst) (Offer lst) Dual (Select lst) (Offer lst) Dual (Jump l) (Jump l) Dual (Recv t) (Send t) Dual (Recv t) (Send t) Dual (Send t) (Recv t) Dual (Send t) (Recv t) (Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt')

(~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> (Cons a nxt)

(~|~) :: (TyNum target, TyList nxt) => target -> nxt -> Cons (Cons (Jump target) Nil) nxt

class SWellFormedConfig idxA idxB ss

testWellformed :: SWellFormedConfig idxA idxB ss => ss -> idxA -> idxB -> Bool

data Cons

Instances (ListLength n l, Succ l l', Show n, Show t) => Show (Cons t n) TyList nxt => TyList (Cons val nxt) (SValidSessionType nxt, SNonTerminal val) => SValidSessionType (Cons val nxt) STerminal a => SValidSessionType (Cons a Nil) (SValidSessionType val, SListOfSessionTypes nxt) => SListOfSessionTypes (Cons val nxt) (SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) nxt) (ListLength n len, Succ len len') => ListLength (Cons t n) len' OnlyOutgoing nxt nxt' => OnlyOutgoing (Cons (Recv t) nxt) nxt' (SNoJumpsBeyond val idx, SNoJumpsBeyond nxt idx) => SNoJumpsBeyond (Cons val nxt) idx (Elem nxt idx' res, Pred idx idx', SmallerThan idx' len, ListLength nxt len) => Elem (Cons val nxt) idx res Elem (Cons res nxt) (D0 E) res OnlyOutgoing (Cons (Offer jl) Nil) (Cons (Choice jl) Nil) OnlyOutgoing (Cons (Select jl) Nil) (Cons (Choice jl) Nil) OnlyOutgoing (Cons (Jump l) Nil) (Cons (Jump l) Nil) OnlyOutgoing nxt nxt' => OnlyOutgoing (Cons (Send t) nxt) (Cons t nxt') OnlyOutgoing (Cons End Nil) (Cons End Nil) (Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt') (ProgramToMVarsOutgoing nxt nxt', OnlyOutgoing val val') => ProgramToMVarsOutgoing (Cons val nxt) (Cons (MVar (ProgramCell (Cell val'))) nxt')

cons :: TyList n => t -> n -> (Cons t n)

data Nil

Instances Show Nil TyList Nil SListOfSessionTypes Nil SListOfJumps Nil SNoJumpsBeyond Nil idx Dual Nil Nil ProgramToMVarsOutgoing Nil Nil ListLength Nil (D0 E)

nil :: Nil

data E

Constructors E Instances Show E Reverse' E a a IncrementRightToLeft E (D1 E)

data D0 n

Constructors D0 n Instances ListLength Nil (D0 E) Pred m m' => Add m (D0 E) m Show n => Show (D0 n) TypeNumberToInt (D0 E) TyNum n => TyNum (D0 n) TyNum (D0 E) Pred y y' => SmallerThan (D0 E) y StripLeadingZeros a b => StripLeadingZeros (D0 a) b Pred n n' => Add (D0 E) n n Reverse' n (D0 a) r => Reverse' (D0 n) a r StripLeadingZeros (D0 E) (D0 E) DecrementRightToLeft (D1 a) (D0 a) DecrementRightToLeft a b => DecrementRightToLeft (D0 a) (D9 b) IncrementRightToLeft a b => IncrementRightToLeft (D9 a) (D0 b) IncrementRightToLeft (D0 a) (D1 a) Add (D0 E) (D0 E) (D0 E) Elem (Cons res nxt) (D0 E) res

data D1 n

Constructors D1 n Instances IncrementRightToLeft E (D1 E) Show n => Show (D1 n) TyNum n => TyNum (D1 n) TyNum (D1 E) Reverse' n (D1 a) r => Reverse' (D1 n) a r StripLeadingZeros (D1 a) (D1 a) DecrementRightToLeft (D2 a) (D1 a) DecrementRightToLeft (D1 a) (D0 a) IncrementRightToLeft (D1 a) (D2 a) IncrementRightToLeft (D0 a) (D1 a)

data D2 n

Constructors D2 n Instances Show n => Show (D2 n) TyNum n => TyNum (D2 n) TyNum (D2 E) Reverse' n (D2 a) r => Reverse' (D2 n) a r StripLeadingZeros (D2 a) (D2 a) DecrementRightToLeft (D3 a) (D2 a) DecrementRightToLeft (D2 a) (D1 a) IncrementRightToLeft (D2 a) (D3 a) IncrementRightToLeft (D1 a) (D2 a)

data D3 n

Constructors D3 n Instances Show n => Show (D3 n) TyNum n => TyNum (D3 n) TyNum (D3 E) Reverse' n (D3 a) r => Reverse' (D3 n) a r StripLeadingZeros (D3 a) (D3 a) DecrementRightToLeft (D4 a) (D3 a) DecrementRightToLeft (D3 a) (D2 a) IncrementRightToLeft (D3 a) (D4 a) IncrementRightToLeft (D2 a) (D3 a)

data D4 n

Constructors D4 n Instances Show n => Show (D4 n) TyNum n => TyNum (D4 n) TyNum (D4 E) Reverse' n (D4 a) r => Reverse' (D4 n) a r StripLeadingZeros (D4 a) (D4 a) DecrementRightToLeft (D5 a) (D4 a) DecrementRightToLeft (D4 a) (D3 a) IncrementRightToLeft (D4 a) (D5 a) IncrementRightToLeft (D3 a) (D4 a)

data D5 n

Constructors D5 n Instances Show n => Show (D5 n) TyNum n => TyNum (D5 n) TyNum (D5 E) Reverse' n (D5 a) r => Reverse' (D5 n) a r StripLeadingZeros (D5 a) (D5 a) DecrementRightToLeft (D6 a) (D5 a) DecrementRightToLeft (D5 a) (D4 a) IncrementRightToLeft (D5 a) (D6 a) IncrementRightToLeft (D4 a) (D5 a)

data D6 n

Constructors D6 n Instances Show n => Show (D6 n) TyNum n => TyNum (D6 n) TyNum (D6 E) Reverse' n (D6 a) r => Reverse' (D6 n) a r StripLeadingZeros (D6 a) (D6 a) DecrementRightToLeft (D7 a) (D6 a) DecrementRightToLeft (D6 a) (D5 a) IncrementRightToLeft (D6 a) (D7 a) IncrementRightToLeft (D5 a) (D6 a)

data D7 n

Constructors D7 n Instances Show n => Show (D7 n) TyNum n => TyNum (D7 n) TyNum (D7 E) Reverse' n (D7 a) r => Reverse' (D7 n) a r StripLeadingZeros (D7 a) (D7 a) DecrementRightToLeft (D8 a) (D7 a) DecrementRightToLeft (D7 a) (D6 a) IncrementRightToLeft (D7 a) (D8 a) IncrementRightToLeft (D6 a) (D7 a)

data D8 n

Constructors D8 n Instances Show n => Show (D8 n) TyNum n => TyNum (D8 n) TyNum (D8 E) Reverse' n (D8 a) r => Reverse' (D8 n) a r StripLeadingZeros (D8 a) (D8 a) DecrementRightToLeft (D9 a) (D8 a) DecrementRightToLeft (D8 a) (D7 a) IncrementRightToLeft (D8 a) (D9 a) IncrementRightToLeft (D7 a) (D8 a)

data D9 n

Constructors D9 n Instances Show n => Show (D9 n) TyNum n => TyNum (D9 n) TyNum (D9 E) Reverse' n (D9 a) r => Reverse' (D9 n) a r StripLeadingZeros (D9 a) (D9 a) DecrementRightToLeft (D9 a) (D8 a) DecrementRightToLeft a b => DecrementRightToLeft (D0 a) (D9 b) IncrementRightToLeft a b => IncrementRightToLeft (D9 a) (D0 b) IncrementRightToLeft (D8 a) (D9 a)

newtype SChain m x y a

Constructors SChain runSChain :: x -> m (a, y) Instances MonadIO m => SMonadIO (SChain m) Monad m => SMonad (SChain m) Monad m => Monad (SChain m x x)

class SMonad m where

An extension of the typical Monad such that you track additional from and to parameters. Thus you can think of this like State where the type of the State varies. Methods (~>>) :: m x y a -> m y z b -> m x z b (~>>=) :: m x y a -> (a -> m y z b) -> m x z b sreturn :: a -> m x x a Instances Monad m => SMonad (SChain m) SMonad m => SMonad (SStateT s m)

newtype SStateT s m x y a

Constructors SStateT runSStateT :: s -> m x y (a, s) Instances SMonad m => SMonadState s (SStateT s m) SMonadTrans (SStateT s) SMonad m => SMonad (SStateT s m)

class SMonadTrans t where

Methods slift :: SMonad m => m x y a -> t m x y a Instances SMonadTrans (SStateT s)

class SMonad m => SMonadIO m where

Methods sliftIO :: IO a -> m x x a Instances MonadIO m => SMonadIO (SChain m)

class SMonad m => SMonadState s m | m -> s where

Methods sget :: m x x s sput :: s -> m x x () Instances SMonad m => SMonadState s (SStateT s m)

Produced by Haddock version 2.1.0