hvect-0.3.0.0: Simple strict heterogeneous lists

Data.HVect

Synopsis

# typesafe strict vector

data HVect ts where Source

Heterogeneous vector

Constructors

 HNil :: HVect [] (:&:) :: !t -> !(HVect ts) -> HVect (t : ts) infixr 5

Instances

 (Eq (HVect ts), Eq t) => Eq (HVect ((:) * t ts)) Eq (HVect ([] *)) (Ord (HVect ts), Ord t) => Ord (HVect ((:) * t ts)) Ord (HVect ([] *)) (Show (HVect ts), Show t) => Show (HVect ((:) * t ts)) Show (HVect ([] *))

head :: HVect (t : ts) -> t Source

tail :: HVect (t : ts) -> HVect ts Source

singleton :: a -> HVect `[a]` Source

type family HVectLen ts :: Nat Source

Equations

 HVectLen [] = Zero HVectLen (t : ts) = Succ (HVectLen ts)

findFirst :: forall x ts n. ListContains n x ts => HVect ts -> x Source

Find first element in `HVect` of type x

type family InList x xs :: Nat Source

Equations

 InList x (x : ys) = Zero InList x (y : ys) = Succ (InList x ys)

type ListContains n x ts = (SNatRep n, InList x ts ~ n, HVectIdx n ts ~ x) Source

type family NotInList x xs :: Bool Source

Equations

 NotInList x (x : ys) = False NotInList x (y : ys) = NotInList x ys NotInList x [] = True

(!!) :: SNat n -> HVect as -> HVectIdx n as infixl 9 Source

type family HVectIdx n ts :: * Source

Equations

 HVectIdx Zero (a : as) = a HVectIdx (Succ n) (a : as) = HVectIdx n as

type family HVectElim ts a :: * Source

Equations

 HVectElim [] a = a HVectElim (t : ts) a = t -> HVectElim ts a

type family Append as bs :: [*] Source

Equations

 Append [] bs = bs Append (a : as) bs = a : Append as bs

(<++>) :: HVect as -> HVect bs -> HVect (Append as bs) infixr 5 Source

type family ReverseLoop as bs :: [*] Source

Equations

 ReverseLoop [] bs = bs ReverseLoop (a : as) bs = ReverseLoop as (a : bs)

type Reverse as = ReverseLoop as [] Source

uncurry :: HVectElim ts a -> HVect ts -> a Source

data Rep ts where Source

Constructors

 RNil :: Rep [] RCons :: Rep ts -> Rep (t : ts)

class HasRep ts where Source

Methods

hasRep :: Rep ts Source

Instances

 HasRep ([] *) HasRep ts => HasRep ((:) * t ts)

curryExpl :: Rep ts -> (HVect ts -> a) -> HVectElim ts a Source

curry :: HasRep ts => (HVect ts -> a) -> HVectElim ts a Source

packExpl :: Rep ts -> (forall a. HVectElim ts a -> a) -> HVect ts Source

pack :: HasRep ts => (forall a. HVectElim ts a -> a) -> HVect ts Source

# type level numeric utilities

data Nat where Source

Constructors

 Zero :: Nat Succ :: Nat -> Nat

data SNat n where Source

Constructors

 SZero :: SNat Zero SSucc :: SNat n -> SNat (Succ n)

data AnySNat where Source

Constructors

 AnySNat :: forall n. SNat n -> AnySNat

type family m :< n :: Bool Source

Equations

 m :< Zero = False Zero :< (Succ n) = True (Succ m) :< (Succ n) = m :< n