Safe Haskell	None
Language	Haskell2010

Data.HVect

Contents

typesafe strict vector
type class constraints on list elements
type level numeric utilities

Synopsis

typesafe strict vector

data HVect (ts :: [*]) where #

Heterogeneous vector

Constructors

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

Instances

(Eq (HVect ts), Eq t) => Eq (HVect ((:) * t ts)) #
Methods (==) :: HVect ((* ': t) ts) -> HVect ((* ': t) ts) -> Bool # (/=) :: HVect ((* ': t) ts) -> HVect ((* ': t) ts) -> Bool #
Eq (HVect ([] *)) #
Methods (==) :: HVect [] -> HVect [] -> Bool # (/=) :: HVect [] -> HVect [] -> Bool #
(Ord (HVect ts), Ord t) => Ord (HVect ((:) * t ts)) #
Methods compare :: HVect ((* ': t) ts) -> HVect ((* ': t) ts) -> Ordering # (<) :: HVect ((* ': t) ts) -> HVect ((* ': t) ts) -> Bool # (<=) :: HVect ((* ': t) ts) -> HVect ((* ': t) ts) -> Bool # (>) :: HVect ((* ': t) ts) -> HVect ((* ': t) ts) -> Bool # (>=) :: HVect ((* ': t) ts) -> HVect ((* ': t) ts) -> Bool # max :: HVect ((* ': t) ts) -> HVect ((* ': t) ts) -> HVect ((* ': t) ts) # min :: HVect ((* ': t) ts) -> HVect ((* ': t) ts) -> HVect ((* ': t) ts) #
Ord (HVect ([] *)) #
Methods compare :: HVect [] -> HVect [] -> Ordering # (<) :: HVect [] -> HVect [] -> Bool # (<=) :: HVect [] -> HVect [] -> Bool # (>) :: HVect [] -> HVect [] -> Bool # (>=) :: HVect [] -> HVect [] -> Bool # max :: HVect [] -> HVect [] -> HVect [] # min :: HVect [] -> HVect [] -> HVect [] #
(Show (HVect ts), Show t) => Show (HVect ((:) * t ts)) #
Methods showsPrec :: Int -> HVect ((* ': t) ts) -> ShowS # show :: HVect ((* ': t) ts) -> String # showList :: [HVect ((* ': t) ts)] -> ShowS #
Show (HVect ([] *)) #
Methods showsPrec :: Int -> HVect [] -> ShowS # show :: HVect [] -> String # showList :: [HVect [*]] -> ShowS #

empty :: HVect '[] #

null :: HVect as -> Bool #

head :: HVect (t ': ts) -> t #

tail :: HVect (t ': ts) -> HVect ts #

singleton :: a -> HVect '[a] #

length :: HVect as -> SNat (HVectLen as) #

type family HVectLen (ts :: [*]) :: Nat where ... #

Equations

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

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

Find first element in HVect of type x

type family InList (x :: *) (xs :: [*]) :: Nat where ... #

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) #

type family NotInList (x :: *) (xs :: [*]) :: Bool where ... #

Equations

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

type family MaybeToList (a :: Maybe *) :: [*] where ... #

Equations

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

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

type family HVectIdx (n :: Nat) (ts :: [*]) :: * where ... #

Equations

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

type family HVectElim (ts :: [*]) (a :: *) :: * where ... #

Equations

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

type family Append (as :: [*]) (bs :: [*]) :: [*] where ... #

Equations

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

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

type family ReverseLoop (as :: [*]) (bs :: [*]) :: [*] where ... #

Equations

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

type Reverse as = ReverseLoop as '[] #

reverse :: HVect as -> HVect (Reverse as) #

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

data Rep (ts :: [*]) where #

Constructors

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

class HasRep (ts :: [*]) where #

Minimal complete definition

hasRep

Methods

hasRep :: Rep ts #

Instances

HasRep ([] *) #
Methods hasRep :: Rep [*] #
HasRep ts => HasRep ((:) * t ts) #
Methods hasRep :: Rep ((* ': t) ts) #

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

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

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

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

type class constraints on list elements

type family AllHave (c :: * -> Constraint) (xs :: [*]) :: Constraint where ... #

Equations

AllHave c '[] = True ~ True
AllHave c (x ': xs) = (c x, AllHave c xs)

type level numeric utilities

data Nat where #

Constructors

Zero :: Nat
Succ :: Nat -> Nat

data SNat (n :: Nat) where #

Constructors

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

sNatToInt :: SNat n -> Int #

intToSNat :: Int -> AnySNat #

data AnySNat where #

Constructors

AnySNat :: forall n. SNat n -> AnySNat

type family (m :: Nat) :< (n :: Nat) :: Bool where ... #

Equations

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