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

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

Instances

type HVectLen ([] *) = Zero
type HVectLen ((:) * t ts) = Succ (HVectLen ts)

(!!) :: ((n :< HVectLen as) ~ True) => SNat n -> HVect as -> HVectIdx n as infixl 9 Source

type family HVectIdx n ts :: * Source

Instances

type HVectIdx a ([] *) = ()
type HVectIdx Zero ((:) * a as) = a
type HVectIdx (Succ n) ((:) * a as) = HVectIdx n as

type family HVectElim ts a :: * Source

Instances

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

type family Append as bs :: [*] Source

Instances

type Append ([] *) bs = bs
type 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

Instances

type ReverseLoop ([] *) bs = bs
type 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 ([] *)
HasRep ts => HasRep ((:) * t ts)

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

Instances

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