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

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