Safe Haskell	None
Language	Haskell98

Control.Effect.Sessions.Process

Synopsis

Documentation

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

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

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

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 EqFix f f' s :: Constraint Source

Compute fixed-point equality of session types by unrolling

Equations

EqFix a (Fix Star b) b = ()
EqFix a (Fix Star b) s = EqFix a (Fix a b) s
EqFix a (Fix (t :! s) b) (t' :! s') = (t ~ t', EqFix a (Fix s b) s')
EqFix a (Fix (t :? s) b) (t' :? s') = (t ~ t', EqFix a (Fix s b) s')
EqFix a (Fix (t1 :+ t2) b) (t1' :+ t2') = (t1 ~ t1', t2 ~ t2')
EqFix a (Fix (t :! s) b) (t' :! s') = (t ~ t', EqFix a (Fix s b) s')

type Duality env c = DualP (env :@ Ch c) (env :@ Op c) Source

Predicate over environments that channel c has dual endpoints with dual session types

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 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

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 Chan n Source

Namec channels, encapsulating Concurrent Haskell channels

Constructors

forall a . MkChan (Chan a)

type family CmpSessionMap x y Source

Compare channel names for normalising type-level finite map representations

Equations

CmpSessionMap (Ch c :-> a) (Op d :-> b) = LT
CmpSessionMap (Op c :-> a) (Ch d :-> b) = GT
CmpSessionMap (Ch c :-> a) (Ch d :-> b) = CmpSymbol c d
CmpSessionMap (Op c :-> a) (Op d :-> b) = CmpSymbol c d

fail :: t Source

type family DistribL g Source

Normalises session types using the left-distributivity rule for effects: i.e. f * (g + h) = (f * g) + (f * h)

Equations

DistribL (a :! (s :+ t)) = DistribL (a :! s) :+ DistribL (a :! t)
DistribL (a :? (s :+ t)) = DistribL (a :? s) :+ DistribL (a :? t)
DistribL (a :? s) = DistribInsideSeq ((:?) a) (DistribL s)
DistribL (a :! s) = DistribInsideSeq ((:!) a) (DistribL s)
DistribL (a :+ b) = DistribL a :+ DistribL b
DistribL Star = Star
DistribL End = End

type family DistribInsideSeq k a :: Session Source

Part of the normalisation procedure for left-distributivity

Equations

DistribInsideSeq k (s :+ t) = k s :+ k t
DistribInsideSeq k s = k s

type ToFix s = ToFixP (DistribL s) Source

Map an affine equation on effects to the fixed point solution: That is '(Seq Star a) :+ b' where Star is the placeholder for a recursion variable then 'ToFix ((Seq Star a) :+ b) = Fix a b'

type family ToFixPP a a' b b' :: Session Source

Equations

ToFixPP a (t :! s) b b' = ToFixPP a s b b'
ToFixPP a (t :? s) b b' = ToFixPP a s b b'
ToFixPP a End b b' = ToFixPP b b' a End
ToFixPP a Star b b' = Fix a b
ToFixPP a a' b Star = Fix b a

type family ToFixP s Source

Equations

ToFixP (a :+ b) = ToFixPP a a b b
ToFixP s = ToFixPP s s End End

type family ToFixes env :: [Map Name Session] Source

Equations

ToFixes [] = []
ToFixes ((c :-> v) : env) = (c :-> ToFix v) : env

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 BalancedF s t :: Constraint Source

Side recursive case of balancing (check each var -> session type map against every other

Equations

BalancedF (c :-> s) [] = ()
BalancedF (Ch c :-> Bal s) ((Op c :-> Bal t) : env) = t ~ Dual s
BalancedF (Op c :-> Bal s) ((Ch c :-> Bal t) : env) = t ~ Dual s
BalancedF (Ch c :-> Bal s) ((Op c :-> t) : env) = t ~ Dual s
BalancedF (Op c :-> Bal s) ((Ch c :-> t) : env) = t ~ Dual s
BalancedF (c :-> s) ((c :-> t) : env) = (NotBal s, NotBal t)
BalancedF (c :-> s) ((d :-> t) : env) = BalancedF (c :-> s) 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 = ()