sessions-2008.3.25: 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', TyListReverse lst' lst'') => lst -> SendPid False lst''Source
recvPid :: (TyListSortNums lst lst', TyListReverse lst' lst'') => lst -> RecvPid False lst''Source
data SendPid inverted lst Source
Constructors
SendPid inverted lst
show/hide Instances
(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
(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)
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
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
data Jump l Source
Constructors
Jump l
show/hide Instances
Show l => Show (Jump l)
TyNum l => STerminal (Jump l)
SmallerThan l idx => SNoJumpsBeyond (Jump l) idx
Dual (Jump l) (Jump l)
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 (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
SmallerThan l idx => SNoJumpsBeyond (Jump l) idx
SNoJumpsBeyond (Recv t) idx
SNoJumpsBeyond (Send t) idx
(SNoJumpsBeyond val idx, SNoJumpsBeyond nxt idx) => SNoJumpsBeyond (Cons val nxt) 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 prog frag Source
class ExpandPids p a b | p a -> b whereSource
Methods
expandPids :: p -> a -> bSource
show/hide Instances
ExpandPids p (Cons (Select loj) Nil) (Cons (Select loj) Nil)
ExpandPids p (Cons (Offer loj) Nil) (Cons (Offer loj) Nil)
ExpandPids p (Cons (Jump l) Nil) (Cons (Jump l) Nil)
(ExpandPids p nxt nxt', TyList nxt, TyList nxt') => ExpandPids p (Cons (Send t) nxt) (Cons (Send t) nxt')
(ExpandPids p nxt nxt', TyList nxt, TyList nxt') => ExpandPids p (Cons (Recv t) nxt) (Cons (Recv t) nxt')
ExpandPids p (Cons End Nil) (Cons End Nil)
(ExpandPids prog nxt nxt', TyList nxt, TyList nxt', BuildPidTyMap progO t (TyMap sessionsToIdx idxsToPairStructs), If invert prog' prog progO, Dual prog prog') => ExpandPids prog (Cons (SendPid invert t) nxt) (Cons (Send (Pid progO sessionsToIdx idxsToPairStructs)) nxt')
(ExpandPids prog nxt nxt', TyList nxt, TyList nxt', BuildPidTyMap progO t (TyMap sessionsToIdx idxsToPairStructs), If invert prog' prog progO, Dual prog prog') => ExpandPids prog (Cons (RecvPid invert t) nxt) (Cons (Recv (Pid progO sessionsToIdx idxsToPairStructs)) nxt')
Produced by Haddock version 2.3.0