| ||||||||||||||||||||
| ||||||||||||||||||||
| 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 | ||||||||||||||||||||
| ||||||||||||||||||||
| end :: Cons End Nil | ||||||||||||||||||||
| data Send where | ||||||||||||||||||||
| ||||||||||||||||||||
| data Recv where | ||||||||||||||||||||
| ||||||||||||||||||||
| data Jump l | ||||||||||||||||||||
| ||||||||||||||||||||
| jump :: TyNum n => n -> Cons (Jump n) Nil | ||||||||||||||||||||
| data Select where | ||||||||||||||||||||
| ||||||||||||||||||||
| select :: SListOfJumps (Cons val nxt) => (Cons val nxt) -> Cons (Select (Cons val nxt)) Nil | ||||||||||||||||||||
| data Offer where | ||||||||||||||||||||
| ||||||||||||||||||||
| offer :: SListOfJumps (Cons val nxt) => (Cons val nxt) -> Cons (Offer (Cons val nxt)) Nil | ||||||||||||||||||||
| class Dual a b | a -> b, b -> a where | ||||||||||||||||||||
| ||||||||||||||||||||
| class SListOfJumps lst | ||||||||||||||||||||
| ||||||||||||||||||||
| class SListOfSessionTypes lstOfLists | ||||||||||||||||||||
| ||||||||||||||||||||
| class SNonTerminal a | ||||||||||||||||||||
| ||||||||||||||||||||
| class STerminal a | ||||||||||||||||||||
| ||||||||||||||||||||
| class SValidSessionType lst | ||||||||||||||||||||
| ||||||||||||||||||||
| (~>) :: (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 | ||||||||||||||||||||
| ||||||||||||||||||||
| class SWellFormedConfig idxA idxB ss | ||||||||||||||||||||
| testWellformed :: SWellFormedConfig idxA idxB ss => ss -> idxA -> idxB -> Bool | ||||||||||||||||||||
| data Choice where | ||||||||||||||||||||
| ||||||||||||||||||||
| class OnlyOutgoing a b | a -> b where | ||||||||||||||||||||
| ||||||||||||||||||||
| Produced by Haddock version 2.1.0 |