sessions-2008.5.6: Session Types for HaskellSource codeContentsIndex
Control.Concurrent.Session.SessionType
Description

This module is concerned with allowing you to describe a session type. A session type is treated as a table or 2D array, where each row represents a particular session type function which can refer, by index, to the other rows.

Basically, what you have here is the ability to describe a program at the type level.

Just look at Control.Concurrent.Session.Tests for examples

Documentation
data End Source
Constructors
End
show/hide Instances
end :: Cons End NilSource
sendPid :: TyListSortNums lst lst' => lst -> SendPid False lst'Source
recvPid :: TyListSortNums lst lst' => lst -> RecvPid False lst'Source
data SendPid inverted lst Source
Constructors
SendPid inverted lst
show/hide Instances
(Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog' idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (SendPid True idxs) (Send (Pid prog' prog invertedSessions sessionsToIdx idxsToPairStructs))
(Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (SendPid False idxs) (Send (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs))
(Show inverted, Show lst) => Show (SendPid inverted lst)
SNonTerminal (SendPid inverted t)
(MakeListOfJumps lol lol', SNoJumpsBeyond lol' idx) => SNoJumpsBeyond (SendPid inverted lol) idx
Not inverted inverted' => Dual (RecvPid inverted lst) (SendPid inverted' lst)
Not inverted inverted' => Dual (SendPid inverted lst) (RecvPid inverted' lst)
data RecvPid inverted lst Source
Constructors
RecvPid inverted lst
show/hide Instances
(Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog' idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (RecvPid True idxs) (Recv (Pid prog' prog invertedSessions sessionsToIdx idxsToPairStructs))
(Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (RecvPid False idxs) (Recv (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs))
(Show inverted, Show lst) => Show (RecvPid inverted lst)
SNonTerminal (RecvPid inverted t)
(MakeListOfJumps lol lol', SNoJumpsBeyond lol' idx) => SNoJumpsBeyond (RecvPid inverted lol) idx
Not inverted inverted' => Dual (RecvPid inverted lst) (SendPid inverted' lst)
Not inverted inverted' => Dual (SendPid inverted lst) (RecvPid inverted' lst)
sendSession :: idx -> SendSession False idxSource
recvSession :: idx -> RecvSession False idxSource
data SendSession inverted idx Source
Constructors
SendSession inverted idx
show/hide Instances
(Outgoing current ~ outgoing, Outgoing current' ~ incoming, Dual prog prog', Expand prog' frag current, Dual frag frag', Expand prog' frag' current') => ExpandSession prog (SendSession True frag) (Send (SessionState prog' prog ((,,) current outgoing incoming)))
(Outgoing current ~ outgoing, Outgoing current' ~ incoming, Dual prog prog', Expand prog frag current, Dual frag frag', Expand prog frag' current') => ExpandSession prog (SendSession False frag) (Send (SessionState prog prog' ((,,) current outgoing incoming)))
(Show inverted, Show idx) => Show (SendSession inverted idx)
SValidSessionType idx => SNonTerminal (SendSession inverted idx)
SNoJumpsBeyond l idx => SNoJumpsBeyond (SendSession inverted l) idx
Not inverted inverted' => Dual (RecvSession inverted idx) (SendSession inverted' idx)
Not inverted inverted' => Dual (SendSession inverted idx) (RecvSession inverted' idx)
data RecvSession inverted idx Source
Constructors
RecvSession inverted idx
show/hide Instances
(Outgoing current ~ outgoing, Outgoing current' ~ incoming, Dual prog prog', Expand prog' frag current, Dual frag frag', Expand prog' frag' current') => ExpandSession prog (RecvSession True frag) (Recv (SessionState prog' prog ((,,) current outgoing incoming)))
(Outgoing current ~ outgoing, Outgoing current' ~ incoming, Dual prog prog', Expand prog frag current, Dual frag frag', Expand prog frag' current') => ExpandSession prog (RecvSession False frag) (Recv (SessionState prog prog' ((,,) current outgoing incoming)))
(Show inverted, Show idx) => Show (RecvSession inverted idx)
SValidSessionType idx => SNonTerminal (RecvSession inverted idx)
SNoJumpsBeyond l idx => SNoJumpsBeyond (RecvSession inverted l) idx
Not inverted inverted' => Dual (RecvSession inverted idx) (SendSession inverted' idx)
Not inverted inverted' => Dual (SendSession inverted idx) (RecvSession inverted' idx)
data Send whereSource
Constructors
Send :: t -> Send t
SendInt :: Send Int
SendBool :: Send Bool
SendChar :: Send Char
SendStr :: Send String
SendDouble :: Send Double
show/hide Instances
(Outgoing current ~ outgoing, Outgoing current' ~ incoming, Dual prog prog', Expand prog' frag current, Dual frag frag', Expand prog' frag' current') => ExpandSession prog (SendSession True frag) (Send (SessionState prog' prog ((,,) current outgoing incoming)))
(Outgoing current ~ outgoing, Outgoing current' ~ incoming, Dual prog prog', Expand prog frag current, Dual frag frag', Expand prog frag' current') => ExpandSession prog (SendSession False frag) (Send (SessionState prog prog' ((,,) current outgoing incoming)))
(Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog' idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (SendPid True idxs) (Send (Pid prog' prog invertedSessions sessionsToIdx idxsToPairStructs))
(Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (SendPid False idxs) (Send (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs))
SNonTerminal (Send t)
SNoJumpsBeyond (Send t) idx
Dual (Recv t) (Send t)
Dual (Send t) (Recv t)
data Recv whereSource
Constructors
Recv :: t -> Recv t
RecvInt :: Recv Int
RecvBool :: Recv Bool
RecvChar :: Recv Char
RecvStr :: Recv String
RecvDouble :: Recv Double
show/hide Instances
(Outgoing current ~ outgoing, Outgoing current' ~ incoming, Dual prog prog', Expand prog' frag current, Dual frag frag', Expand prog' frag' current') => ExpandSession prog (RecvSession True frag) (Recv (SessionState prog' prog ((,,) current outgoing incoming)))
(Outgoing current ~ outgoing, Outgoing current' ~ incoming, Dual prog prog', Expand prog frag current, Dual frag frag', Expand prog frag' current') => ExpandSession prog (RecvSession False frag) (Recv (SessionState prog prog' ((,,) current outgoing incoming)))
(Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog' idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (RecvPid True idxs) (Recv (Pid prog' prog invertedSessions sessionsToIdx idxsToPairStructs))
(Dual prog prog', BuildInvertedSessionsSet idxs invertedSessions, BuildPidTyMap prog idxs (TyMap sessionsToIdx idxsToPairStructs)) => ExpandPid prog (RecvPid False idxs) (Recv (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs))
SNonTerminal (Recv t)
SNoJumpsBeyond (Recv t) idx
Dual (Recv t) (Send t)
Dual (Send t) (Recv t)
data Jump l Source
Constructors
Jump l
show/hide Instances
jump :: TyNum n => n -> Cons (Jump n) NilSource
data Select whereSource
Constructors
Select :: lstOfLabels -> Select lstOfLabels
show/hide 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)
select :: SListOfJumps (Cons val nxt) => Cons val nxt -> Cons (Select (Cons val nxt)) NilSource
data Offer whereSource
Constructors
Offer :: lstOfLabels -> Offer lstOfLabels
show/hide 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)
offer :: SListOfJumps (Cons val nxt) => Cons val nxt -> Cons (Offer (Cons val nxt)) NilSource
class Dual a b | a -> b, b -> a whereSource
Associated Types
type DualT a Source
Methods
dual :: a -> bSource
show/hide 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)
(TyList nxt, TyList nxt', Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt')
Not inverted inverted' => Dual (RecvSession inverted idx) (SendSession inverted' idx)
Not inverted inverted' => Dual (RecvSession inverted idx) (SendSession inverted' idx)
Not inverted inverted' => Dual (SendSession inverted idx) (RecvSession inverted' idx)
Not inverted inverted' => Dual (SendSession inverted idx) (RecvSession inverted' idx)
Not inverted inverted' => Dual (RecvPid inverted lst) (SendPid inverted' lst)
Not inverted inverted' => Dual (RecvPid inverted lst) (SendPid inverted' lst)
Not inverted inverted' => Dual (SendPid inverted lst) (RecvPid inverted' lst)
Not inverted inverted' => Dual (SendPid inverted lst) (RecvPid inverted' lst)
class SListOfJumps lst Source
show/hide Instances
class SListOfSessionTypes lstOfLists Source
show/hide Instances
class SNonTerminal a Source
show/hide Instances
class STerminal a Source
show/hide Instances
STerminal End
SListOfJumps (Cons val nxt) => STerminal (Offer (Cons val nxt))
SListOfJumps (Cons val nxt) => STerminal (Select (Cons val nxt))
TyNum l => STerminal (Jump l)
class SValidSessionType lst Source
show/hide Instances
(~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> Cons a nxtSource
(~|~) :: (TyNum target, TyList nxt) => target -> nxt -> Cons (Cons (Jump target) Nil) nxtSource
class SNoJumpsBeyond s idx Source
show/hide Instances
SNoJumpsBeyond Nil idx
SNoJumpsBeyond End idx
SNoJumpsBeyond lol idx => SNoJumpsBeyond (Offer lol) idx
SNoJumpsBeyond lol idx => SNoJumpsBeyond (Select lol) idx
SmallerThanBool l idx True => SNoJumpsBeyond (Jump l) idx
SNoJumpsBeyond (Recv t) idx
SNoJumpsBeyond (Send t) idx
(SNoJumpsBeyond val idx, SNoJumpsBeyond nxt idx) => SNoJumpsBeyond (Cons val nxt) idx
SNoJumpsBeyond l idx => SNoJumpsBeyond (RecvSession inverted l) idx
SNoJumpsBeyond l idx => SNoJumpsBeyond (SendSession inverted l) idx
(MakeListOfJumps lol lol', SNoJumpsBeyond lol' idx) => SNoJumpsBeyond (RecvPid inverted lol) idx
(MakeListOfJumps lol lol', SNoJumpsBeyond lol' idx) => SNoJumpsBeyond (SendPid inverted lol) idx
class MakeListOfJumps x y | x -> y whereSource
Methods
makeListOfJumps :: x -> ySource
show/hide Instances
MakeListOfJumps Nil Nil
(TyNum num, MakeListOfJumps nxt nxt', TyList nxt, TyList nxt') => MakeListOfJumps (Cons ((,) num invert) nxt) (Cons (Cons (Jump num) Nil) nxt')
class SWellFormedConfig idxA idxB ss Source
testWellformed :: SWellFormedConfig idxA idxB ss => ss -> idxA -> idxB -> BoolSource
data Choice whereSource
Constructors
Choice :: lstOfLabels -> Choice lstOfLabels
type family Outgoing frag Source
class Expand prog frag expanded | prog frag -> expandedSource
Associated Types
type ExpandT prog frag Source
Methods
show/hide Instances
Expand prog (Cons End Nil) (Cons End Nil)
Expand prog (Cons (Jump l) Nil) (Cons (Jump l) Nil)
Expand prog (Cons (Offer loj) Nil) (Cons (Offer loj) Nil)
Expand prog (Cons (Select loj) Nil) (Cons (Select loj) Nil)
Expand prog nxt nxt' => Expand prog (Cons (Recv t) nxt) (Cons (Recv t) nxt')
Expand prog nxt nxt' => Expand prog (Cons (Send t) nxt) (Cons (Send t) nxt')
(Expand prog nxt nxt', ExpandSession prog (RecvSession invert frag) expandedRecvSession) => Expand prog (Cons (RecvSession invert frag) nxt) (Cons expandedRecvSession nxt')
(Expand prog nxt nxt', ExpandSession prog (SendSession invert frag) expandedSendSession) => Expand prog (Cons (SendSession invert frag) nxt) (Cons expandedSendSession nxt')
(Expand prog nxt nxt', ExpandPid prog (RecvPid invert idxs) expandedRecvPid) => Expand prog (Cons (RecvPid invert idxs) nxt) (Cons expandedRecvPid nxt')
(Expand prog nxt nxt', ExpandPid prog (SendPid invert idxs) expandedSendPid) => Expand prog (Cons (SendPid invert idxs) nxt) (Cons expandedSendPid nxt')
Produced by Haddock version 2.4.2