Safe Haskell | None |
---|---|
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 where ...
- findFirst :: forall x ts n. ListContains n x ts => HVect ts -> x
- type family InList (x :: *) (xs :: [*]) :: Nat where ...
- type ListContains n x ts = (SNatRep n, InList x ts ~ n, HVectIdx n ts ~ x)
- type family NotInList (x :: *) (xs :: [*]) :: Bool where ...
- type family MaybeToList (a :: Maybe *) :: [*] where ...
- (!!) :: SNat n -> HVect as -> HVectIdx n as
- type family HVectIdx (n :: Nat) (ts :: [*]) :: * where ...
- type family HVectElim (ts :: [*]) (a :: *) :: * where ...
- type family Append (as :: [*]) (bs :: [*]) :: [*] where ...
- (<++>) :: HVect as -> HVect bs -> HVect (Append as bs)
- type family ReverseLoop (as :: [*]) (bs :: [*]) :: [*] where ...
- 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
- type family AllHave (c :: * -> Constraint) (xs :: [*]) :: Constraint where ...
- data Nat where
- data SNat n where
- sNatToInt :: SNat n -> Int
- intToSNat :: Int -> AnySNat
- data AnySNat where
- type family (m :: Nat) :< (n :: Nat) :: Bool where ...
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 MaybeToList (a :: Maybe *) :: [*] where ... Source #
MaybeToList (Just r) = '[r] | |
MaybeToList Nothing = '[] |
type family ReverseLoop (as :: [*]) (bs :: [*]) :: [*] where ... Source #
ReverseLoop '[] bs = bs | |
ReverseLoop (a ': as) bs = ReverseLoop as (a ': bs) |
type Reverse as = ReverseLoop as '[] Source #
type class constraints on list elements
type family AllHave (c :: * -> Constraint) (xs :: [*]) :: Constraint where ... Source #