hvect-0.3.1.0: Simple strict heterogeneous lists

Safe HaskellSafe
LanguageHaskell2010

Data.HVect

Contents

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)) Source 
Eq (HVect ([] *)) Source 
(Ord (HVect ts), Ord t) => Ord (HVect ((:) * t ts)) Source 
Ord (HVect ([] *)) Source 
(Show (HVect ts), Show t) => Show (HVect ((:) * t ts)) Source 
Show (HVect ([] *)) Source 

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 

type family MaybeToList a :: [*] Source

Equations

MaybeToList (Just r) = `[r]` 
MaybeToList Nothing = `[]` 

(!!) :: 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 ([] *) Source 
HasRep ts => HasRep ((:) * t ts) Source 

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