sessions-2008.3.23: 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
data SendPid lst Source
Constructors
SendPid lst
show/hide Instances
Show lst => Show (SendPid lst)
SNonTerminal (SendPid t)
(MakeListOfJumps lol lol', SNoJumpsBeyond lol' idx) => SNoJumpsBeyond (SendPid lol) idx
Dual (RecvPid lst) (SendPid lst)
Dual (SendPid lst) (RecvPid lst)
data RecvPid lst Source
Constructors
RecvPid lst
show/hide Instances
Show lst => Show (RecvPid lst)
SNonTerminal (RecvPid t)
(MakeListOfJumps lol lol', SNoJumpsBeyond lol' idx) => SNoJumpsBeyond (RecvPid lol) idx
Dual (RecvPid lst) (SendPid lst)
Dual (SendPid lst) (RecvPid 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)
Dual (RecvPid lst) (SendPid lst)
Dual (RecvPid lst) (SendPid lst)
Dual (SendPid lst) (RecvPid lst)
Dual (SendPid lst) (RecvPid lst)
(TyList nxt, TyList nxt', Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt')
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
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
Produced by Haddock version 2.3.0