module Control.Concurrent.Session.List where
import Control.Concurrent.Session.Number
data Nil :: * where
Nil :: Nil
data Cons :: * -> * -> * where
Cons :: t -> n -> Cons t n
class ListLength list length | list -> length where
listLength :: list -> length
instance ListLength Nil (D0 E) where
listLength Nil = (D0 E)
instance (ListLength n len, Succ len len') => ListLength (Cons t n) len' where
listLength (Cons _ nxt) = tySucc . listLength $ nxt
instance Show Nil where
show Nil = "Nil"
instance (ListLength n l, Succ l l', Show n, Show t) => Show (Cons t n) where
show (Cons val nxt) = "Cons " ++ (show val) ++ " (" ++ (show nxt) ++ ")"
nil :: Nil
nil = Nil
cons :: (TyList n) => t -> n -> (Cons t n)
cons t n = Cons t n
class TyList l
instance TyList Nil
instance (TyList nxt) => TyList (Cons val nxt)
class Elem lst idx res | lst idx -> res where
tyListElem :: lst -> idx -> res
tyListUpdate :: lst -> idx -> res -> lst
instance Elem (Cons res nxt) (D0 E) res where
tyListElem (Cons val _) _ = val
tyListUpdate (Cons _ nxt) _ val = (Cons val nxt)
instance ( Elem nxt idx' res
, Pred idx idx'
, SmallerThan idx' len
, ListLength nxt len) =>
Elem (Cons val nxt) idx res where
tyListElem (Cons _ nxt) idx = tyListElem nxt (tyPred idx)
tyListUpdate (Cons val nxt) idx val'
= Cons val (tyListUpdate nxt (tyPred idx) val')