effect-sessions-1.0: Sessions and session types for Concurrent Haskell

Safe HaskellNone
LanguageHaskell98

Control.Effect.Sessions

Synopsis

Documentation

data Process s a Source

Process computation type indexed by an environment of the (free) channel names used in the computation, paired with a specification of their behaviour.

Constructors

Process 

Fields

getProcess :: IO a
 

Instances

data Chan n Source

Namec channels, encapsulating Concurrent Haskell channels

Constructors

forall a . MkChan (Chan a) 

data Name Source

Channel endpoint names

Constructors

Ch Symbol 
Op Symbol 

Instances

Effect [Map Name Session] Process Source 
type Unit [Map Name Session] Process = [] (Map Name Session) Source 
type Plus [Map Name Session] Process s t = Union Name Session s t Source 
type Inv [Map Name Session] Process s t = Balanced s t Source 
type Cmp (Map Name Session) ((:->) Name Session c a) ((:->) Name Session d b) = CmpSessionMap ((:->) Name Session c a) ((:->) Name Session d b) Source

Compare channel names for normalising type-level finite map representations

data Symbol :: *

(Kind) This is the kind of type-level symbols.

Instances

type (==) Symbol a b = EqSymbol a b 

data Session Source

Session types

Constructors

forall a . a :! Session

Send

forall a . a :? Session

Receive

forall a . a :*! Session

Output

Session :+ Session

Alternation (for branch/select)

Bal Session

Marks a session that should balance when composed

End

End of session

Fix Session Session

Denotes an affine fixed point, where Fix a b = a* . b

Star

A placeholder for a recursion variable- never generated by the encoding or produced by any operation, but set as the session type for a recursive call in a fixed-point (see affineFix).

Instances

Effect [Map Name Session] Process Source 
type Combine Session s t = SessionSeq s t Source 
type Unit [Map Name Session] Process = [] (Map Name Session) Source 
type Plus [Map Name Session] Process s t = Union Name Session s t Source 
type Inv [Map Name Session] Process s t = Balanced s t Source 
type Cmp (Map Name Session) ((:->) Name Session c a) ((:->) Name Session d b) = CmpSessionMap ((:->) Name Session c a) ((:->) Name Session d b) Source

Compare channel names for normalising type-level finite map representations

data Delegate Source

Delegated session

Constructors

Delg Session 

type family Dual s Source

Duality function: calculuate the dual of a simple, non-recursive session type

Equations

Dual End = End 
Dual (t :! s) = t :? Dual s 
Dual (t :*! s) = t :? Dual s 
Dual (t :? s) = t :! Dual s 
Dual (s :+ t) = Dual s :+ Dual t 
Dual (Bal t) = Dual t 
Dual Star = Star 

type family DualP s t :: Constraint Source

Duality relation: extends the duality function to include recursive session types

Equations

DualP End End = () 
DualP (t :! s) (t' :? s') = (t ~ t', DualP s s') 
DualP (t :? s) (t' :! s') = (t ~ t', DualP s s') 
DualP (Bal s) s' = DualP s s' 
DualP s (Bal s') = DualP s s' 
DualP (s :+ t) (s' :+ t') = (DualP s s', DualP t t') 
DualP (Fix a b) s = EqFix a (Fix a b) (Dual s) 
DualP s (Fix a b) = EqFix a (Fix a b) (Dual s) 

type family SessionSeq s t Source

Sequential composition of sessions

Equations

SessionSeq End (Bal s) = s 
SessionSeq End s = s 
SessionSeq (a :? s) t = a :? SessionSeq s t 
SessionSeq (a :! s) t = a :! SessionSeq s t 
SessionSeq (a :*! s) t = a :*! SessionSeq s t 
SessionSeq (s1 :+ s2) t = SessionSeq s1 t :+ SessionSeq s2 t 
SessionSeq (Bal s) t = SessionSeq s t 
SessionSeq Star Star = Star 

type family Balanced s t :: Constraint Source

Predicate for checking that two environments are balanced

Equations

Balanced [] [] = () 
Balanced env [] = () 
Balanced [] env = () 
Balanced ((c :-> s) : env) env' = (BalancedF (c :-> s) env', Balanced env env') 

type family NotBal s :: Constraint Source

Checks that we are not requiring a balanced session

Equations

NotBal (s :! t) = () 
NotBal (s :? t) = () 
NotBal (s :+ t) = () 
NotBal (s :*! t) = () 
NotBal (Bal Star) = () 
NotBal (Bal (Int :! (s :*! t))) = () 
NotBal Star = () 
NotBal End = () 

class Effect m where Source

Specifies "parametric effect monads" which are essentially monads but annotated by a type-level monoid formed by Plus and Unit

Minimal complete definition

return, (>>=)

Associated Types

type Unit m :: k Source

Effect of a trivially effectful computation |

type Plus m f g :: k Source

Cominbing effects of two subcomputations |

type Inv m f g :: Constraint Source

Inv provides a way to give instances of Effect their own constraints for >>=

Methods

return :: a -> m (Unit m) a Source

Effect-parameterised version of return. Annotated with the 'Unit m' effect, denoting pure compuation

(>>=) :: Inv m f g => m f a -> (a -> m g b) -> m (Plus m f g) b Source

Effect-parameterise version of >>= (bind). Combines two effect annotations f and g on its parameter computations into Plus

(>>) :: Inv m f g => m f a -> m g b -> m (Plus m f g) b Source

Instances

fail :: t Source

run :: Process [] a -> IO a Source

A process can be run if it is closed (i.e., empty channel environment)

data Map k v Source

Constructors

k :-> v infixr 4 

Instances

Effect [Map Name Session] Process Source 
type Unit [Map Name Session] Process = [] (Map Name Session) Source 
type Plus [Map Name Session] Process s t = Union Name Session s t Source 
type Inv [Map Name Session] Process s t = Balanced s t Source 
type Cmp (Map Name Session) ((:->) Name Session c a) ((:->) Name Session d b) = CmpSessionMap ((:->) Name Session c a) ((:->) Name Session d b) Source

Compare channel names for normalising type-level finite map representations

type family m :@ c :: Session Source

Lookup a channel from an enrivonment, returning End if it is not a member

Equations

[] :@ k = End 
((k :-> v) : m) :@ k = v 
(kvp : m) :@ k = m :@ k 

type Union m n = Nub (Sort (m :++ n)) Source

type family m :\ c :: [Map k v] Source

Equations

[] :\ k = [] 
((k :-> v) : m) :\ k = m :\ k 
(kvp : m) :\ k = kvp : (m :\ k) 

send :: Chan c -> t -> Process `[c :-> (t :! End)]` () Source

Send a primitive-typed value

recv :: Chan c -> Process `[c :-> (t :? End)]` t Source

Receive a primitive-typed value

new :: Duality env c => ((Chan (Ch c), Chan (Op c)) -> Process env t) -> Process ((env :\ Op c) :\ Ch c) t Source

Create a new channel and pass its two endpoints to the supplied continuation (the first parameter). This channel is thus only in scope for this continuation

par :: Balanced env (AllBal env') => Process env () -> Process env' () -> Process (Union env env') () Source

Parallel compose two processes, if they contain disjoint (or balanced) sessions

rsend :: Chan c -> Chan d -> Process `[c :-> (Delg s :*! End), d :-> Bal s]` () Source

Output a channel (dual to a replicated input)

chSend :: Chan c -> Chan d -> Process `[c :-> (Delg s :! End), d :-> Bal s]` () Source

Send a channel d over channel c

chRecv :: Chan c -> (Chan d -> Process env a) -> Process (Union `[c :-> (Delg (env :@ d) :? (env :@ c))]` (env :\ d)) a Source

Receive a channel over a channel c, bind to the name d

sub :: Subeffect m f g => m f a -> m g a Source

subL :: Process `[c :-> s]` a -> Process `[c :-> (s :+ t)]` a Source

Explicit subeffecting introduction of :+ with the current session behaviour on the left

subR :: Process `[c :-> t]` a -> Process `[c :-> (s :+ t)]` a Source

Explicit subeffecting introduction of :+ with the current session behaviour on the right

subEnd :: Chan c -> Process [] a -> Process `[c :-> End]` a Source

Explicit subeffecting introduction of a terminated session for channel c

affineFix :: ((a -> Process `[c :-> Star]` b) -> a -> Process `[c :-> h]` b) -> a -> Process `[c :-> ToFix h]` b Source

Recursion combinator for recursive functions which have an affine fixed-point equation on their effects. For example, if 'h ~ (Seq h a) :+ b' then 'ToFix h = Fix a b'

print :: Show a => a -> Process [] () Source

Print to stdout in a process

putStrLn :: String -> Process ([] (Map Name Session)) () Source

putStrLn in a process

liftIO :: IO a -> Process [] a Source

Lift IO computations to a process

ifThenElse :: Bool -> t -> t -> t Source