Safe Haskell | Safe-Inferred |
---|---|

Language | Haskell2010 |

- data HVect ts where
- 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
- findFirst :: forall x ts n. ListContains n x ts => HVect ts -> x
- type family InList x xs :: Nat
- type ListContains n x ts = (SNatRep n, InList x ts ~ n, HVectIdx n ts ~ x)
- type family NotInList x xs :: Bool
- (!!) :: SNat n -> HVect as -> HVectIdx n as
- type family HVectIdx n ts :: *
- type family HVectElim ts a :: *
- type family Append as bs :: [*]
- (<++>) :: HVect as -> HVect bs -> HVect (Append as bs)
- type family ReverseLoop as bs :: [*]
- type Reverse as = ReverseLoop as []
- reverse :: HVect as -> HVect (Reverse as)
- uncurry :: HVectElim ts a -> HVect ts -> a
- data Rep ts where
- class HasRep ts where
- 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
- data Nat where
- data SNat n where
- sNatToInt :: SNat n -> Int
- intToSNat :: Int -> AnySNat
- data AnySNat where
- type family m :< n :: Bool

# typesafe strict vector

Heterogeneous vector

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

Find first element in `HVect`

of type x

type ListContains n x ts = (SNatRep n, InList x ts ~ n, HVectIdx n ts ~ x) Source

type family ReverseLoop as bs :: [*] Source

ReverseLoop [] bs = bs | |

ReverseLoop (a : as) bs = ReverseLoop as (a : bs) |

type Reverse as = ReverseLoop as [] Source