sessions-2008.2.28: Session Types for Haskell Source code Contents Index

Control.Concurrent.Session.Runtime

Description

Having actually described a session type, you'll now want to implement it! Use the methods of SMonad to chain functions together.

Synopsis

data OfferImpls where OfferImplsNil :: OfferImpls Nil prog progOut progIn finalState finalResult (~||~) :: forall prog prog' progOut progIn outgoing incoming finalState finalResult jumps l. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming)))) => SessionChain prog progOut progIn (outgoing, incoming) finalState finalResult -> OfferImpls jumps prog progOut progIn finalState finalResult -> OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog progOut progIn finalState finalResult data SessionState where SessionState :: prog -> progOut -> progIn -> MVar (Cell currentOutgoing) -> MVar (Cell currentIncoming) -> SessionState prog progOut progIn (currentOutgoing, currentIncoming) newtype SessionChain prog progOut progIn from to res = SessionChain { runSessionChain :: SessionState prog progOut progIn from -> IO (res, SessionState prog progOut progIn to) } 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', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming)))) => SessionChain prog progOut progIn (Cons (Jump l) Nil, Cons (Jump l) 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 soffer :: forall outgoing incoming finalResult prog prog' progOut progIn jumps. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => OfferImpls jumps prog progOut progIn (outgoing, incoming) finalResult -> SessionChain prog progOut progIn (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (outgoing, incoming) finalResult sselect :: forall prog prog' progOut progIn label jumps outgoing incoming len jumpTarget. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, TyListLength jumps len, SmallerThan label len, TypeNumberToInt label, TyListIndex jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', TyListIndex progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn jumpTarget (MVar (ProgramCell (Cell incoming)))) => label -> SessionChain prog progOut progIn (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (outgoing, incoming) () 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', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex 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') class ProgramToMVarsOutgoing prog mvars | prog -> mvars where programToMVarsOutgoing :: prog -> IO mvars data ProgramCell data Cell

Documentation

data OfferImpls where Source

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

(~||~) :: forall prog prog' progOut progIn outgoing incoming finalState finalResult jumps l. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming)))) => SessionChain prog progOut progIn (outgoing, incoming) finalState finalResult -> OfferImpls jumps prog progOut progIn finalState finalResult -> OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog progOut progIn finalState finalResult Source

Use to construct OfferImpls. This function automatically adds the necessary sjump to the start of each branch implementation.

data SessionState where Source

Constructors SessionState :: prog -> progOut -> progIn -> MVar (Cell currentOutgoing) -> MVar (Cell currentIncoming) -> SessionState prog progOut progIn (currentOutgoing, currentIncoming)

newtype SessionChain prog progOut progIn from to res Source

The representation of a computation that performs work using session types. Again, really quite similar to a more-parameterized State monad. Constructors SessionChain runSessionChain :: SessionState prog progOut progIn from -> IO (res, SessionState prog progOut progIn to) Instances (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => SMonadIO (SessionChain prog progOut progIn) (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => SMonad (SessionChain prog progOut progIn)

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', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming)))) => SessionChain prog progOut progIn (Cons (Jump l) Nil, Cons (Jump l) Nil) (outgoing, incoming) () Source

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.

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) () Source

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 Source

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.

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

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, TyListLength jumps len, SmallerThan label len, TypeNumberToInt label, TyListIndex jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', TyListIndex progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn jumpTarget (MVar (ProgramCell (Cell incoming)))) => label -> SessionChain prog progOut progIn (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (outgoing, incoming) () Source

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

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', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex 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') Source

Run! Provide a program and a start point within that program (which is automatically sjumped to), 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.

class ProgramToMVarsOutgoing prog mvars | prog -> mvars where Source

Methods programToMVarsOutgoing :: prog -> IO mvars Source Instances ProgramToMVarsOutgoing Nil Nil (ProgramToMVarsOutgoing nxt nxt', OnlyOutgoing val val', TyList nxt, TyList nxt') => ProgramToMVarsOutgoing (Cons val nxt) (Cons (MVar (ProgramCell (Cell val'))) nxt')

data ProgramCell Source

data Cell Source

Produced by Haddock version 2.3.0