Safe Haskell	Safe
Language	Haskell2010

Data.HVect

Contents

typesafe strict vector
type level numeric utilities

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

empty :: HVect `[]` Source

null :: HVect as -> Bool Source

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

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

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

length :: HVect as -> SNat (HVectLen as) 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

reverse :: HVect as -> HVect (Reverse 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)

sNatToInt :: SNat n -> Int Source

intToSNat :: Int -> AnySNat Source

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