sessions-2008.2.23: Session Types for Haskell

Control.Concurrent.Session.List

Description

Heterogeneous lists. This has been done many times, in many different ways. Explicit constructors are hidden deliberately.

Synopsis

Documentation

data Cons whereSource

Constructors

Cons :: t -> n -> Cons t n 

Instances

SListOfJumps (Cons val nxt) => STerminal (Offer (Cons val nxt)) 
SListOfJumps (Cons val nxt) => STerminal (Select (Cons val nxt)) 
(ListLength n l, Succ l l', Show n, Show t) => Show (Cons t n) 
TyList nxt => TyList (Cons val nxt) 
(SValidSessionType nxt, SNonTerminal val) => SValidSessionType (Cons val nxt) 
STerminal a => SValidSessionType (Cons a Nil) 
(SValidSessionType val, SListOfSessionTypes nxt) => SListOfSessionTypes (Cons val nxt) 
(SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) nxt) 
(ListLength n len, Succ len len') => ListLength (Cons t n) len' 
OnlyOutgoing nxt nxt' => OnlyOutgoing (Cons (Recv t) nxt) nxt' 
(SNoJumpsBeyond val idx, SNoJumpsBeyond nxt idx) => SNoJumpsBeyond (Cons val nxt) idx 
(Elem nxt idx' res, Pred idx idx', SmallerThan idx' len, ListLength nxt len) => Elem (Cons val nxt) idx res 
Elem (Cons res nxt) (D0 E) res 
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) 
(Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt') 
(ProgramToMVarsOutgoing nxt nxt', OnlyOutgoing val val') => ProgramToMVarsOutgoing (Cons val nxt) (Cons (MVar (ProgramCell (Cell val'))) nxt') 

class ListLength list length | list -> length whereSource

Find the length of a list.

Methods

listLength :: list -> lengthSource

Instances

ListLength Nil (D0 E) 
(ListLength n len, Succ len len') => ListLength (Cons t n) len' 

cons :: TyList n => t -> n -> Cons t nSource

class TyList l Source

Instances

TyList Nil 
TyList nxt => TyList (Cons val nxt) 

class Elem lst idx res | lst idx -> res whereSource

Index or update a list

Methods

tyListElem :: lst -> idx -> resSource

tyListUpdate :: lst -> idx -> res -> lstSource

Instances

(Elem nxt idx' res, Pred idx idx', SmallerThan idx' len, ListLength nxt len) => Elem (Cons val nxt) idx res 
Elem (Cons res nxt) (D0 E) res