Control.Concurrent.Session.SessionType

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

Constructors

End

Instances

Show End

STerminal End

SNoJumpsBeyond End idx

Dual End End

OnlyOutgoing (Cons End Nil) (Cons End Nil)

end :: Cons End Nil

data Send where

Constructors

Send :: t -> Send t

SendInt :: Send Int

SendBool :: Send Bool

SendChar :: Send Char

SendStr :: Send String

SendDouble :: Send Double

Instances

SNonTerminal (Send t)

SNoJumpsBeyond (Send t) idx

Dual (Recv t) (Send t)

Dual (Send t) (Recv t)

OnlyOutgoing nxt nxt' => OnlyOutgoing (Cons (Send t) nxt) (Cons t nxt')

data Recv where

Constructors

Recv :: t -> Recv t

RecvInt :: Recv Int

RecvBool :: Recv Bool

RecvChar :: Recv Char

RecvStr :: Recv String

RecvDouble :: Recv Double

Instances

SNonTerminal (Recv t)

SNoJumpsBeyond (Recv t) idx

Dual (Recv t) (Send t)

Dual (Send t) (Recv t)

OnlyOutgoing nxt nxt' => OnlyOutgoing (Cons (Recv t) nxt) nxt'

data Jump l

Constructors

Jump l

Instances

Show l => Show (Jump l)

TyNum l => STerminal (Jump l)

SmallerThan l idx => SNoJumpsBeyond (Jump l) idx

Dual (Jump l) (Jump l)

(SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) nxt)

OnlyOutgoing (Cons (Jump l) Nil) (Cons (Jump l) Nil)

jump :: TyNum n => n -> Cons (Jump n) Nil

data Select where

Constructors

Select :: lstOfLabels -> Select lstOfLabels

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)

OnlyOutgoing (Cons (Select jl) Nil) (Cons (Choice jl) Nil)

select :: SListOfJumps (Cons val nxt) => Cons val nxt -> Cons (Select (Cons val nxt)) Nil

data Offer where

Constructors

Offer :: lstOfLabels -> Offer lstOfLabels

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)

OnlyOutgoing (Cons (Offer jl) Nil) (Cons (Choice jl) Nil)

offer :: SListOfJumps (Cons val nxt) => Cons val nxt -> Cons (Offer (Cons val nxt)) Nil

class Dual a b | a -> b, b -> a where

Methods

dual :: a -> b

Instances

Dual Nil Nil

Dual End End

Dual (Offer lst) (Select lst)

Dual (Select lst) (Offer lst)

Dual (Jump l) (Jump l)

Dual (Recv t) (Send t)

Dual (Send t) (Recv t)

(Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt')

class SListOfJumps lst

Instances

SListOfJumps Nil

(SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) nxt)

class SListOfSessionTypes lstOfLists

Instances

SListOfSessionTypes Nil

(SValidSessionType val, SListOfSessionTypes nxt) => SListOfSessionTypes (Cons val nxt)

class SNonTerminal a

Instances

SNonTerminal (Recv t)

SNonTerminal (Send t)

class STerminal a

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

Instances

(SValidSessionType nxt, SNonTerminal val) => SValidSessionType (Cons val nxt)

STerminal a => SValidSessionType (Cons a Nil)

(~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> Cons a nxt

(~|~) :: (TyNum target, TyList nxt) => target -> nxt -> Cons (Cons (Jump target) Nil) nxt

class SNoJumpsBeyond s idx

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

class SWellFormedConfig idxA idxB ss

Instances

(SListOfSessionTypes ss, ListLength ss len, SNoJumpsBeyond ss len, SmallerThan idxA len, Elem ss idxA st, ListLength st len', SmallerThan idxB len') => SWellFormedConfig idxA idxB ss

testWellformed :: SWellFormedConfig idxA idxB ss => ss -> idxA -> idxB -> Bool

data Choice where

Constructors

Choice :: lstOfLabels -> Choice lstOfLabels

Instances

OnlyOutgoing (Cons (Offer jl) Nil) (Cons (Choice jl) Nil)

OnlyOutgoing (Cons (Select jl) Nil) (Cons (Choice jl) Nil)

class OnlyOutgoing a b | a -> b where

Methods

onlyOutgoing :: a -> b

Instances

OnlyOutgoing nxt nxt' => OnlyOutgoing (Cons (Recv t) nxt) nxt'

OnlyOutgoing (Cons (Offer jl) Nil) (Cons (Choice jl) Nil)

OnlyOutgoing (Cons (Select jl) Nil) (Cons (Choice jl) Nil)

OnlyOutgoing (Cons (Jump l) Nil) (Cons (Jump l) Nil)

OnlyOutgoing nxt nxt' => OnlyOutgoing (Cons (Send t) nxt) (Cons t nxt')

OnlyOutgoing (Cons End Nil) (Cons End Nil)