Data.HVect

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

Defined in Data.HVect

Methods

(==) :: HVect (t ': ts) -> HVect (t ': ts) -> Bool

(/=) :: HVect (t ': ts) -> HVect (t ': ts) -> Bool

Eq (HVect ('[] :: [Type]))

Defined in Data.HVect

Methods

(==) :: HVect '[] -> HVect '[] -> Bool

(/=) :: HVect '[] -> HVect '[] -> Bool

(Ord (HVect ts), Ord t) => Ord (HVect (t ': ts))

Defined in Data.HVect

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 ('[] :: [Type]))

Defined in Data.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))

Defined in Data.HVect

Methods

showsPrec :: Int -> HVect (t ': ts) -> ShowS

show :: HVect (t ': ts) -> String

showList :: [HVect (t ': ts)] -> ShowS

Show (HVect ('[] :: [Type]))

Defined in Data.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

Methods

hasRep :: Rep ts

Instances

HasRep ('[] :: [Type])

Defined in Data.HVect

Methods

hasRep :: Rep '[]

HasRep ts => HasRep (t ': ts)

Defined in Data.HVect

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