Heterogeneous lists. This has been done many times, in many different ways. Explicit constructors are hidden deliberately.
- data Nil where
- data Cons where
- 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
Show Nil | |
TyList Nil | |
SListOfSessionTypes Nil | |
SListOfJumps Nil | |
SNoJumpsBeyond Nil idx | |
Dual Nil Nil | |
ProgramToMVarsOutgoing Nil Nil | |
ListLength Nil (D0 E) | |
STerminal a => SValidSessionType (Cons a Nil) | |
(SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) 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 (Cons End Nil) (Cons End Nil) |
class ListLength list length | list -> length whereSource
Find the length of a list.
listLength :: list -> lengthSource
ListLength Nil (D0 E) | |
(ListLength n len, Succ len len') => ListLength (Cons t n) len' |
class Elem lst idx res | lst idx -> res whereSource
Index or update a list
tyListElem :: lst -> idx -> resSource
tyListUpdate :: lst -> idx -> res -> lstSource
(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 |