sessions-2008.2.23: Session Types for Haskell Source code Contents Index

Control.Concurrent.Session.List

Description

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

Synopsis

data Nil where Nil :: Nil data Cons where Cons :: t -> n -> Cons t n class ListLength list length | list -> length where listLength :: list -> length nil :: Nil cons :: TyList n => t -> n -> Cons t n class TyList l class Elem lst idx res | lst idx -> res where tyListElem :: lst -> idx -> res tyListUpdate :: lst -> idx -> res -> lst

Documentation

data Nil where Source

Constructors Nil :: Nil Instances Show Nil TyList Nil SListOfSessionTypes Nil SListOfJumps Nil SNoJumpsBeyond Nil idx Dual Nil Nil ProgramToMVarsOutgoing Nil Nil ListLength Nil (D0 E)

data Cons where Source

Constructors Cons :: t -> n -> Cons t n Instances (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 where Source

Find the length of a list. Methods listLength :: list -> length Source Instances ListLength Nil (D0 E) ListLength Nil (D0 E) (ListLength n len, Succ len len') => ListLength (Cons t n) len'

nil :: Nil Source

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

class TyList l Source

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

class Elem lst idx res | lst idx -> res where Source

Index or update a list Methods tyListElem :: lst -> idx -> res Source tyListUpdate :: lst -> idx -> res -> lst Source 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 Elem (Cons res nxt) (D0 E) res

Produced by Haddock version 2.3.0